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

for H2 being StableSubgroup of G

for H1 being strict StableSubgroup of G holds

( H1 is StableSubgroup of H2 iff H1 /\ H2 = H1 )

let G be GroupWithOperators of O; :: thesis: for H2 being StableSubgroup of G

for H1 being strict StableSubgroup of G holds

( H1 is StableSubgroup of H2 iff H1 /\ H2 = H1 )

let H2 be StableSubgroup of G; :: thesis: for H1 being strict StableSubgroup of G holds

( H1 is StableSubgroup of H2 iff H1 /\ H2 = H1 )

let H1 be strict StableSubgroup of G; :: thesis: ( H1 is StableSubgroup of H2 iff H1 /\ H2 = H1 )

thus ( H1 is StableSubgroup of H2 implies H1 /\ H2 = H1 ) :: thesis: ( H1 /\ H2 = H1 implies H1 is StableSubgroup of H2 )

then the carrier of H1 = (carr H1) /\ (carr H2) by Def25

.= the carrier of H1 /\ the carrier of H2 ;

hence H1 is StableSubgroup of H2 by Lm20, XBOOLE_1:17; :: thesis: verum

for H2 being StableSubgroup of G

for H1 being strict StableSubgroup of G holds

( H1 is StableSubgroup of H2 iff H1 /\ H2 = H1 )

let G be GroupWithOperators of O; :: thesis: for H2 being StableSubgroup of G

for H1 being strict StableSubgroup of G holds

( H1 is StableSubgroup of H2 iff H1 /\ H2 = H1 )

let H2 be StableSubgroup of G; :: thesis: for H1 being strict StableSubgroup of G holds

( H1 is StableSubgroup of H2 iff H1 /\ H2 = H1 )

let H1 be strict StableSubgroup of G; :: thesis: ( H1 is StableSubgroup of H2 iff H1 /\ H2 = H1 )

thus ( H1 is StableSubgroup of H2 implies H1 /\ H2 = H1 ) :: thesis: ( H1 /\ H2 = H1 implies H1 is StableSubgroup of H2 )

proof

assume
H1 /\ H2 = H1
; :: thesis: H1 is StableSubgroup of H2
assume
H1 is StableSubgroup of H2
; :: thesis: H1 /\ H2 = H1

then H1 is Subgroup of H2 by Def7;

then A1: the carrier of H1 c= the carrier of H2 by GROUP_2:def 5;

the carrier of (H1 /\ H2) = (carr H1) /\ (carr H2) by Def25;

hence H1 /\ H2 = H1 by A1, Lm4, XBOOLE_1:28; :: thesis: verum

end;then H1 is Subgroup of H2 by Def7;

then A1: the carrier of H1 c= the carrier of H2 by GROUP_2:def 5;

the carrier of (H1 /\ H2) = (carr H1) /\ (carr H2) by Def25;

hence H1 /\ H2 = H1 by A1, Lm4, XBOOLE_1:28; :: thesis: verum

then the carrier of H1 = (carr H1) /\ (carr H2) by Def25

.= the carrier of H1 /\ the carrier of H2 ;

hence H1 is StableSubgroup of H2 by Lm20, XBOOLE_1:17; :: thesis: verum