let O be set ; :: thesis: for G1, G2, G3 being GroupWithOperators of O st G1 is StableSubgroup of G2 & G2 is StableSubgroup of G3 holds

G1 is StableSubgroup of G3

let G1, G2, G3 be GroupWithOperators of O; :: thesis: ( G1 is StableSubgroup of G2 & G2 is StableSubgroup of G3 implies G1 is StableSubgroup of G3 )

assume that

A1: G1 is StableSubgroup of G2 and

A2: G2 is StableSubgroup of G3 ; :: thesis: G1 is StableSubgroup of G3

A3: G1 is Subgroup of G2 by A1, Def7;

then G1 is Subgroup of G3 by A3, GROUP_2:56;

hence G1 is StableSubgroup of G3 by A4, Def7; :: thesis: verum

G1 is StableSubgroup of G3

let G1, G2, G3 be GroupWithOperators of O; :: thesis: ( G1 is StableSubgroup of G2 & G2 is StableSubgroup of G3 implies G1 is StableSubgroup of G3 )

assume that

A1: G1 is StableSubgroup of G2 and

A2: G2 is StableSubgroup of G3 ; :: thesis: G1 is StableSubgroup of G3

A3: G1 is Subgroup of G2 by A1, Def7;

A4: now :: thesis: for o being Element of O holds G1 ^ o = (G3 ^ o) | the carrier of G1

G2 is Subgroup of G3
by A2, Def7;let o be Element of O; :: thesis: G1 ^ o = (G3 ^ o) | the carrier of G1

A5: the carrier of G1 c= the carrier of G2 by A3, GROUP_2:def 5;

G1 ^ o = (G2 ^ o) | the carrier of G1 by A1, Def7

.= ((G3 ^ o) | the carrier of G2) | the carrier of G1 by A2, Def7

.= (G3 ^ o) | ( the carrier of G2 /\ the carrier of G1) by RELAT_1:71 ;

hence G1 ^ o = (G3 ^ o) | the carrier of G1 by A5, XBOOLE_1:28; :: thesis: verum

end;A5: the carrier of G1 c= the carrier of G2 by A3, GROUP_2:def 5;

G1 ^ o = (G2 ^ o) | the carrier of G1 by A1, Def7

.= ((G3 ^ o) | the carrier of G2) | the carrier of G1 by A2, Def7

.= (G3 ^ o) | ( the carrier of G2 /\ the carrier of G1) by RELAT_1:71 ;

hence G1 ^ o = (G3 ^ o) | the carrier of G1 by A5, XBOOLE_1:28; :: thesis: verum

then G1 is Subgroup of G3 by A3, GROUP_2:56;

hence G1 is StableSubgroup of G3 by A4, Def7; :: thesis: verum