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 A1:
G1 c= G
; ( the Source of G1 c= the Source of G & the Target of G1 c= the Target of G )
A2:
G1 is Subgraph of G
by A1, Def24;
A3:
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
consider x,
y being
set such that A5:
[x,y] = v
by A4, 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;
A9:
the
carrier' of
G1 c= the
carrier' of
G
by A2, Def18;
A10:
x in the
carrier' of
G
by A8, A9;
A11:
x in dom the
Source of
G
by A10, FUNCT_2:def 1;
A12:
y = the
Source of
G . x
by A2, A6, A7, Def18;
thus
v in the
Source of
G
by A5, A11, A12, FUNCT_1:def 4;
verum
end;
thus
the Source of G1 c= the Source of G
by A3, TARSKI:def 3; the Target of G1 c= the Target of G
A13:
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
consider x,
y being
set such that A15:
[x,y] = v
by A14, 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;
A19:
the
carrier' of
G1 c= the
carrier' of
G
by A2, Def18;
A20:
x in the
carrier' of
G
by A18, A19;
A21:
x in dom the
Target of
G
by A20, FUNCT_2:def 1;
A22:
y = the
Target of
G . x
by A2, A16, A17, Def18;
thus
v in the
Target of
G
by A15, A21, A22, FUNCT_1:def 4;
verum
end;
thus
the Target of G1 c= the Target of G
by A13, TARSKI:def 3; verum