let G be addGroup; :: thesis: for H being Subgroup of G holds
( ((0). G) /\ H = (0). G & H /\ ((0). G) = (0). G )
let H be Subgroup of G; :: thesis: ( ((0). G) /\ H = (0). G & H /\ ((0). G) = (0). G )
A1: (0). G is Subgroup of H by Th65;
hence ((0). G) /\ H = (0). G by Lm3; :: thesis: H /\ ((0). G) = (0). G
thus H /\ ((0). G) = (0). G by A1, Lm3; :: thesis: verum