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, Def24;
A4:
G2 is Subgraph of G3
by A2, Def24;
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 A7:
the carrier of G1 c= the carrier of G3
by A5, XBOOLE_1:1;
A8:
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 A10:
the carrier' of G1 c= the carrier' of G3
by A8, XBOOLE_1:1;
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 A12:
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 A13: the
Source of
G1 . v =
the
Source of
G2 . v
by A3, Def18
.=
the
Source of
G3 . v
by A4, A8, A12, 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 A14: the
Target of
G1 . v =
the
Target of
G2 . v
by A3, A12, Def18
.=
the
Target of
G3 . v
by A4, A8, A12, 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 A12, FUNCT_2:def 1;
then
the
Source of
G1 . v in rng the
Source of
G1
by FUNCT_1:def 5;
hence
the
Source of
G3 . v in the
carrier of
G1
by A13;
the Target of G3 . v in the carrier of G1
v in dom the
Target of
G1
by A12, FUNCT_2:def 1;
then
the
Target of
G1 . v in rng the
Target of
G1
by FUNCT_1:def 5;
hence
the
Target of
G3 . v in the
carrier of
G1
by A14;
verum
end;
then
G1 is Subgraph of G3
by A7, A10, Def18;
hence
G1 c= G3
by Def24; verum