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 S_{1}[ 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 ) )

_{1}[ {} the carrier of F]
;

S_{1}[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

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 S

( 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 & S_{1}[B] holds

S_{1}[B \/ {x}]

A16:
Sfor B being Subset of F st x in A & B c= A & S

S

let x be Element of F; :: thesis: for B being Subset of F st x in A & B c= A & S_{1}[B] holds

S_{1}[B \/ {x}]

let B be Subset of F; :: thesis: ( x in A & B c= A & S_{1}[B] implies S_{1}[B \/ {x}] )

assume that

A5: x in A and

A6: B c= A and

A7: S_{1}[B]
; :: thesis: S_{1}[B \/ {x}]

reconsider x9 = x as Element of F ;

_{1}[B \/ {x}]
; :: thesis: verum

end;S

let B be Subset of F; :: thesis: ( x in A & B c= A & S

assume that

A5: x in A and

A6: B c= A and

A7: S

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 ) ) )end;

hence
S( 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 ) ) ;

end;

( 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 ) ) )

( 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 A8, TARSKI:def 1;

hence m <= C by A3, A5, A6, A9, TARSKI:def 1; :: thesis: verum

end;( 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 A8, TARSKI:def 1;

hence m <= C by A3, A5, A6, A9, TARSKI:def 1; :: thesis: verum

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 ) ) )

( 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 A7, A11;

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 A13, 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 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: verum

end;( 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 A7, A11;

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 A13, 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 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: verum

S

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