let G be _Graph; for a, b being Vertex of G st a <> b & not a,b are_adjacent holds
for S being VertexSeparator of a,b
for G2 being removeVertices of G,S
for a2, b2 being Vertex of G2 st a2 = a & b2 = b holds
(G2 .reachableFrom a2) /\ (G2 .reachableFrom b2) = {}
let a, b be Vertex of G; ( a <> b & not a,b are_adjacent implies for S being VertexSeparator of a,b
for G2 being removeVertices of G,S
for a2, b2 being Vertex of G2 st a2 = a & b2 = b holds
(G2 .reachableFrom a2) /\ (G2 .reachableFrom b2) = {} )
assume that
A1:
a <> b
and
A2:
not a,b are_adjacent
; for S being VertexSeparator of a,b
for G2 being removeVertices of G,S
for a2, b2 being Vertex of G2 st a2 = a & b2 = b holds
(G2 .reachableFrom a2) /\ (G2 .reachableFrom b2) = {}
let S be VertexSeparator of a,b; for G2 being removeVertices of G,S
for a2, b2 being Vertex of G2 st a2 = a & b2 = b holds
(G2 .reachableFrom a2) /\ (G2 .reachableFrom b2) = {}
let G2 be removeVertices of G,S; for a2, b2 being Vertex of G2 st a2 = a & b2 = b holds
(G2 .reachableFrom a2) /\ (G2 .reachableFrom b2) = {}
let a2, b2 be Vertex of G2; ( a2 = a & b2 = b implies (G2 .reachableFrom a2) /\ (G2 .reachableFrom b2) = {} )
assume that
A3:
a2 = a
and
A4:
b2 = b
; (G2 .reachableFrom a2) /\ (G2 .reachableFrom b2) = {}
set A = G2 .reachableFrom a2;
set B = G2 .reachableFrom b2;
now for x being object holds not x in (G2 .reachableFrom a2) /\ (G2 .reachableFrom b2)let x be
object ;
not x in (G2 .reachableFrom a2) /\ (G2 .reachableFrom b2)assume A5:
x in (G2 .reachableFrom a2) /\ (G2 .reachableFrom b2)
;
contradiction
x in G2 .reachableFrom a2
by A5, XBOOLE_0:def 4;
then consider W1 being
Walk of
G2 such that A6:
W1 is_Walk_from a2,
x
by GLIB_002:def 5;
x in G2 .reachableFrom b2
by A5, XBOOLE_0:def 4;
then consider rW2 being
Walk of
G2 such that A7:
rW2 is_Walk_from b2,
x
by GLIB_002:def 5;
set W2 =
rW2 .reverse() ;
set W =
W1 .append (rW2 .reverse());
rW2 .reverse() is_Walk_from x,
b2
by A7, GLIB_001:23;
then
W1 .append (rW2 .reverse()) is_Walk_from a2,
b2
by A6, GLIB_001:31;
hence
contradiction
by A1, A2, A3, A4, Def8;
verum end;
hence
(G2 .reachableFrom a2) /\ (G2 .reachableFrom b2) = {}
by XBOOLE_0:def 1; verum