theorem :: GROUP_4:70

for G being Group holds the L_join of (lattice G) = SubJoin G ;