let L be Nelson_Algebra; :: thesis: for a, b being Element of L holds a "/\" (a => b) = a "/\" ((- a) "\/" b)
let a, b be Element of L; :: thesis: a "/\" (a => b) = a "/\" ((- a) "\/" b)
A1: a "/\" (a => b) < a "/\" ((- a) "\/" b)

proof

a => b < a => b by Def2;
then A2: a "/\" (a => b) < b by Def4;
b < b "\/" (- a) by Th7;
then A3: a "/\" (a => b) < (- a) "\/" b by A2, Def3;
a "/\" (a => b) < a by Th6;
hence a "/\" (a => b) < a "/\" ((- a) "\/" b) by A3, Def8; :: thesis: verum

end;

A4: - (a "/\" ((- a) "\/" b)) < - (a "/\" (a => b))

proof

A5: - (a "/\" ((- a) "\/" b)) = (- a) "\/" (- ((- a) "\/" b)) by Th8;
A6: (- a) "\/" (- ((- a) "\/" b)) = (- a) "\/" ((- (- a)) "/\" (- b)) by Th1;
A7: (- a) "\/" ((- (- a)) "/\" (- b)) = (- a) "\/" (a "/\" (- b)) by ROBBINS3:def 6;
A8: a "/\" (- b) < - (a => b) by Def9;
- (a => b) < (- a) "\/" (- (a => b)) by Th7;
then A9: - (a => b) < - (a "/\" (a => b)) by Th8;
A10: - a < (- a) "\/" (- (a => b)) by Th7;
A11: a "/\" (- b) < - (a "/\" (a => b)) by A8, A9, Def3;
- a < - (a "/\" (a => b)) by A10, Th8;
hence - (a "/\" ((- a) "\/" b)) < - (a "/\" (a => b)) by A5, A6, A7, A11, Def7; :: thesis: verum

end;

A12: a "/\" ((- a) "\/" b) < a "/\" (a => b)

proof

(- a) "\/" b < a => b by Th13;
hence a "/\" ((- a) "\/" b) < a "/\" (a => b) by Lm1; :: thesis: verum

end;

A13: - (a "/\" (a => b)) < - (a "/\" ((- a) "\/" b))

proof

- (a => b) < a "/\" (- b) by Def10;
then (- a) "\/" (- (a => b)) < (- a) "\/" (a "/\" (- b)) by Lm1;
then - (a "/\" (a => b)) < (- a) "\/" (a "/\" (- b)) by Th8;
then - (a "/\" (a => b)) < (- a) "\/" ((- (- a)) "/\" (- b)) by ROBBINS3:def 6;
then - (a "/\" (a => b)) < (- a) "\/" (- ((- a) "\/" b)) by Th1;
hence - (a "/\" (a => b)) < - (a "/\" ((- a) "\/" b)) by Th8; :: thesis: verum

end;

A14: a "/\" ((- a) "\/" b) <= a "/\" (a => b) by A12, A13, Th5;
a "/\" (a => b) <= a "/\" ((- a) "\/" b) by A1, A4, Th5;
hence a "/\" (a => b) = a "/\" ((- a) "\/" b) by A14, Th3; :: thesis: verum