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

for H1, H2 being StableSubgroup of G holds

( ( for H being StableSubgroup of G st H = H1 /\ H2 holds

the carrier of H = the carrier of H1 /\ the carrier of H2 ) & ( for H being strict StableSubgroup of G st the carrier of H = the carrier of H1 /\ the carrier of H2 holds

H = H1 /\ H2 ) )

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

( ( for H being StableSubgroup of G st H = H1 /\ H2 holds

the carrier of H = the carrier of H1 /\ the carrier of H2 ) & ( for H being strict StableSubgroup of G st the carrier of H = the carrier of H1 /\ the carrier of H2 holds

H = H1 /\ H2 ) )

let H1, H2 be StableSubgroup of G; :: thesis: ( ( for H being StableSubgroup of G st H = H1 /\ H2 holds

the carrier of H = the carrier of H1 /\ the carrier of H2 ) & ( for H being strict StableSubgroup of G st the carrier of H = the carrier of H1 /\ the carrier of H2 holds

H = H1 /\ H2 ) )

A1: ( the carrier of H1 = carr H1 & the carrier of H2 = carr H2 ) ;

thus for H being StableSubgroup of G st H = H1 /\ H2 holds

the carrier of H = the carrier of H1 /\ the carrier of H2 :: thesis: for H being strict StableSubgroup of G st the carrier of H = the carrier of H1 /\ the carrier of H2 holds

H = H1 /\ H2

assume the carrier of H = the carrier of H1 /\ the carrier of H2 ; :: thesis: H = H1 /\ H2

hence H = H1 /\ H2 by A1, Def25; :: thesis: verum

for H1, H2 being StableSubgroup of G holds

( ( for H being StableSubgroup of G st H = H1 /\ H2 holds

the carrier of H = the carrier of H1 /\ the carrier of H2 ) & ( for H being strict StableSubgroup of G st the carrier of H = the carrier of H1 /\ the carrier of H2 holds

H = H1 /\ H2 ) )

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

( ( for H being StableSubgroup of G st H = H1 /\ H2 holds

the carrier of H = the carrier of H1 /\ the carrier of H2 ) & ( for H being strict StableSubgroup of G st the carrier of H = the carrier of H1 /\ the carrier of H2 holds

H = H1 /\ H2 ) )

let H1, H2 be StableSubgroup of G; :: thesis: ( ( for H being StableSubgroup of G st H = H1 /\ H2 holds

the carrier of H = the carrier of H1 /\ the carrier of H2 ) & ( for H being strict StableSubgroup of G st the carrier of H = the carrier of H1 /\ the carrier of H2 holds

H = H1 /\ H2 ) )

A1: ( the carrier of H1 = carr H1 & the carrier of H2 = carr H2 ) ;

thus for H being StableSubgroup of G st H = H1 /\ H2 holds

the carrier of H = the carrier of H1 /\ the carrier of H2 :: thesis: for H being strict StableSubgroup of G st the carrier of H = the carrier of H1 /\ the carrier of H2 holds

H = H1 /\ H2

proof

let H be strict StableSubgroup of G; :: thesis: ( the carrier of H = the carrier of H1 /\ the carrier of H2 implies H = H1 /\ H2 )
let H be StableSubgroup of G; :: thesis: ( H = H1 /\ H2 implies the carrier of H = the carrier of H1 /\ the carrier of H2 )

assume H = H1 /\ H2 ; :: thesis: the carrier of H = the carrier of H1 /\ the carrier of H2

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

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

:: thesis: verum

end;assume H = H1 /\ H2 ; :: thesis: the carrier of H = the carrier of H1 /\ the carrier of H2

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

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

:: thesis: verum

assume the carrier of H = the carrier of H1 /\ the carrier of H2 ; :: thesis: H = H1 /\ H2

hence H = H1 /\ H2 by A1, Def25; :: thesis: verum