let L be Nelson_Algebra; :: thesis: for a, b, c, d being Element of L holds (b => a) => ((c => d) => ((a => c) => (b => d))) = Top L
let a, b, c, d be Element of L; :: thesis: (b => a) => ((c => d) => ((a => c) => (b => d))) = Top L
A1: c "/\" (c => d) < d by Th17;
a "/\" (a => c) < c by Th17;
then (a "/\" (a => c)) "/\" (c => d) < c "/\" (c => d) by Lm1;
then A2: (a "/\" (a => c)) "/\" (c => d) < d by Def3, A1;
b "/\" (b => a) < a by Th17;
then ( (a => c) "/\" (b "/\" (b => a)) < (a => c) "/\" a & (a => c) "\/" (b "/\" (b => a)) < (a => c) "\/" a ) by Lm1;
then ((a => c) "/\" (b "/\" (b => a))) "/\" (c => d) < ((a => c) "/\" a) "/\" (c => d) by Lm1;
then ((a => c) "/\" (b "/\" (b => a))) "/\" (c => d) < d by A2, Def3;
then ((a => c) "/\" (c => d)) "/\" (b "/\" (b => a)) < d by LATTICES:def 7;
then (((a => c) "/\" (c => d)) "/\" b) "/\" (b => a) < d by LATTICES:def 7;
then (((a => c) "/\" b) "/\" (c => d)) "/\" (b => a) < d by LATTICES:def 7;
then (b "/\" (a => c)) "/\" ((c => d) "/\" (b => a)) < d by LATTICES:def 7;
then b "/\" ((a => c) "/\" ((c => d) "/\" (b => a))) < d by LATTICES:def 7;
then (a => c) "/\" ((c => d) "/\" (b => a)) < b => d by Def4;
then (c => d) "/\" (b => a) < (a => c) => (b => d) by Def4;
then b => a < (c => d) => ((a => c) => (b => d)) by Def4;
hence (b => a) => ((c => d) => ((a => c) => (b => d))) = Top L ; :: thesis: verum