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