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