defpred S₁[ set ] means ( $1 <> {} implies ex m being set st
( m in $1 & ( for C being set st C in $1 holds
m c= C ) ) );
let F be set ; :: thesis: ( F is finite & F <> {} & F is c=-linear implies ex m being set st
( m in F & ( for C being set st C in F holds
m c= C ) ) )
assume that
A1: F is finite and
A2: F <> {} and
A3: F is c=-linear ; :: thesis: ex m being set st
( m in F & ( for C being set st C in F holds
m c= C ) )
A4: S₁[ {} ] ;

A5: now :: thesis: for x, B being set st x in F & B c= F & S₁[B] holds
S₁[B \/ {x}]

let x, B be set ; :: thesis: ( x in F & B c= F & S₁[B] implies S₁[B \/ {x}] )
assume that
A6: x in F and
A7: B c= F and
A8: S₁[B] ; :: thesis: S₁[B \/ {x}]

now :: thesis: ( B \/ {x} <> {} implies ex m being set st
( m in B \/ {x} & ( for C being set st C in B \/ {x} holds
m c= C ) ) )

per cases ( for y being set holds
( not y in B or not y c= x ) or ex y being set st
( y in B & y c= x ) ) ;

suppose A9: for y being set holds
( not y in B or not y c= x ) ; :: thesis: ( B \/ {x} <> {} implies ex m being set st
( m in B \/ {x} & ( for C being set st C in B \/ {x} holds
m c= C ) ) )

assume B \/ {x} <> {} ; :: thesis: ex m being set st
( m in B \/ {x} & ( for C being set st C in B \/ {x} holds
m c= C ) )
take m = x; :: thesis: ( m in B \/ {x} & ( for C being set st C in B \/ {x} holds
m c= C ) )
x in {x} by TARSKI:def 1;
hence m in B \/ {x} by XBOOLE_0:def 3; :: thesis: for C being set st C in B \/ {x} holds
m c= C
let C be set ; :: thesis: ( C in B \/ {x} implies m c= C )
assume C in B \/ {x} ; :: thesis: m c= C
then A10: ( C in B or C in {x} ) by XBOOLE_0:def 3;
then C,x are_c=-comparable by A3, A6, A7, TARSKI:def 1;
then ( C c= x or x c= C ) ;
hence m c= C by A9, A10, TARSKI:def 1; :: thesis: verum

end;

suppose ex y being set st
( y in B & y c= x ) ; :: thesis: ( B \/ {x} <> {} implies ex m being set st
( m in B \/ {x} & ( for C being set st C in B \/ {x} holds
m c= C ) ) )

then consider y being set such that
A11: y in B and
A12: y c= x ;
assume B \/ {x} <> {} ; :: thesis: ex m being set st
( m in B \/ {x} & ( for C being set st C in B \/ {x} holds
m c= C ) )
consider m being set such that
A13: m in B and
A14: for C being set st C in B holds
m c= C by A8, A11;
m c= y by A11, A14;
then A15: m c= x by A12;
take m = m; :: thesis: ( m in B \/ {x} & ( for C being set st C in B \/ {x} holds
m c= C ) )
thus m in B \/ {x} by A13, XBOOLE_0:def 3; :: thesis: for C being set st C in B \/ {x} holds
m c= C
let C be set ; :: thesis: ( C in B \/ {x} implies m c= C )
assume C in B \/ {x} ; :: thesis: m c= C
then ( C in B or C in {x} ) by XBOOLE_0:def 3;
hence m c= C by A14, A15, TARSKI:def 1; :: thesis: verum

end;

end;

end;

hence S₁[B \/ {x}] ; :: thesis: verum

end;

S₁[F] from FINSET_1:sch 2(A1, A4, A5);
hence ex m being set st
( m in F & ( for C being set st C in F holds
m c= C ) ) by A2; :: thesis: verum