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
A2: ex_sup_of M,Q by Def1;
set x = sup M;
M is_<=_than sup M by A2, YELLOW_0:def 9;
hence q <= sup M by A1; :: thesis: verum