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