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;

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)

hence
(G2 .reachableFrom a2) /\ (G2 .reachableFrom b2) = {}
by XBOOLE_0:def 1; :: thesis: verumlet 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;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