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

proof

A2: - (a => b) < a "/\" (- b) by Def10;
- b < (- b) "\/" (- c) by Th7;
then - b < - (b "/\" c) by Th8;
then A3: a "/\" (- b) < a "/\" (- (b "/\" c)) by Lm1;
A4: - (a => b) < a "/\" (- (b "/\" c)) by A2, A3, Def3;
a "/\" (- (b "/\" c)) < - (a => (b "/\" c)) by Def9;
then A5: - (a => b) < - (a => (b "/\" c)) by A4, Def3;
A6: - (a => c) < a "/\" (- c) by Def10;
- c < (- b) "\/" (- c) by Th7;
then - c < - (b "/\" c) by Th8;
then a "/\" (- c) < a "/\" (- (b "/\" c)) by Lm1;
then A7: - (a => c) < a "/\" (- (b "/\" c)) by A6, Def3;
a "/\" (- (b "/\" c)) < - (a => (b "/\" c)) by Def9;
then - (a => c) < - (a => (b "/\" c)) by A7, Def3;
then (- (a => b)) "\/" (- (a => c)) < - (a => (b "/\" c)) by A5, Def7;
hence - ((a => b) "/\" (a => c)) < - (a => (b "/\" c)) by Th8; :: thesis: verum

end;

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

proof

A9: - (a => (b "/\" c)) < a "/\" (- (b "/\" c)) by Def10;
A10: a "/\" (- b) < - (a => b) by Def9;
a "/\" (- c) < - (a => c) by Def9;
then (a "/\" (- b)) "\/" (a "/\" (- c)) < (- (a => b)) "\/" (- (a => c)) by A10, Lm2;
then a "/\" ((- b) "\/" (- c)) < (- (a => b)) "\/" (- (a => c)) by LATTICES:def 11;
then a "/\" (- (b "/\" c)) < (- (a => b)) "\/" (- (a => c)) by Th8;
then a "/\" (- (b "/\" c)) < - ((a => b) "/\" (a => c)) by Th8;
hence - (a => (b "/\" c)) < - ((a => b) "/\" (a => c)) by A9, Def3; :: thesis: verum

end;

A11: a => (b "/\" c) < (a => b) "/\" (a => c)

proof

A12: a => (b "/\" c) < a => b by Th6, Th16bis;
a => (b "/\" c) < a => c by Th6, Th16bis;
hence a => (b "/\" c) < (a => b) "/\" (a => c) by A12, Def8; :: thesis: verum

end;

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

proof

a => b < a => b by Def2;
then A14: a "/\" (a => b) < b by Def4;
a => c < a => c by Def2;
then a "/\" (a => c) < c by Def4;
then (a "/\" (a => b)) "/\" (a "/\" (a => c)) < b "/\" c by A14, Lm2;
then ((a "/\" (a => b)) "/\" a) "/\" (a => c) < b "/\" c by LATTICES:def 7;
then ((a "/\" a) "/\" (a => b)) "/\" (a => c) < b "/\" c by LATTICES:def 7;
then a "/\" ((a => b) "/\" (a => c)) < b "/\" c by LATTICES:def 7;
hence (a => b) "/\" (a => c) < a => (b "/\" c) by Def4; :: thesis: verum

end;

A15: a => (b "/\" c) <= (a => b) "/\" (a => c) by A1, A11, Th5;
(a => b) "/\" (a => c) <= a => (b "/\" c) by A8, A13, Th5;
hence a => (b "/\" c) = (a => b) "/\" (a => c) by A15, Th3; :: thesis: verum