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:
assume that
A1: F is finite and
A2: F <> {} and
A3: F is c=-linear ; :: thesis:
A4: S₁[ {} ] ;

A5: now :: thesis:

let x, B be set ; :: thesis:
assume that
A6: x in F and
A7: B c= F and
A8: S₁[B] ; :: thesis:

suppose A9: for y being set holds
( not y in B or not y c= x ) ; :: thesis:

assume B \/ {x} <> {} ; :: thesis:
take m = x; :: thesis:
x in {x} by TARSKI:def 1;
hence m in B \/ {x} by XBOOLE_0:def 3; :: thesis:
let C be set ; :: thesis:
assume C in B \/ {x} ; :: thesis:
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:

end;

suppose ex y being set st
( y in B & y c= x ) ; :: thesis:

then consider y being set such that
A11: y in B and
A12: y c= x ;
assume B \/ {x} <> {} ; :: thesis:
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:
thus m in B \/ {x} by A13, XBOOLE_0:def 3; :: thesis:
let C be set ; :: thesis:
assume C in B \/ {x} ; :: thesis:
then ( C in B or C in {x} ) by XBOOLE_0:def 3;
hence m c= C by A14, A15, TARSKI:def 1; :: thesis:

end;

end;

end;

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

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: