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