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