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} "/\" Dproof
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
and A3:
x' in {x}
and A4:
y in D
;
reconsider a' =
a as
Element of
L by A2;
A5:
x' = x
by A3, TARSKI:def 1;
A6:
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 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