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;
A4: now :: thesis: for o being Element of O holds G1 ^ o = (G3 ^ o) | the carrier of G1
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;
G2 is Subgroup of G3 by A2, Def7;
then G1 is Subgroup of G3 by A3, GROUP_2:56;
hence G1 is StableSubgroup of G3 by A4, Def7; :: thesis: verum