let P be non empty flat Poset; :: thesis: for K being Chain of P st not K is empty holds
ex_sup_of K,P
let K be Chain of P; :: thesis: ( not K is empty implies ex_sup_of K,P )
assume not K is empty ; :: thesis: ex_sup_of K,P
then reconsider K = K as non empty Chain of P ;
consider a being Element of P such that
A1: ( K = {a} or K = {(Bottom P),a} ) by Thflat01;
take a ; :: according to YELLOW_0:def 7 :: thesis: ( K is_<=_than a & ( for b1 being Element of the carrier of P holds
( not K is_<=_than b1 or a <= b1 ) ) & ( for b1 being Element of the carrier of P holds
( not K is_<=_than b1 or ex b2 being Element of the carrier of P st
( K is_<=_than b2 & not b1 <= b2 ) or b1 = a ) ) )
per cases ( K = {a} or K = {(Bottom P),a} ) by A1;
suppose B100: K = {a} ; :: thesis: ( K is_<=_than a & ( for b1 being Element of the carrier of P holds
( not K is_<=_than b1 or a <= b1 ) ) & ( for b1 being Element of the carrier of P holds
( not K is_<=_than b1 or ex b2 being Element of the carrier of P st
( K is_<=_than b2 & not b1 <= b2 ) or b1 = a ) ) )
B101: for p being Element of P st p in K holds
p <= a by B100, TARSKI:def 1;
B2: for p being Element of P st K is_<=_than p holds
p >= a
proof
let p be Element of P; :: thesis: ( K is_<=_than p implies p >= a )
a in K by B100, TARSKI:def 1;
hence ( K is_<=_than p implies p >= a ) ; :: thesis: verum
end;
for p being Element of P st K is_<=_than p & ( for p1 being Element of P st K is_<=_than p1 holds
p1 >= p ) holds
p = a
proof
let p be Element of P; :: thesis: ( K is_<=_than p & ( for p1 being Element of P st K is_<=_than p1 holds
p1 >= p ) implies p = a )
assume that
C1: K is_<=_than p and
C2: for p1 being Element of P st K is_<=_than p1 holds
p1 >= p ; :: thesis: p = a
C3: p >= a by B2, C1;
a >= p by B101, C2, LATTICE3:def 9;
hence p = a by C3, ORDERS_2:2; :: thesis: verum
end;
hence ( K is_<=_than a & ( for b1 being Element of the carrier of P holds
( not K is_<=_than b1 or a <= b1 ) ) & ( for b1 being Element of the carrier of P holds
( not K is_<=_than b1 or ex b2 being Element of the carrier of P st
( K is_<=_than b2 & not b1 <= b2 ) or b1 = a ) ) ) by B101, B2; :: thesis: verum
end;
suppose A2: K = {(Bottom P),a} ; :: thesis: ( K is_<=_than a & ( for b1 being Element of the carrier of P holds
( not K is_<=_than b1 or a <= b1 ) ) & ( for b1 being Element of the carrier of P holds
( not K is_<=_than b1 or ex b2 being Element of the carrier of P st
( K is_<=_than b2 & not b1 <= b2 ) or b1 = a ) ) )
B101: for p being Element of P st p in K holds
p <= a
proof
let p be Element of P; :: thesis: ( p in K implies p <= a )
assume p in K ; :: thesis: p <= a
then ( p = Bottom P or p = a ) by A2, TARSKI:def 2;
hence p <= a by YELLOW_0:44; :: thesis: verum
end;
B2: for p being Element of P st K is_<=_than p holds
p >= a
proof
let p be Element of P; :: thesis: ( K is_<=_than p implies p >= a )
a in K by A2, TARSKI:def 2;
hence ( K is_<=_than p implies p >= a ) ; :: thesis: verum
end;
for p being Element of P st K is_<=_than p & ( for p1 being Element of P st K is_<=_than p1 holds
p1 >= p ) holds
p = a
proof
let p be Element of P; :: thesis: ( K is_<=_than p & ( for p1 being Element of P st K is_<=_than p1 holds
p1 >= p ) implies p = a )
assume that
C1: K is_<=_than p and
C2: for p1 being Element of P st K is_<=_than p1 holds
p1 >= p ; :: thesis: p = a
C3: p >= a by B2, C1;
a >= p by B101, C2, LATTICE3:def 9;
hence p = a by C3, ORDERS_2:2; :: thesis: verum
end;
hence ( K is_<=_than a & ( for b1 being Element of the carrier of P holds
( not K is_<=_than b1 or a <= b1 ) ) & ( for b1 being Element of the carrier of P holds
( not K is_<=_than b1 or ex b2 being Element of the carrier of P st
( K is_<=_than b2 & not b1 <= b2 ) or b1 = a ) ) ) by B101, B2; :: thesis: verum
end;
end;