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