let G be _Graph; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( a2 = a & b2 = b implies (G2 .reachableFrom a2) /\ (G2 .reachableFrom b2) = {} )
assume that
A3: a2 = a and
A4: b2 = b ; :: thesis: (G2 .reachableFrom a2) /\ (G2 .reachableFrom b2) = {}
set A = G2 .reachableFrom a2;
set B = G2 .reachableFrom b2;

now :: thesis: for x being object holds not x in (G2 .reachableFrom a2) /\ (G2 .reachableFrom b2)

let x be object ; :: thesis: not x in (G2 .reachableFrom a2) /\ (G2 .reachableFrom b2)
assume A5: x in (G2 .reachableFrom a2) /\ (G2 .reachableFrom b2) ; :: thesis: 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; :: thesis: verum

end;

hence (G2 .reachableFrom a2) /\ (G2 .reachableFrom b2) = {} by XBOOLE_0:def 1; :: thesis: verum