let
L
be
B_Lattice
;
:: thesis:
for
X
,
Y
being
Element
of
L
holds
X
`
[=
(
X
"/\"
Y
)
`
let
X
,
Y
be
Element
of
L
;
:: thesis:
X
`
[=
(
X
"/\"
Y
)
`
X
`
[=
(
X
`
)
"\/"
(
Y
`
)
by
LATTICES:5
;
hence
X
`
[=
(
X
"/\"
Y
)
`
by
LATTICES:23
;
:: thesis:
verum