:: deftheorem defines lattice GROUP_4:def 12 :
for G being Group holds lattice G = LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #);