let F be non empty Poset; :: thesis:
defpred S₁[ set ] means ( $1 <> {} implies ex m being Element of F st
( m in $1 & ( for C being Element of F st C in $1 holds
m <= C ) ) );
let A be Subset of F; :: thesis:
assume that
A1: A is finite and
A2: A <> {} and
A3: for B, C being Element of F st B in A & C in A & not B <= C holds
C <= B ; :: thesis:

A4: now :: thesis:

let x be Element of F; :: thesis:
let B be Subset of F; :: thesis:
assume that
A5: x in A and
A6: B c= A and
A7: S₁[B] ; :: thesis:
reconsider x9 = x as Element of F ;

now :: thesis:

per cases ;

suppose A8: for y being Element of F holds
( not y in B or not y <= x9 ) ; :: thesis:

assume B \/ {x} <> {} ; :: thesis:
take m = x9; :: thesis:
x in {x} by TARSKI:def 1;
hence m in B \/ {x} by XBOOLE_0:def 3; :: thesis:
let C be Element of F; :: thesis:
assume C in B \/ {x} ; :: thesis:
then A9: ( C in B or C in {x} ) by XBOOLE_0:def 3;
then ( not C <= x9 or C = x ) by A8, TARSKI:def 1;
hence m <= C by A3, A5, A6, A9, TARSKI:def 1; :: thesis:

end;

suppose A10: ex y being Element of F st
( y in B & y <= x9 ) ; :: thesis:

assume B \/ {x} <> {} ; :: thesis:
consider y being Element of F such that
A11: y in B and
A12: y <= x9 by A10;
consider m being Element of F such that
A13: m in B and
A14: for C being Element of F st C in B holds
m <= C by A7, A11;
take m = m; :: thesis:
thus m in B \/ {x} by A13, XBOOLE_0:def 3; :: thesis:
let C be Element of F; :: thesis:
assume C in B \/ {x} ; :: thesis:
then A15: ( C in B or C in {x} ) by XBOOLE_0:def 3;
m <= y by A11, A14;
then m <= x9 by A12, ORDERS_2:3;
hence m <= C by A14, A15, TARSKI:def 1; :: thesis:

end;

end;

end;

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

end;

A16: S₁[ {} the carrier of F] ;
S₁[A] from PRE_POLY:sch 2(A1, A16, A4);
hence ex m being Element of F st
( m in A & ( for C being Element of F st C in A holds
m <= C ) ) by A2; :: thesis: