let L be antisymmetric with_infima RelStr ; :: thesis: for X being Subset of L
for Y being non empty Subset of L holds X c= uparrow (X "/\" Y)
let X be Subset of L; :: thesis: for Y being non empty Subset of L holds X c= uparrow (X "/\" Y)
let Y be non empty Subset of L; :: thesis: X c= uparrow (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 uparrow (X "/\" Y) )
assume A2: q in X ; :: thesis: q in uparrow (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 11;
then A3: x "/\" y <= x by LATTICE3:def 14;
( uparrow (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:15;
hence q in uparrow (X "/\" Y) by A3; :: thesis: verum