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