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)
set b = the Element of B;
let x be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not x in A or x <= sup (A "\/" B) )
assume x in A ; :: thesis: x <= sup (A "\/" B)
then A1: x "\/" the Element of B in A "\/" B ;
ex xx being Element of L st
( x <= xx & the Element of B <= xx & ( for c being Element of L st x <= c & the Element of B <= c holds
xx <= c ) ) by LATTICE3:def 10;
then A2: x <= x "\/" the Element of B by LATTICE3:def 13;
ex_sup_of A "\/" B,L by YELLOW_0:17;
then A "\/" B is_<=_than sup (A "\/" B) by YELLOW_0:def 9;
then x "\/" the Element of B <= sup (A "\/" B) by A1;
hence x <= sup (A "\/" B) by A2, YELLOW_0:def 2; :: thesis: verum