let L be antisymmetric with_suprema RelStr ; :: thesis: for X being Subset of L
for Y being non empty Subset of L holds X c= downarrow (X "\/" Y)
let X be Subset of L; :: thesis: for Y being non empty Subset of L holds X c= downarrow (X "\/" Y)
let Y be non empty Subset of L; :: thesis: X c= downarrow (X "\/" Y)
let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in X or q in downarrow (X "\/" Y) )
assume A1: q in X ; :: thesis: q in downarrow (X "\/" Y)
then reconsider X1 = X as non empty Subset of L ;
reconsider x = q as Element of X1 by A1;
consider y being set such that
A2: y in Y by XBOOLE_0:def 1;
reconsider y = y as Element of Y by A2;
A3: downarrow (X "\/" Y) = { s where s is Element of L : ex y being Element of L st
( s <= y & y in X "\/" Y ) } by WAYBEL_0:14;
ex s being Element of L st
( x <= s & y <= s & ( for c being Element of L st x <= c & y <= c holds
s <= c ) ) by LATTICE3:def 10;
then ( x <= x "\/" y & x "\/" y in X1 "\/" Y ) by LATTICE3:def 13;
hence q in downarrow (X "\/" Y) by A3; :: thesis: verum