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