let L be non empty Poset; :: thesis: ( L is with_suprema iff for X being non empty finite Subset of L holds ex_sup_of X,L )

hereby :: thesis: ( ( for X being non empty finite Subset of L holds ex_sup_of X,L ) implies L is with_suprema )

defpred S₁[ set ] means ( not $1 is empty implies ex_sup_of $1,L );
assume A1: L is with_suprema ; :: thesis: for X being non empty finite Subset of L holds ex_sup_of X,L
let X be non empty finite Subset of L; :: thesis: ex_sup_of X,L
A2: for x, Y being set st x in X & Y c= X & S₁[Y] holds
S₁[Y \/ {x}]

proof

let x, Y be set ; :: thesis: ( x in X & Y c= X & S₁[Y] implies S₁[Y \/ {x}] )
assume that
A3: x in X and
Y c= X and
A4: ( not Y is empty implies ex_sup_of Y,L ) ; :: thesis: S₁[Y \/ {x}]
reconsider z = x as Element of L by A3;
assume not Y \/ {x} is empty ; :: thesis: ex_sup_of Y \/ {x},L

per cases ( Y is empty or not Y is empty ) ;

suppose Y is empty ; :: thesis: ex_sup_of Y \/ {x},L

then Y \/ {x} = {z} ;
hence ex_sup_of Y \/ {x},L by Th38; :: thesis: verum

end;

suppose A5: not Y is empty ; :: thesis: ex_sup_of Y \/ {x},L

thus ex_sup_of Y \/ {x},L :: thesis: verum

proof

take a = ("\/" (Y,L)) "\/" z; :: according to YELLOW_0:def 7 :: thesis: ( Y \/ {x} is_<=_than a & ( for b being Element of L st Y \/ {x} is_<=_than b holds
b >= a ) & ( for c being Element of L st Y \/ {x} is_<=_than c & ( for b being Element of L st Y \/ {x} is_<=_than b holds
b >= c ) holds
c = a ) )
A6: Y is_<=_than "\/" (Y,L) by A4, Def9;
A7: ex_sup_of {("\/" (Y,L)),z},L by A1, Th20;
then z <= a by Th18;
then A8: {x} is_<=_than a by Th7;
"\/" (Y,L) <= a by A7, Th18;
then A9: Y is_<=_than a by A6, Th11;
hence Y \/ {x} is_<=_than a by A8, Th10; :: thesis: ( ( for b being Element of L st Y \/ {x} is_<=_than b holds
b >= a ) & ( for c being Element of L st Y \/ {x} is_<=_than c & ( for b being Element of L st Y \/ {x} is_<=_than b holds
b >= c ) holds
c = a ) )

hereby :: thesis: for c being Element of L st Y \/ {x} is_<=_than c & ( for b being Element of L st Y \/ {x} is_<=_than b holds
b >= c ) holds
c = a

let b be Element of L; :: thesis: ( Y \/ {x} is_<=_than b implies b >= a )
assume A10: Y \/ {x} is_<=_than b ; :: thesis: b >= a
Y c= Y \/ {x} by XBOOLE_1:7;
then Y is_<=_than b by A10;
then A11: "\/" (Y,L) <= b by A4, A5, Def9;
z in {x} by TARSKI:def 1;
then z in Y \/ {x} by XBOOLE_0:def 3;
then z <= b by A10;
hence b >= a by A7, A11, Th18; :: thesis: verum

end;

let c be Element of L; :: thesis: ( Y \/ {x} is_<=_than c & ( for b being Element of L st Y \/ {x} is_<=_than b holds
b >= c ) implies c = a )
assume that
A12: Y \/ {x} is_<=_than c and
A13: for b being Element of L st Y \/ {x} is_<=_than b holds
b >= c ; :: thesis: c = a
Y c= Y \/ {x} by XBOOLE_1:7;
then Y is_<=_than c by A12;
then A14: "\/" (Y,L) <= c by A4, A5, Def9;
z in {x} by TARSKI:def 1;
then z in Y \/ {x} by XBOOLE_0:def 3;
then z <= c by A12;
then A15: c >= a by A7, A14, Th18;
a >= c by A9, A8, A13, Th10;
hence c = a by A15, ORDERS_2:2; :: thesis: verum

end;

end;

end;

end;

A16: S₁[ {} ] ;
A17: X is finite ;
S₁[X] from FINSET_1:sch 2(A17, A16, A2);
hence ex_sup_of X,L ; :: thesis: verum

end;

assume for X being non empty finite Subset of L holds ex_sup_of X,L ; :: thesis: L is with_suprema
then for a, b being Element of L holds ex_sup_of {a,b},L ;
hence L is with_suprema by Th20; :: thesis: verum