let G1, G2, G3 be addGroup; :: 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 addF 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, DefA5;
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, DefA5;
then A5: the carrier of G1 c= the carrier of G3 by A3;
the addF of G1 = the addF of G2 || the carrier of G1 by A1, DefA5
.= ( the addF of G3 || the carrier of G2) || the carrier of G1 by A2, DefA5
.= the addF of G3 || the carrier of G1 by A4, FUNCT_1:51 ;
hence G1 is Subgroup of G3 by A5, DefA5; :: thesis: verum