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 A1: ( G1 is StableSubgroup of G2 & G2 is StableSubgroup of G3 ) ; :: thesis: G1 is StableSubgroup of G3
then A2: ( G1 is Subgroup of G2 & G2 is Subgroup of G3 ) by Def7;
then A3: G1 is Subgroup of G3 by GROUP_2:65;

now

let o be Element of O; :: thesis: G1 ^ o = (G3 ^ o) | the carrier of G1
A4: the carrier of G1 c= the carrier of G2 by A2, 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 A1, Def7
.= (G3 ^ o) | (the carrier of G2 /\ the carrier of G1) by RELAT_1:100 ;
hence G1 ^ o = (G3 ^ o) | the carrier of G1 by A4, XBOOLE_1:28; :: thesis: verum

end;

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