let L be reflexive antisymmetric with_infima RelStr ; :: thesis: for x being Element of L
for D being non empty lower Subset of L holds {x} "/\" D = (downarrow x) /\ D
let x be Element of L; :: thesis: for D being non empty lower Subset of L holds {x} "/\" D = (downarrow x) /\ D
let D be non empty lower Subset of L; :: thesis: {x} "/\" D = (downarrow x) /\ D
A1: {x} "/\" D = { (x' "/\" y) where x', y is Element of L : ( x' in {x} & y in D ) } by YELLOW_4:def 4;
thus {x} "/\" D c= (downarrow x) /\ D :: according to XBOOLE_0:def 10 :: thesis: (downarrow x) /\ D c= {x} "/\" D

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in {x} "/\" D or a in (downarrow x) /\ D )
assume a in {x} "/\" D ; :: thesis: a in (downarrow x) /\ D
then a in { (x' "/\" y) where x', y is Element of L : ( x' in {x} & y in D ) } by YELLOW_4:def 4;
then consider x', y being Element of L such that
A2: ( a = x' "/\" y & x' in {x} & y in D ) ;
reconsider a' = a as Element of L by A2;
A3: x' = x by A2, TARSKI:def 1;
ex v being Element of L st
( x' >= v & y >= v & ( for c being Element of L st x' >= c & y >= c holds
v >= c ) ) by LATTICE3:def 11;
then A4: ( x' "/\" y <= x' & x' "/\" y <= y ) by LATTICE3:def 14;
then A5: a in downarrow x by A2, A3, WAYBEL_0:17;
a' in D by A2, A4, WAYBEL_0:def 19;
hence a in (downarrow x) /\ D by A5, XBOOLE_0:def 4; :: thesis: verum

end;

thus (downarrow x) /\ D c= {x} "/\" D :: thesis: verum

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (downarrow x) /\ D or a in {x} "/\" D )
assume A6: a in (downarrow x) /\ D ; :: thesis: a in {x} "/\" D
then A7: ( a in downarrow x & a in D ) by XBOOLE_0:def 4;
reconsider a' = a as Element of D by A6, XBOOLE_0:def 4;
A8: x in {x} by TARSKI:def 1;
a' <= x by A7, WAYBEL_0:17;
then a' = a' "/\" x by YELLOW_0:25;
hence a in {x} "/\" D by A1, A8; :: thesis: verum

end;