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