let V be set ; for G being Graph
for v1, v2 being Element of G
for p being oriented Chain of G st p is_orientedpath_of v1,v2,V & v1 <> v2 holds
v1 in V
let G be Graph; for v1, v2 being Element of G
for p being oriented Chain of G st p is_orientedpath_of v1,v2,V & v1 <> v2 holds
v1 in V
let v1, v2 be Element of G; for p being oriented Chain of G st p is_orientedpath_of v1,v2,V & v1 <> v2 holds
v1 in V
let p be oriented Chain of G; ( p is_orientedpath_of v1,v2,V & v1 <> v2 implies v1 in V )
assume that
A1:
p is_orientedpath_of v1,v2,V
and
A2:
v1 <> v2
; v1 in V
p is_orientedpath_of v1,v2
by A1;
then A3:
v1 in vertices p
by Th27;
not v1 in {v2}
by A2, TARSKI:def 1;
then A4:
v1 in (vertices p) \ {v2}
by A3, XBOOLE_0:def 5;
(vertices p) \ {v2} c= V
by A1;
hence
v1 in V
by A4; verum