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

for H1 being StableSubgroup of G

for H2 being strict StableSubgroup of G holds

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

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

for H2 being strict StableSubgroup of G holds

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

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

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

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

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

for H1 being StableSubgroup of G

for H2 being strict StableSubgroup of G holds

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

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

for H2 being strict StableSubgroup of G holds

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

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

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

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

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

proof

thus
( H1 "\/" H2 = H2 implies H1 is StableSubgroup of H2 )
by Th35; :: thesis: verum
assume
H1 is StableSubgroup of H2
; :: thesis: H1 "\/" H2 = H2

then H1 is Subgroup of H2 by Def7;

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

hence H1 "\/" H2 = the_stable_subgroup_of (carr H2) by XBOOLE_1:12

.= H2 by Th25 ;

:: thesis: verum

end;then H1 is Subgroup of H2 by Def7;

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

hence H1 "\/" H2 = the_stable_subgroup_of (carr H2) by XBOOLE_1:12

.= H2 by Th25 ;

:: thesis: verum