let G be _Graph; for v1, v2 being Vertex of G st not v1 in G .reachableFrom v2 holds
G .reachableFrom v1 misses G .reachableFrom v2
let v1, v2 be Vertex of G; ( not v1 in G .reachableFrom v2 implies G .reachableFrom v1 misses G .reachableFrom v2 )
assume A1:
not v1 in G .reachableFrom v2
; G .reachableFrom v1 misses G .reachableFrom v2
assume
not G .reachableFrom v1 misses G .reachableFrom v2
; contradiction
then
(G .reachableFrom v1) /\ (G .reachableFrom v2) <> {}
by XBOOLE_0:def 7;
then consider w being object such that
A2:
w in (G .reachableFrom v1) /\ (G .reachableFrom v2)
by XBOOLE_0:def 1;
A3:
( w in G .reachableFrom v1 & w in G .reachableFrom v2 )
by A2, XBOOLE_0:def 4;
then consider W1 being Walk of G such that
A4:
W1 is_Walk_from v1,w
by GLIB_002:def 5;
consider W2 being Walk of G such that
A5:
W2 is_Walk_from v2,w
by A3, GLIB_002:def 5;
W1 .reverse() is_Walk_from w,v1
by A4, GLIB_001:23;
then
W2 .append (W1 .reverse()) is_Walk_from v2,v1
by A5, GLIB_001:31;
hence
contradiction
by A1, GLIB_002:def 5; verum