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

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 )
;

end;

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 Lm4;

hence the_stable_subgroup_of A is StableSubgroup of the_stable_subgroup_of B by A2, Lm24; :: thesis: verum

end;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 Lm4;

hence the_stable_subgroup_of A is StableSubgroup of the_stable_subgroup_of B by A2, Lm24; :: thesis: verum

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

end;

now :: thesis: for a being Element of G st a in the_stable_subgroup_of A holds

a in the_stable_subgroup_of B

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

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;

then rng F c= the_stable_subset_generated_by (B, the action of G) by A6;

hence a in the_stable_subgroup_of B by A5, A7, Th24; :: thesis: verum

end;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 :: thesis: for y being object st y in C holds

y in the_stable_subset_generated_by (B, the action of G)

then
C c= the_stable_subset_generated_by (B, the action of G)
;y in the_stable_subset_generated_by (B, the action of G)

let y be object ; :: 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, Lm30;

x in A by A3;

hence y in the_stable_subset_generated_by (B, the action of G) by A1, A9, Lm30; :: thesis: verum

end;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, Lm30;

x in A by A3;

hence y in the_stable_subset_generated_by (B, the action of G) by A1, A9, Lm30; :: thesis: verum

then rng F c= the_stable_subset_generated_by (B, the action of G) by A6;

hence a in the_stable_subgroup_of B by A5, A7, Th24; :: thesis: verum