let L be reflexive antisymmetric with_infima RelStr ; 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; for D being non empty lower Subset of L holds {x} "/\" D = (downarrow x) /\ D
let D be non empty lower Subset of L; {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
XBOOLE_0:def 10 (downarrow x) /\ D c= {x} "/\" Dproof
let a be
object ;
TARSKI:def 3 ( not a in {x} "/\" D or a in (downarrow x) /\ D )
assume
a in {x} "/\" D
;
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;
verum
end;
thus
(downarrow x) /\ D c= {x} "/\" D
verum