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
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
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;
the carrier of (gr A) c= the carrier of (the_stable_subgroup_of B) by A2, Def26;
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