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