:: deftheorem Def2 defines meet LATSUBGR:def 2 :
for G being Group
for F being non empty Subset of (Subgroups G)
for b₃ being strict Subgroup of G holds
( b₃ = meet F iff the carrier of b₃ = meet ((carr G) .: F) );