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 )

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
defpred S₁[ set ] means ( not $1 is empty implies ex_sup_of $1,L );
A2: X is finite ;
A3: S₁[ {} ] ;
A4: 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
A5: ( x in X & Y c= X ) and
A6: ( not Y is empty implies ex_sup_of Y,L ) ; :: thesis: S₁[Y \/ {x}]
assume not Y \/ {x} is empty ; :: thesis: ex_sup_of Y \/ {x},L
reconsider z = x as Element of L by A5;

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 A7: 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 ) )
A8: ex_sup_of {("\/" Y,L),z},L by A1, Th20;
then ( Y is_<=_than "\/" Y,L & "\/" Y,L <= a & z <= a ) by A6, A7, Def9, Th18;
then ( Y is_<=_than a & {x} is_<=_than a ) by Th7, Th11;
hence A9: Y \/ {x} is_<=_than a by 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} & z in {x} ) by TARSKI:def 1, XBOOLE_1:7;
then ( Y is_<=_than b & z in Y \/ {x} ) by A10, Th9, XBOOLE_0:def 3;
then ( "\/" Y,L <= b & z <= b ) by A6, A7, A10, Def9, LATTICE3:def 9;
hence b >= a by A8, 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
A11: Y \/ {x} is_<=_than c and
A12: for b being Element of L st Y \/ {x} is_<=_than b holds
b >= c ; :: thesis: c = a
A13: a >= c by A9, A12;
( Y c= Y \/ {x} & z in {x} ) by TARSKI:def 1, XBOOLE_1:7;
then ( Y is_<=_than c & z in Y \/ {x} ) by A11, Th9, XBOOLE_0:def 3;
then ( "\/" Y,L <= c & z <= c ) by A6, A7, A11, Def9, LATTICE3:def 9;
then c >= a by A8, Th18;
hence c = a by A13, ORDERS_2:25; :: thesis: verum

end;

end;

end;

end;

S₁[X] from FINSET_1:sch 2(A2, A3, A4);
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