let G, G1 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
;
for v being object st v in the Source of G1 holds
v in the Source of G
proof
let v be
object ;
( 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
object 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
; the Target of G1 c= the Target of G
let v be object ; TARSKI:def 3 ( not v in the Target of G1 or 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 object 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