Structure of subgroups (and similar structures) in set.mm

[Edward McCants]

Taking a look at how subgroups are defined in set.mm (and submonoids, and I presume other sub-structures), I was surprised by what I found.  It seems to be a mapping from a group to a (not necessarily proper) subset of the elements of the group.  My (possibly naive) expectation was for SubGrp to be a relation on groups so that "A SubGrp B" means that A is a subgroup of B.

Is there a particular advantage to this definition?

Aside: I'm looking at this from the perspective of (hopefully) introducing the concept of Simple Groups to set.mm soon.