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