let P be non empty flat Poset; :: thesis: for p being Element of P
for K being non empty Chain of P st K = {(Bottom P),p} holds
sup K = p
let p be Element of P; :: thesis: for K being non empty Chain of P st K = {(Bottom P),p} holds
sup K = p
let K be non empty Chain of P; :: thesis: ( K = {(Bottom P),p} implies sup K = p )
set z = Bottom P;
assume A0: K = {(Bottom P),p} ; :: thesis: sup K = p
A1: ex_sup_of K,P by Lemflat02;
( Bottom P <= p & p <= p ) by YELLOW_0:44;
then A2: K is_<=_than p by YELLOW_0:8, A0;
for p1 being Element of P st K is_<=_than p1 holds
p <= p1 by A0, YELLOW_0:8;
hence sup K = p by YELLOW_0:def 9, A1, A2; :: thesis: verum