let L be with_suprema Poset; :: thesis: for a, b being Element of L holds sup {a,b} = a "\/" b
let a, b be Element of L; :: thesis: sup {a,b} = a "\/" b
( a "\/" b >= a & a "\/" b >= b ) by Th22;
then A1: a "\/" b is_>=_than {a,b} by Th8;

A2: now

let c be Element of L; :: thesis: ( c is_>=_than {a,b} implies c >= a "\/" b )
assume c is_>=_than {a,b} ; :: thesis: c >= a "\/" b
then ( c >= a & c >= b ) by Th8;
hence c >= a "\/" b by Th22; :: thesis: verum

end;

then ex_sup_of {a,b},L by A1, Th15;
hence sup {a,b} = a "\/" b by A1, A2, Def9; :: thesis: verum