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 ;
A2: ex_sup_of M,Q by Def1;
thus sup M <= q1 by A2, A1, YELLOW_0:def 9; :: thesis: verum