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