theorem Th30: :: NELSON_1:51

for L being Nelson_Algebra
for a, b being Element of L holds (a "/\" b) => b = Top L