let L be non empty transitive antisymmetric complete RelStr ; :: thesis: for A being Subset of L
for B being non empty Subset of L holds A is_<=_than sup (A "\/" B)
let A be Subset of L; :: thesis: for B being non empty Subset of L holds A is_<=_than sup (A "\/" B)
let B be non empty Subset of L; :: thesis: A is_<=_than sup (A "\/" B)
ex_sup_of A "\/" B,L by YELLOW_0:17;
then A1: A "\/" B is_<=_than sup (A "\/" B) by YELLOW_0:def 9;
let x be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not x in A or x <= sup (A "\/" B) )
assume A2: x in A ; :: thesis: x <= sup (A "\/" B)
consider b being Element of B;
x "\/" b in A "\/" B by A2;
then A3: x "\/" b <= sup (A "\/" B) by A1, LATTICE3:def 9;
ex xx being Element of L st
( x <= xx & b <= xx & ( for c being Element of L st x <= c & b <= c holds
xx <= c ) ) by LATTICE3:def 10;
then x <= x "\/" b by LATTICE3:def 13;
hence x <= sup (A "\/" B) by A3, YELLOW_0:def 2; :: thesis: verum