let G be finite _Graph; :: thesis: for a, b being Vertex of G ex S being VertexSeparator of a,b st S is minimal
let a, b be Vertex of G; :: thesis: ex S being VertexSeparator of a,b st S is minimal
set X = { S where S is VertexSeparator of a,b : verum } ;
consider s being VertexSeparator of a,b;
A1: s in { S where S is VertexSeparator of a,b : verum } ;

now

let x be set ; :: thesis: ( x in { S where S is VertexSeparator of a,b : verum } implies x in bool (the_Vertices_of G) )
assume x in { S where S is VertexSeparator of a,b : verum } ; :: thesis: x in bool (the_Vertices_of G)
then ex y being VertexSeparator of a,b st x = y ;
hence x in bool (the_Vertices_of G) ; :: thesis: verum

end;

then { S where S is VertexSeparator of a,b : verum } c= bool (the_Vertices_of G) by TARSKI:def 3;
then reconsider X = { S where S is VertexSeparator of a,b : verum } as non empty finite set by A1;
defpred S₁[ set , set ] means ex p being VertexSeparator of a,b st
( $1 = p & $2 = card p );

A3: now

let x be set ; :: thesis: ( x in X implies ex y being set st
( y in REAL & S₁[x,y] ) )
assume A4: x in X ; :: thesis: ex y being set st
( y in REAL & S₁[x,y] )
consider Y being VertexSeparator of a,b such that
A5: Y = x by A4;
card Y is Element of NAT ;
hence ex y being set st
( y in REAL & S₁[x,y] ) by A5; :: thesis: verum

end;

consider F being Function of X,REAL such that
A6: for x being set st x in X holds
S₁[x,F . x] from FUNCT_2:sch 1(A3);
A7: dom F = X by FUNCT_2:def 1;
deffunc H₁( Element of X) -> Element of REAL = F /. $1;
consider Min being Element of X such that
A8: for N being Element of X holds H₁(Min) <= H₁(N) from GRAPH_5:sch 2();
consider M being VertexSeparator of a,b such that
A9: ( M = Min & card M = F . Min ) by A6;

now

assume not M is minimal ; :: thesis: contradiction
then consider T being Subset of M such that
A10: ( T <> M & T is VertexSeparator of a,b ) by Def9;
T in X by A10;
then reconsider T2 = T as Element of X ;
consider Tp being VertexSeparator of a,b such that
A11: ( Tp = T2 & card Tp = F . T2 ) by A6;
Tp in dom F by A7;
then F /. Tp = F . Tp by PARTFUN1:def 8;
then A12: card M <= card T by A8, A9, A11;
A13: card T <= card M by NAT_1:44;
card T <> card M by A10, TRIANG_1:3;
hence contradiction by A12, A13, XXREAL_0:1; :: thesis: verum

end;

hence ex S being VertexSeparator of a,b st S is minimal ; :: thesis: verum