let L be with_suprema Poset; for a, b being Element of L holds sup {a,b} = a "\/" b
let a, b be Element of L; sup {a,b} = a "\/" b
( 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; verum