theorem
:: NELSON_1:24
for
L
being
Nelson_Algebra
for
a
,
b
,
c
being
Element
of
L
holds
a
=>
(
b
"/\"
c
)
=
(
a
=>
b
)
"/\"
(
a
=>
c
)