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)
consider y being object such that
A1: y in Y by XBOOLE_0:def 1;
reconsider y = y as Element of Y by A1;
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in X or q in downarrow (X "\/" Y) )
assume A2: 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 A2;
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 A3: x <= x "\/" y by LATTICE3:def 13;
( downarrow (X "\/" Y) = { s where s is Element of L : ex y being Element of L st
( s <= y & y in X "\/" Y ) } & x "\/" y in X1 "\/" Y ) by WAYBEL_0:14;
hence q in downarrow (X "\/" Y) by A3; :: thesis: verum