let L be Nelson_Algebra; :: thesis: for a, b being Element of L holds (- a) "\/" b <= a => b
let a, b be Element of L; :: thesis: (- a) "\/" b <= a => b
a < - (! a) by Def11;
then a "/\" (- b) < (- (! a)) "/\" (- b) by Lm1;
then A1: a "/\" (- b) < - ((! a) "\/" b) by Th1;
- (a => b) < a "/\" (- b) by Def10;
then A2: - (a => b) < - ((! a) "\/" b) by A1, Def3;
a => (Bottom L) < a => (Bottom L) by Def2;
then (a => (Bottom L)) "/\" a < Bottom L by Def4;
then a "/\" (a => ((Top L) `)) < Bottom L by Th2;
then A3: a "/\" (! a) < Bottom L by Def14;
Bottom L <= b ;
then Bottom L < b by Th5;
then a "/\" (! a) < b by A3, Def3;
then A4: ! a < a => b by Def4;
b "/\" a < b by Th6;
then b < a => b by Def4;
then A5: (! a) "\/" b <= a => b by A2, Th5, A4, Def7;
a "/\" (- a) < Bottom L by Def13;
then A6: - a < a => (Bottom L) by Def4;
a => ((Top L) `) = ! a by Def14;
then A7: - a < ! a by A6, Th2;
A8: - (! a) < a by Def12;
a = - (- a) by ROBBINS3:def 6;
then - a <= ! a by A8, A7, Th5;
then b "\/" (- a) <= b "\/" (! a) by Th10;
hence (- a) "\/" b <= a => b by A5, Th9; :: thesis: verum