let L be Nelson_Algebra; :: thesis: for a, b, c being Element of L holds a => (b => c) = (a "/\" b) => c
let a, b, c be Element of L; :: thesis: a => (b => c) = (a "/\" b) => c
A1: a => (b => c) < (a "/\" b) => c
proof
A2: a "/\" ((- b) "\/" c) < (- b) "\/" c by Th6;
(- b) "\/" c < b => c by Th13;
then A3: a "/\" ((- b) "\/" c) < b => c by A2, Def3;
a "/\" (- a) < b => c by Def13;
then (a "/\" ((- b) "\/" c)) "\/" (a "/\" (- a)) < b => c by A3, Def7;
then a "/\" (((- b) "\/" c) "\/" (- a)) < b => c by LATTICES:def 11;
then b "/\" (a "/\" (((- b) "\/" c) "\/" (- a))) < c by Def4;
then b "/\" (a "/\" (((- b) "\/" (- a)) "\/" c)) < c by LATTICES:def 5;
then A4: (b "/\" a) "/\" (((- a) "\/" (- b)) "\/" c) < c by LATTICES:def 7;
A5: (b "/\" a) "/\" ((- a) "\/" ((- b) "\/" c)) = ((b "/\" a) "/\" (- a)) "\/" ((b "/\" a) "/\" ((- b) "\/" c)) by LATTICES:def 11;
b "/\" ((- b) "\/" c) = b "/\" (b => c) by Th14;
then A6: ((b "/\" a) "/\" (- a)) "\/" (a "/\" (b "/\" ((- b) "\/" c))) = ((b "/\" a) "/\" (- a)) "\/" ((a "/\" b) "/\" (b => c)) by LATTICES:def 7
.= (b "/\" a) "/\" ((- a) "\/" (b => c)) by LATTICES:def 11 ;
a "/\" ((- a) "\/" (b => c)) = a "/\" (a => (b => c)) by Th14;
then A7: (b "/\" a) "/\" ((- a) "\/" (b => c)) = b "/\" (a "/\" (a => (b => c))) by LATTICES:def 7;
A8: (b "/\" a) "/\" ((- a) "\/" ((- b) "\/" c)) < c by A4, LATTICES:def 5;
(b "/\" a) "/\" ((- a) "\/" ((- b) "\/" c)) = ((b "/\" a) "/\" (- a)) "\/" (a "/\" (b "/\" ((- b) "\/" c))) by A5, LATTICES:def 7;
then (b "/\" a) "/\" (a => (b => c)) < c by LATTICES:def 7, A7, A6, A8;
hence a => (b => c) < (a "/\" b) => c by Def4; :: thesis: verum
end;
A9: - (a => (b => c)) < - ((a "/\" b) => c)
proof
A10: - (a => (b => c)) < a "/\" (- (b => c)) by Def10;
- (b => c) < b "/\" (- c) by Def10;
then a "/\" (- (b => c)) < a "/\" (b "/\" (- c)) by Lm1;
then A11: - (a => (b => c)) < a "/\" (b "/\" (- c)) by A10, Def3;
A12: a "/\" (b "/\" (- c)) = (a "/\" b) "/\" (- c) by LATTICES:def 7;
(a "/\" b) "/\" (- c) < - ((a "/\" b) => c) by Def9;
hence - (a => (b => c)) < - ((a "/\" b) => c) by A11, A12, Def3; :: thesis: verum
end;
A13: (a "/\" b) => c < a => (b => c)
proof
(a "/\" b) => c < (a "/\" b) => c by Def2;
then (a "/\" b) "/\" ((a "/\" b) => c) < c by Def4;
then b "/\" (a "/\" ((a "/\" b) => c)) < c by LATTICES:def 7;
then a "/\" ((a "/\" b) => c) < b => c by Def4;
hence (a "/\" b) => c < a => (b => c) by Def4; :: thesis: verum
end;
A14: - ((a "/\" b) => c) < - (a => (b => c))
proof
A15: - ((a "/\" b) => c) < (a "/\" b) "/\" (- c) by Def10;
A16: (a "/\" b) "/\" (- c) = a "/\" (b "/\" (- c)) by LATTICES:def 7
.= a "/\" ((- (- b)) "/\" (- c)) by ROBBINS3:def 6
.= a "/\" (- ((- b) "\/" c)) by Th1 ;
a "/\" (- ((- b) "\/" c)) < - (a => ((- b) "\/" c)) by Def9;
then A17: - ((a "/\" b) => c) < - (a => ((- b) "\/" c)) by A15, A16, Def3;
A18: b "/\" (- c) < - (b => c) by Def9;
b "/\" (- c) = (- (- b)) "/\" (- c) by ROBBINS3:def 6
.= - ((- b) "\/" c) by Th1 ;
then - (a => ((- b) "\/" c)) < - (a => (b => c)) by Th15, A18;
hence - ((a "/\" b) => c) < - (a => (b => c)) by A17, Def3; :: thesis: verum
end;
A19: a => (b => c) <= (a "/\" b) => c by Th5, A1, A14;
(a "/\" b) => c <= a => (b => c) by Th5, A13, A9;
hence a => (b => c) = (a "/\" b) => c by A19, Th3; :: thesis: verum