let Q be non empty strict chain-complete Poset; :: thesis: for M being non empty Chain of Q
for q1 being Element of Q st ( for q being Element of Q st q in M holds
q <= q1 ) holds
sup M <= q1
let M be non empty Chain of Q; :: thesis: for q1 being Element of Q st ( for q being Element of Q st q in M holds
q <= q1 ) holds
sup M <= q1
let q1 be Element of Q; :: thesis: ( ( for q being Element of Q st q in M holds
q <= q1 ) implies sup M <= q1 )
assume for q being Element of Q st q in M holds
q <= q1 ; :: thesis: sup M <= q1
then A1: M is_<=_than q1 by LATTICE3:def 9;
A00: ex_sup_of M,Q by DefchainComplete;
thus sup M <= q1 by YELLOW_0:def 9, A00, A1; :: thesis: verum