let F be non empty Poset; :: thesis: for A being Subset of F st A is finite & A <> {} & ( for B, C being Element of F st B in A & C in A & not B <= C holds
C <= B ) holds
ex m being Element of F st
( m in A & ( for C being Element of F st C in A holds
m <= C ) )

defpred S1[ 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: ( A is finite & A <> {} & ( for B, C being Element of F st B in A & C in A & not B <= C holds
C <= B ) implies ex m being Element of F st
( m in A & ( for C being Element of F st C in A holds
m <= C ) ) )

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: ex m being Element of F st
( m in A & ( for C being Element of F st C in A holds
m <= C ) )

A4: now :: thesis: for x being Element of F
for B being Subset of F st x in A & B c= A & S1[B] holds
S1[B \/ {x}]
let x be Element of F; :: thesis: for B being Subset of F st x in A & B c= A & S1[B] holds
S1[B \/ {x}]

let B be Subset of F; :: thesis: ( x in A & B c= A & S1[B] implies S1[B \/ {x}] )
assume that
A5: x in A and
A6: B c= A and
A7: S1[B] ; :: thesis: S1[B \/ {x}]
reconsider x9 = x as Element of F ;
now :: thesis: ( B \/ {x} <> {} implies ex m being Element of F st
( m in B \/ {x} & ( for C being Element of F st C in B \/ {x} holds
m <= C ) ) )
per cases ( for y being Element of F holds
( not y in B or not y <= x9 ) or ex y being Element of F st
( y in B & y <= x9 ) )
;
suppose A8: for y being Element of F holds
( not y in B or not y <= x9 ) ; :: thesis: ( B \/ {x} <> {} implies ex m being Element of F st
( m in B \/ {x} & ( for C being Element of F st C in B \/ {x} holds
m <= C ) ) )

assume B \/ {x} <> {} ; :: thesis: ex m being Element of F st
( m in B \/ {x} & ( for C being Element of F st C in B \/ {x} holds
m <= C ) )

take m = x9; :: thesis: ( m in B \/ {x} & ( for C being Element of F st C in B \/ {x} holds
m <= C ) )

x in {x} by TARSKI:def 1;
hence m in B \/ {x} by XBOOLE_0:def 3; :: thesis: for C being Element of F st C in B \/ {x} holds
m <= C

let C be Element of F; :: thesis: ( C in B \/ {x} implies m <= C )
assume C in B \/ {x} ; :: thesis: m <= C
then A9: ( C in B or C in {x} ) by XBOOLE_0:def 3;
then ( not C <= x9 or C = x ) by ;
hence m <= C by ; :: thesis: verum
end;
suppose A10: ex y being Element of F st
( y in B & y <= x9 ) ; :: thesis: ( B \/ {x} <> {} implies ex m being Element of F st
( m in B \/ {x} & ( for C being Element of F st C in B \/ {x} holds
m <= C ) ) )

assume B \/ {x} <> {} ; :: thesis: ex m being Element of F st
( m in B \/ {x} & ( for C being Element of F st C in B \/ {x} holds
m <= C ) )

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 ;
take m = m; :: thesis: ( m in B \/ {x} & ( for C being Element of F st C in B \/ {x} holds
m <= C ) )

thus m in B \/ {x} by ; :: thesis: for C being Element of F st C in B \/ {x} holds
m <= C

let C be Element of F; :: thesis: ( C in B \/ {x} implies m <= C )
assume C in B \/ {x} ; :: thesis: m <= C
then A15: ( C in B or C in {x} ) by XBOOLE_0:def 3;
m <= y by ;
then m <= x9 by ;
hence m <= C by ; :: thesis: verum
end;
end;
end;
hence S1[B \/ {x}] ; :: thesis: verum
end;
A16: S1[ {} the carrier of F] ;
S1[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: verum