defpred S₁[ set ] means ( $1 <> {} implies ex m being set st
( m in $1 & ( for C being set st C in $1 holds
C c= m ) ) );
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
C c= m ) ) )
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
C c= m ) )
A4: S₁[ {} ] ;

A5: now

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

now

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

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

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

end;

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

then consider y being set such that
A9: ( y in B & x c= y ) ;
assume B \/ {x} <> {} ; :: thesis: ex m being set st
( m in B \/ {x} & ( for C being set st C in B \/ {x} holds
C c= m ) )
consider m being set such that
A10: m in B and
A11: for C being set st C in B holds
C c= m by A6, A9;
y c= m by A9, A11;
then A12: x c= m by A9, XBOOLE_1:1;
take m = m; :: thesis: ( m in B \/ {x} & ( for C being set st C in B \/ {x} holds
C c= m ) )
thus m in B \/ {x} by A10, XBOOLE_0:def 3; :: thesis: for C being set st C in B \/ {x} holds
C c= m
let C be set ; :: thesis: ( C in B \/ {x} implies C c= m )
assume C in B \/ {x} ; :: thesis: C c= m
then ( C in B or C in {x} ) by XBOOLE_0:def 3;
hence C c= m by A11, A12, 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
C c= m ) ) by A2; :: thesis: verum