let
L
be
B_Lattice
;
:: thesis:
for
X
,
Y
being
Element
of
L
holds
X
"\/"
Y
=
(
X
\
Y
)
"\/"
Y
let
X
,
Y
be
Element
of
L
;
:: thesis:
X
"\/"
Y
=
(
X
\
Y
)
"\/"
Y
thus
X
"\/"
Y
=
(
X
"\/"
Y
)
"/\"
(
Top
L
)
.=
(
X
"\/"
Y
)
"/\"
(
(
Y
`
)
"\/"
Y
)
by
LATTICES:21
.=
(
X
\
Y
)
"\/"
Y
by
LATTICES:11
;
:: thesis:
verum