theorem :: GROUP_4:71

for G being Group holds the L_meet of (lattice G) = SubMeet G ;