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

A1: now :: thesis: for c being Element of L st c is_>=_than {a,b} holds
c >= a "\/" b

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;

( a "\/" b >= a & a "\/" b >= b ) by Th22;
then A2: a "\/" b is_>=_than {a,b} by Th8;
then ex_sup_of {a,b},L by A1, Th15;
hence sup {a,b} = a "\/" b by A2, A1, Def9; :: thesis: verum