let G1, G be Graph; ( G1 c= G implies ( the Source of G1 c= the Source of G & the Target of G1 c= the Target of G ) )
assume
G1 c= G
; ( the Source of G1 c= the Source of G & the Target of G1 c= the Target of G )
then A2:
G1 is Subgraph of G
by Def24;
for v being set st v in the Source of G1 holds
v in the Source of G
proof
let v be
set ;
( v in the Source of G1 implies v in the Source of G )
assume A4:
v in the
Source of
G1
;
v in the Source of G
then consider x,
y being
set such that A5:
[x,y] = v
by RELAT_1:def 1;
A6:
x in dom the
Source of
G1
by A4, A5, FUNCT_1:8;
A7:
y = the
Source of
G1 . x
by A4, A5, FUNCT_1:8;
A8:
x in the
carrier' of
G1
by A6;
the
carrier' of
G1 c= the
carrier' of
G
by A2, Def18;
then
x in the
carrier' of
G
by A8;
then A11:
x in dom the
Source of
G
by FUNCT_2:def 1;
y = the
Source of
G . x
by A2, A6, A7, Def18;
hence
v in the
Source of
G
by A5, A11, FUNCT_1:def 4;
verum
end;
hence
the Source of G1 c= the Source of G
by TARSKI:def 3; the Target of G1 c= the Target of G
for v being set st v in the Target of G1 holds
v in the Target of G
proof
let v be
set ;
( v in the Target of G1 implies v in the Target of G )
assume A14:
v in the
Target of
G1
;
v in the Target of G
then consider x,
y being
set such that A15:
[x,y] = v
by RELAT_1:def 1;
A16:
x in dom the
Target of
G1
by A14, A15, FUNCT_1:8;
A17:
y = the
Target of
G1 . x
by A14, A15, FUNCT_1:8;
A18:
x in the
carrier' of
G1
by A16;
the
carrier' of
G1 c= the
carrier' of
G
by A2, Def18;
then
x in the
carrier' of
G
by A18;
then A21:
x in dom the
Target of
G
by FUNCT_2:def 1;
y = the
Target of
G . x
by A2, A16, A17, Def18;
hence
v in the
Target of
G
by A15, A21, FUNCT_1:def 4;
verum
end;
hence
the Target of G1 c= the Target of G
by TARSKI:def 3; verum