let L be reflexive antisymmetric with_infima RelStr ; :: thesis: for x being Element of
for D being non empty lower Subset of holds {x} "/\" D = (downarrow x) /\ D
let x be Element of ; :: thesis: for D being non empty lower Subset of holds {x} "/\" D = (downarrow x) /\ D
let D be non empty lower Subset of ; :: thesis: {x} "/\" D = (downarrow x) /\ D
A1: {x} "/\" D = { (x' "/\" y) where x', y is Element of : ( 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 : ( x' in {x} & y in D ) } by YELLOW_4:def 4;
then consider x', y being Element of such that
A2: a = x' "/\" y and
A3: x' in {x} and
A4: y in D ;
reconsider a' = a as Element of by A2;
A5: x' = x by A3, TARSKI:def 1;
A6: ex v being Element of st
( x' >= v & y >= v & ( for c being Element of st x' >= c & y >= c holds
v >= c ) ) by LATTICE3:def 11;
then A7: x' "/\" y <= x' by LATTICE3:def 14;
A8: x' "/\" y <= y by A6, LATTICE3:def 14;
A9: a in downarrow x by A2, A5, A7, WAYBEL_0:17;
a' 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 set ; :: 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 a' = a as Element of D by A10, XBOOLE_0:def 4;
A12: x in {x} by TARSKI:def 1;
a' <= x by A11, WAYBEL_0:17;
then a' = a' "/\" x by YELLOW_0:25;
hence a in {x} "/\" D by A1, A12; :: thesis: verum

end;