let L be Nelson_Algebra; :: thesis: for a, b, c, d being Element of L holds (a => b) => ((c => d) => ((a "\/" c) => (b "\/" d))) = Top L
let a, b, c, d be Element of L; :: thesis: (a => b) => ((c => d) => ((a "\/" c) => (b "\/" d))) = Top L
(c => d) "/\" (a => b) < a => b by Th6;
then A1: ((c => d) "/\" (a => b)) "/\" a < b by Def4;
(c => d) "/\" (a => b) < c => d by Th6;
then c "/\" ((c => d) "/\" (a => b)) < d by Def4;
then (((c => d) "/\" (a => b)) "/\" a) "\/" (((c => d) "/\" (a => b)) "/\" c) < b "\/" d by Lm2, A1;
then ((c => d) "/\" (a => b)) "/\" (a "\/" c) < b "\/" d by LATTICES:def 11;
then (c => d) "/\" (a => b) < (a "\/" c) => (b "\/" d) by Def4;
then a => b < (c => d) => ((a "\/" c) => (b "\/" d)) by Def4;
hence (a => b) => ((c => d) => ((a "\/" c) => (b "\/" d))) = Top L ; :: thesis: verum