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