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 = { (x9 "/\" y) where x9, y is Element of L : ( x9 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 object ; :: 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 { (x9 "/\" y) where x9, y is Element of L : ( x9 in {x} & y in D ) } by YELLOW_4:def 4;
then consider x9, y being Element of L such that
A2: a = x9 "/\" y and
A3: x9 in {x} and
A4: y in D ;
reconsider a9 = a as Element of L by A2;
A5: x9 = x by A3, TARSKI:def 1;
A6: ex v being Element of L st
( x9 >= v & y >= v & ( for c being Element of L st x9 >= c & y >= c holds
v >= c ) ) by LATTICE3:def 11;
then A7: x9 "/\" y <= x9 by LATTICE3:def 14;
A8: x9 "/\" y <= y by A6, LATTICE3:def 14;
A9: a in downarrow x by A2, A5, A7, WAYBEL_0:17;
a9 in D by A2, A4, A8, WAYBEL_0:def 19;
hence a in (downarrow x) /\ D by A9, XBOOLE_0:def 4; :: thesis: verum

end;

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

proof

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

end;