let L be Nelson_Algebra; :: thesis: for a, b, c being Element of L st a < b holds
( b => c < a => c & c => a < c => b )
let a, b, c be Element of L; :: thesis: ( a < b implies ( b => c < a => c & c => a < c => b ) )
assume A1: a < b ; :: thesis: ( b => c < a => c & c => a < c => b )
(Top L) => (a => c) = a => c by Th23;
then A2: a => (b => c) < a => c by A1, Th25;
a "/\" (b => c) < b => c by Th6;
then A3: b => c < a => (b => c) by Def4;
A4: c => (Top L) = Top L by Th21;
(c => (a => b)) => ((c => a) => (c => b)) = Top L by Th25;
hence ( b => c < a => c & c => a < c => b ) by A1, A2, A3, A4, Th23, Def3; :: thesis: verum