let P be non empty chain-complete Poset; :: thesis: for L being non empty Chain of P
for p being Element of P st p in L holds
p <= sup L
let L be non empty Chain of P; :: thesis: for p being Element of P st p in L holds
p <= sup L
let p be Element of P; :: thesis: ( p in L implies p <= sup L )
assume A1: p in L ; :: thesis: p <= sup L
A2: ex_sup_of L,P by POSET_1:def 1;
reconsider x = sup L as Element of P ;
L is_<=_than x by YELLOW_0:def 9, A2;
hence p <= sup L by A1; :: thesis: verum