let L be non empty Poset; ( L is with_suprema iff for X being non empty finite Subset of L holds ex_sup_of X,L )
hereby ( ( for X being non empty finite Subset of L holds ex_sup_of X,L ) implies L is with_suprema )
defpred S1[
set ]
means ( not $1 is
empty implies
ex_sup_of $1,
L );
assume A1:
L is
with_suprema
;
for X being non empty finite Subset of L holds ex_sup_of X,Llet X be non
empty finite Subset of
L;
ex_sup_of X,LA2:
for
x,
Y being
set st
x in X &
Y c= X &
S1[
Y] holds
S1[
Y \/ {x}]
proof
let x,
Y be
set ;
( x in X & Y c= X & S1[Y] implies S1[Y \/ {x}] )
assume that A3:
x in X
and
Y c= X
and A4:
( not
Y is
empty implies
ex_sup_of Y,
L )
;
S1[Y \/ {x}]
reconsider z =
x as
Element of
L by A3;
assume
not
Y \/ {x} is
empty
;
ex_sup_of Y \/ {x},L
per cases
( Y is empty or not Y is empty )
;
suppose A5:
not
Y is
empty
;
ex_sup_of Y \/ {x},Lthus
ex_sup_of Y \/ {x},
L
verumproof
take a =
("\/" (Y,L)) "\/" z;
YELLOW_0:def 7 ( 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;
( ( 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 ) )
let c be
Element of
L;
( 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
;
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;
verum
end; end;
end; A16:
S1[
{} ]
;
A17:
X is
finite
;
S1[
X]
from FINSET_1:sch 2(A17, A16, A2);
hence
ex_sup_of X,
L
;
verum
end;
assume
for X being non empty finite Subset of L holds ex_sup_of X,L
; 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; verum