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 b₁ being Element of the carrier of P holds
( not K is_<=_than b₁ or a <= b₁ ) ) & ( for b₁ being Element of the carrier of P holds
( not K is_<=_than b₁ or ex b₂ being Element of the carrier of P st
( K is_<=_than b₂ & not b₁ <= b₂ ) or b₁ = a ) ) )

per cases ( K = {a} or K = {(Bottom P),a} ) by A1;

suppose B100: K = {a} ; :: thesis: ( K is_<=_than a & ( for b₁ being Element of the carrier of P holds
( not K is_<=_than b₁ or a <= b₁ ) ) & ( for b₁ being Element of the carrier of P holds
( not K is_<=_than b₁ or ex b₂ being Element of the carrier of P st
( K is_<=_than b₂ & not b₁ <= b₂ ) or b₁ = 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 b₁ being Element of the carrier of P holds
( not K is_<=_than b₁ or a <= b₁ ) ) & ( for b₁ being Element of the carrier of P holds
( not K is_<=_than b₁ or ex b₂ being Element of the carrier of P st
( K is_<=_than b₂ & not b₁ <= b₂ ) or b₁ = a ) ) ) by B101, B2; :: thesis: verum

end;

suppose A2: K = {(Bottom P),a} ; :: thesis: ( K is_<=_than a & ( for b₁ being Element of the carrier of P holds
( not K is_<=_than b₁ or a <= b₁ ) ) & ( for b₁ being Element of the carrier of P holds
( not K is_<=_than b₁ or ex b₂ being Element of the carrier of P st
( K is_<=_than b₂ & not b₁ <= b₂ ) or b₁ = 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 b₁ being Element of the carrier of P holds
( not K is_<=_than b₁ or a <= b₁ ) ) & ( for b₁ being Element of the carrier of P holds
( not K is_<=_than b₁ or ex b₂ being Element of the carrier of P st
( K is_<=_than b₂ & not b₁ <= b₂ ) or b₁ = a ) ) ) by B101, B2; :: thesis: verum

end;

end;