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 A1:
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 A2:
v in the
Source of
G1
;
v in the Source of G
then consider x,
y being
set such that A3:
[x,y] = v
by RELAT_1:def 1;
A4:
x in dom the
Source of
G1
by A2, A3, FUNCT_1:1;
A5:
y = the
Source of
G1 . x
by A2, A3, FUNCT_1:1;
A6:
x in the
carrier' of
G1
by A4;
the
carrier' of
G1 c= the
carrier' of
G
by A1, Def18;
then
x in the
carrier' of
G
by A6;
then A7:
x in dom the
Source of
G
by FUNCT_2:def 1;
y = the
Source of
G . x
by A1, A4, A5, Def18;
hence
v in the
Source of
G
by A3, A7, FUNCT_1:def 2;
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 A8:
v in the
Target of
G1
;
v in the Target of G
then consider x,
y being
set such that A9:
[x,y] = v
by RELAT_1:def 1;
A10:
x in dom the
Target of
G1
by A8, A9, FUNCT_1:1;
A11:
y = the
Target of
G1 . x
by A8, A9, FUNCT_1:1;
A12:
x in the
carrier' of
G1
by A10;
the
carrier' of
G1 c= the
carrier' of
G
by A1, Def18;
then
x in the
carrier' of
G
by A12;
then A13:
x in dom the
Target of
G
by FUNCT_2:def 1;
y = the
Target of
G . x
by A1, A10, A11, Def18;
hence
v in the
Target of
G
by A9, A13, FUNCT_1:def 2;
verum
end;
hence
the Target of G1 c= the Target of G
by TARSKI:def 3; verum