:: deftheorem Def1 defines carr LATSUBGR:def 1 :
for G being Group
for b₂ being Function of (Subgroups G),(bool the carrier of G) holds
( b₂ = carr G iff for H being strict Subgroup of G holds b₂ . H = the carrier of H );