let G1, G2, G3 be Group; :: thesis: ( G1 is Subgroup of G2 & G2 is Subgroup of G3 implies G1 is Subgroup of G3 )
assume that
A1: G1 is Subgroup of G2 and
A2: G2 is Subgroup of G3 ; :: thesis: G1 is Subgroup of G3
set h = the multF of G3;
set C = the carrier of G3;
set B = the carrier of G2;
set A = the carrier of G1;
A3: the carrier of G1 c= the carrier of G2 by A1, Def5;
then A4: [: the carrier of G1, the carrier of G1:] c= [: the carrier of G2, the carrier of G2:] by ZFMISC_1:96;
the carrier of G2 c= the carrier of G3 by A2, Def5;
then A5: the carrier of G1 c= the carrier of G3 by A3;
the multF of G1 = the multF of G2 || the carrier of G1 by A1, Def5
.= ( the multF of G3 || the carrier of G2) || the carrier of G1 by A2, Def5
.= the multF of G3 || the carrier of G1 by A4, FUNCT_1:51 ;
hence G1 is Subgroup of G3 by A5, Def5; :: thesis: verum