let
L
be
B_Lattice
;
:: thesis:
for
X
,
Y
being
Element
of
L
holds
(
X
\
Y
)
"/\"
Y
=
Bottom
L
let
X
,
Y
be
Element
of
L
;
:: thesis:
(
X
\
Y
)
"/\"
Y
=
Bottom
L
(
X
\
Y
)
"/\"
Y
=
X
"/\"
(
(
Y
`
)
"/\"
Y
)
by
LATTICES:def 7
.=
X
"/\"
(
Bottom
L
)
by
LATTICES:20
;
hence
(
X
\
Y
)
"/\"
Y
=
Bottom
L
;
:: thesis:
verum