theorem Th35: :: NELSON_1:56

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