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 that
A6: x in F and
A7: B c= F and
A8: 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 A9: 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 A10: ( C in B or C in {x} ) by XBOOLE_0:def 3;
then C,x are_c=-comparable by A3, A6, A7, ORDINAL1:def 8, TARSKI:def 1;
then ( C c= x or x c= C ) by XBOOLE_0:def 9;
hence C c= m by A9, A10, 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
A11: y in B and
A12: 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
A13: m in B and
A14: for C being set st C in B holds
C c= m by A8, A11;
y c= m by A11, A14;
then A15: x c= m by A12, 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 A13, 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 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
C c= m ) ) by A2; :: thesis: verum