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

( ((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