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 );

A2: now

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

end;

consider F being Function of X,REAL such that
A4: for x being set st x in X holds
S₁[x,F . x] from FUNCT_2:sch 1(A2);
deffunc H₁( Element of X) -> Element of REAL = F /. $1;
consider Min being Element of X such that
A5: 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
M = Min and
A6: card M = F . Min by A4;
A7: dom F = X by FUNCT_2:def 1;

now

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

end;

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