let O be set ; :: thesis: for G being GroupWithOperators of O

for H being strict StableSubgroup of G holds H /\ H = H

let G be GroupWithOperators of O; :: thesis: for H being strict StableSubgroup of G holds H /\ H = H

let H be strict StableSubgroup of G; :: thesis: H /\ H = H

the carrier of (H /\ H) = (carr H) /\ (carr H) by Def25

.= the carrier of H ;

hence H /\ H = H by Lm4; :: thesis: verum

for H being strict StableSubgroup of G holds H /\ H = H

let G be GroupWithOperators of O; :: thesis: for H being strict StableSubgroup of G holds H /\ H = H

let H be strict StableSubgroup of G; :: thesis: H /\ H = H

the carrier of (H /\ H) = (carr H) /\ (carr H) by Def25

.= the carrier of H ;

hence H /\ H = H by Lm4; :: thesis: verum