let L be Nelson_Algebra; :: thesis: for a, b being Element of L holds ((- (a => b)) => (a "/\" (- b))) "/\" ((a "/\" (- b)) => (- (a => b))) = Top L
let a, b be Element of L; :: thesis: ((- (a => b)) => (a "/\" (- b))) "/\" ((a "/\" (- b)) => (- (a => b))) = Top L
A1: - (a => b) < a "/\" (- b) by Def10;
a "/\" (- b) < - (a => b) by Def9;
hence ((- (a => b)) => (a "/\" (- b))) "/\" ((a "/\" (- b)) => (- (a => b))) = Top L by A1; :: thesis: verum