let G1, G2, G3 be Group; ( 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
; 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; verum