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

for A, B being Subset of G st B = the carrier of (gr A) holds

the_stable_subgroup_of A = the_stable_subgroup_of B

let G be GroupWithOperators of O; :: thesis: for A, B being Subset of G st B = the carrier of (gr A) holds

the_stable_subgroup_of A = the_stable_subgroup_of B

let A, B be Subset of G; :: thesis: ( B = the carrier of (gr A) implies the_stable_subgroup_of A = the_stable_subgroup_of B )

A1: A c= the carrier of (gr A) by GROUP_4:def 4;

assume A2: B = the carrier of (gr A) ; :: thesis: the_stable_subgroup_of A = the_stable_subgroup_of B

then A c= the carrier of (the_stable_subgroup_of B) by A1;

hence the_stable_subgroup_of A = the_stable_subgroup_of B by A3, Def26; :: thesis: verum

for A, B being Subset of G st B = the carrier of (gr A) holds

the_stable_subgroup_of A = the_stable_subgroup_of B

let G be GroupWithOperators of O; :: thesis: for A, B being Subset of G st B = the carrier of (gr A) holds

the_stable_subgroup_of A = the_stable_subgroup_of B

let A, B be Subset of G; :: thesis: ( B = the carrier of (gr A) implies the_stable_subgroup_of A = the_stable_subgroup_of B )

A1: A c= the carrier of (gr A) by GROUP_4:def 4;

assume A2: B = the carrier of (gr A) ; :: thesis: the_stable_subgroup_of A = the_stable_subgroup_of B

A3: now :: thesis: for H being strict StableSubgroup of G st A c= the carrier of H holds

the_stable_subgroup_of B is StableSubgroup of H

the carrier of (gr A) c= the carrier of (the_stable_subgroup_of B)
by A2, Def26;the_stable_subgroup_of B is StableSubgroup of H

let H be strict StableSubgroup of G; :: thesis: ( A c= the carrier of H implies the_stable_subgroup_of B is StableSubgroup of H )

reconsider H9 = multMagma(# the carrier of H, the multF of H #) as strict Subgroup of G by Lm15;

assume A c= the carrier of H ; :: thesis: the_stable_subgroup_of B is StableSubgroup of H

then gr A is Subgroup of H9 by GROUP_4:def 4;

then B c= the carrier of H9 by A2, GROUP_2:def 5;

hence the_stable_subgroup_of B is StableSubgroup of H by Def26; :: thesis: verum

end;reconsider H9 = multMagma(# the carrier of H, the multF of H #) as strict Subgroup of G by Lm15;

assume A c= the carrier of H ; :: thesis: the_stable_subgroup_of B is StableSubgroup of H

then gr A is Subgroup of H9 by GROUP_4:def 4;

then B c= the carrier of H9 by A2, GROUP_2:def 5;

hence the_stable_subgroup_of B is StableSubgroup of H by Def26; :: thesis: verum

then A c= the carrier of (the_stable_subgroup_of B) by A1;

hence the_stable_subgroup_of A = the_stable_subgroup_of B by A3, Def26; :: thesis: verum