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 ;
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 ;
G1 ^ o = (G2 ^ o) | the carrier of G1 by
.= ((G3 ^ o) | the carrier of G2) | the carrier of G1 by
.= (G3 ^ o) | ( the carrier of G2 /\ the carrier of G1) by RELAT_1:71 ;
hence G1 ^ o = (G3 ^ o) | the carrier of G1 by ; :: thesis: verum
end;
G2 is Subgroup of G3 by ;
then G1 is Subgroup of G3 by ;
hence G1 is StableSubgroup of G3 by ; :: thesis: verum