let L be Nelson_Algebra; :: thesis: for a, b being Element of L holds (! (a => a)) => b = Top L
let a, b be Element of L; :: thesis: (! (a => a)) => b = Top L
A1: a => a = Top L by Th16ter;
A2: ! (Top L) = (Top L) => (- (Top L)) by Def14;
(! (a => a)) => b = ((Top L) => (Bottom L)) => b by Th2, A2, A1
.= (Bottom L) => b by Th23
.= Top L by Th22 ;
hence (! (a => a)) => b = Top L ; :: thesis: verum