let G1, G2, G3 be Graph; ( G1 c= G2 & G2 c= G3 implies G1 c= G3 )
assume that
A1:
G1 c= G2
and
A2:
G2 c= G3
; G1 c= G3
A3:
G1 is Subgraph of G2
by A1;
A4:
G2 is Subgraph of G3
by A2;
A5:
the carrier of G1 c= the carrier of G2
by A3, Def18;
the carrier of G2 c= the carrier of G3
by A4, Def18;
then A6:
the carrier of G1 c= the carrier of G3
by A5;
A7:
the carrier' of G1 c= the carrier' of G2
by A3, Def18;
the carrier' of G2 c= the carrier' of G3
by A4, Def18;
then A8:
the carrier' of G1 c= the carrier' of G3
by A7;
for v being set st v in the carrier' of G1 holds
( the Source of G1 . v = the Source of G3 . v & the Target of G1 . v = the Target of G3 . v & the Source of G3 . v in the carrier of G1 & the Target of G3 . v in the carrier of G1 )
proof
let v be
set ;
( v in the carrier' of G1 implies ( the Source of G1 . v = the Source of G3 . v & the Target of G1 . v = the Target of G3 . v & the Source of G3 . v in the carrier of G1 & the Target of G3 . v in the carrier of G1 ) )
assume A9:
v in the
carrier' of
G1
;
( the Source of G1 . v = the Source of G3 . v & the Target of G1 . v = the Target of G3 . v & the Source of G3 . v in the carrier of G1 & the Target of G3 . v in the carrier of G1 )
hence A10: the
Source of
G1 . v =
the
Source of
G2 . v
by A3, Def18
.=
the
Source of
G3 . v
by A4, A7, A9, Def18
;
( the Target of G1 . v = the Target of G3 . v & the Source of G3 . v in the carrier of G1 & the Target of G3 . v in the carrier of G1 )
thus A11: the
Target of
G1 . v =
the
Target of
G2 . v
by A3, A9, Def18
.=
the
Target of
G3 . v
by A4, A7, A9, Def18
;
( the Source of G3 . v in the carrier of G1 & the Target of G3 . v in the carrier of G1 )
v in dom the
Source of
G1
by A9, FUNCT_2:def 1;
then
the
Source of
G1 . v in rng the
Source of
G1
by FUNCT_1:def 3;
hence
the
Source of
G3 . v in the
carrier of
G1
by A10;
the Target of G3 . v in the carrier of G1
v in dom the
Target of
G1
by A9, FUNCT_2:def 1;
then
the
Target of
G1 . v in rng the
Target of
G1
by FUNCT_1:def 3;
hence
the
Target of
G3 . v in the
carrier of
G1
by A11;
verum
end;
then
G1 is Subgraph of G3
by A6, A8, Def18;
hence
G1 c= G3
; verum