let L be Nelson_Algebra; :: thesis: for a, b being Element of L holds (a => (! b)) => (b => (! a)) = Top L
let a, b be Element of L; :: thesis: (a => (! b)) => (b => (! a)) = Top L
a => (! b) = b => (! a) by Th20;
hence (a => (! b)) => (b => (! a)) = Top L by Th16ter; :: thesis: verum