let L be Nelson_Algebra; :: thesis: for a being Element of L holds ((- (! a)) => a) "/\" (a => (- (! a))) = Top L
let a be Element of L; :: thesis: ((- (! a)) => a) "/\" (a => (- (! a))) = Top L
A1: - (! a) < a by Def12;
a < - (! a) by Def11;
hence ((- (! a)) => a) "/\" (a => (- (! a))) = Top L by A1; :: thesis: verum