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