let O be set ; :: thesis: for G being GroupWithOperators of O
for A, B being Subset of G st A c= B holds
the_stable_subgroup_of A is StableSubgroup of the_stable_subgroup_of B
let G be GroupWithOperators of O; :: thesis: for A, B being Subset of G st A c= B holds
the_stable_subgroup_of A is StableSubgroup of the_stable_subgroup_of B
let A, B be Subset of G; :: thesis: ( A c= B implies the_stable_subgroup_of A is StableSubgroup of the_stable_subgroup_of B )
assume A1: A c= B ; :: thesis: the_stable_subgroup_of A is StableSubgroup of the_stable_subgroup_of B

per cases ( A is empty or not A is empty ) ;

suppose A2: A is empty ; :: thesis: the_stable_subgroup_of A is StableSubgroup of the_stable_subgroup_of B

reconsider H1 = (1). G, H2 = (1). (the_stable_subgroup_of B) as strict StableSubgroup of G by Th11;
the carrier of H1 = {(1_ G)} by Def8
.= {(1_ (the_stable_subgroup_of B))} by Th4
.= the carrier of H2 by Def8 ;
then (1). G = (1). (the_stable_subgroup_of B) by Lm5;
hence the_stable_subgroup_of A is StableSubgroup of the_stable_subgroup_of B by A2, Lm25; :: thesis: verum

end;

suppose A3: not A is empty ; :: thesis: the_stable_subgroup_of A is StableSubgroup of the_stable_subgroup_of B

now

set D = the_stable_subset_generated_by B,the action of G;
let a be Element of G; :: thesis: ( a in the_stable_subgroup_of A implies a in the_stable_subgroup_of B )
assume a in the_stable_subgroup_of A ; :: thesis: a in the_stable_subgroup_of B
then consider F being FinSequence of the carrier of G, I being FinSequence of INT , C being Subset of G such that
A4: C = the_stable_subset_generated_by A,the action of G and
A5: len F = len I and
A6: rng F c= C and
A7: Product (F |^ I) = a by Th24;

now

let y be set ; :: thesis: ( y in C implies y in the_stable_subset_generated_by B,the action of G )
assume A8: y in C ; :: thesis: y in the_stable_subset_generated_by B,the action of G
then reconsider b = y as Element of G ;
consider F1 being FinSequence of O, x being Element of A such that
A9: (Product F1,the action of G) . x = b by A3, A4, A8, Lm31;
x in A by A3;
hence y in the_stable_subset_generated_by B,the action of G by A1, A9, Lm31; :: thesis: verum

end;

then C c= the_stable_subset_generated_by B,the action of G by TARSKI:def 3;
then rng F c= the_stable_subset_generated_by B,the action of G by A6, XBOOLE_1:1;
hence a in the_stable_subgroup_of B by A5, A7, Th24; :: thesis: verum

end;

hence the_stable_subgroup_of A is StableSubgroup of the_stable_subgroup_of B by Th13; :: thesis: verum

end;

end;