nelson_1.miz

begin

 definition

 let L be non empty OrthoLattStr;

 :: NELSON_1:def1

 attr L is DeMorgan means

 : Def1: for x,y be Element of L holds ((x "/\" y) ` ) = ((x ` ) "\/" (y ` ));

 end

 registration

 cluster de_Morgan involutive -> DeMorgan for non empty OrthoLattStr;

 coherence

 proof

 let L be non empty OrthoLattStr;

 assume

 A1: L is de_Morgan involutive;

 let x,y be Element of L;

 (x "/\" y) = (((x ` ) "\/" (y ` )) ` ) by A1;

 hence thesis by A1;

 end;

 cluster DeMorgan involutive -> de_Morgan for non empty OrthoLattStr;

 coherence

 proof

 let L be non empty OrthoLattStr;

 assume

 A1: L is DeMorgan involutive;

 now

 let x,y be Element of L;

 ((x ` ) "\/" (y ` )) = ((x "/\" y) ` ) by A1;

 hence (((x ` ) "\/" (y ` )) ` ) = (x "/\" y) by A1;

 end;

 hence thesis;

 end;

 end

 registration

 cluster trivial -> DeMorgan for non empty OrthoLattStr;

 coherence by STRUCT_0:def 10;

 end

 registration

 cluster DeMorgan involutive bounded distributive Lattice-like for non empty OrthoLattStr;

 existence

 proof

 take TrivOrtLat ;

 thus thesis;

 end;

 end

 definition

 mode DeMorgan_Algebra is DeMorgan involutive distributive Lattice-like non empty OrthoLattStr;

 end

 definition

 mode Quasi-Boolean_Algebra is bounded DeMorgan_Algebra;

 end

 reserve L for Quasi-Boolean_Algebra,

x,y,z for Element of L;

 theorem :: NELSON_1:1



 Th1: ((x "\/" y) ` ) = ((x ` ) "/\" (y ` ))

 proof

 (((x ` ) "/\" (y ` )) ` ) = (((x ` ) ` ) "\/" ((y ` ) ` )) by Def1;



 hence ((x ` ) "/\" (y ` )) = ((((x ` ) ` ) "\/" ((y ` ) ` )) ` ) by ROBBINS3:def 6

 .= ((x "\/" ((y ` ) ` )) ` ) by ROBBINS3:def 6

 .= ((x "\/" y) ` ) by ROBBINS3:def 6;

 end;

 theorem :: NELSON_1:2



 Th2: (( Top L) ` ) = ( Bottom L)

 proof



 thus (( Top L) ` ) = ((( Top L) ` ) "\/" ( Bottom L))

 .= ((( Top L) ` ) "\/" ((( Bottom L) ` ) ` )) by ROBBINS3:def 6

 .= ((( Top L) "/\" (( Bottom L) ` )) ` ) by Def1

 .= ( Bottom L) by ROBBINS3:def 6;

 end;

 theorem :: NELSON_1:3

 (( Bottom L) ` ) = ( Top L)

 proof



 thus (( Bottom L) ` ) = ((((( Bottom L) ` ) "/\" ( Top L)) ` ) ` ) by ROBBINS3:def 6

 .= ((((( Bottom L) ` ) ` ) "\/" (( Top L) ` )) ` ) by Def1

 .= ((( Bottom L) "\/" (( Top L) ` )) ` ) by ROBBINS3:def 6

 .= ( Top L) by ROBBINS3:def 6;

 end;

 theorem :: NELSON_1:4

 (x "/\" (x "/\" y)) = (x "/\" y)

 proof



 thus (x "/\" (x "/\" y)) = ((x "/\" x) "/\" y) by LATTICES:def 7

 .= (x "/\" y);

 end;

 theorem :: NELSON_1:5

 (x "\/" (x "\/" y)) = (x "\/" y)

 proof



 thus (x "\/" (x "\/" y)) = ((x "\/" x) "\/" y) by LATTICES:def 5

 .= (x "\/" y);

 end;

 begin

 definition

 struct ( OrthoLattStr) NelsonStr (# the carrier -> set,

the unity -> Element of the carrier,

the Compl, Nnegation -> UnOp of the carrier,

the Iimpl, impl, L_join, L_meet -> BinOp of the carrier #)

 attr strict strict;

 end

 registration

 cluster strict non empty for NelsonStr;

 existence

 proof

 set A = { {} };

 set B = the Element of A;

 set C = the UnOp of A;

 set D = the BinOp of A;

 take NelsonStr (# A, B, C, C, D, D, D, D #);

 thus thesis;

 end;

 end

 registration

 cluster trivial DeMorgan involutive bounded distributive Lattice-like for non empty NelsonStr;

 existence

 proof

 set A = { {} };

 set B = the Element of A;

 set C = the UnOp of A;

 set D = the BinOp of A;

 reconsider N = NelsonStr (# A, B, C, C, D, D, D, D #) as non empty NelsonStr;

 take N;

 A1:

 now

 let x,y be Element of N;

 x = {} & y = {} by TARSKI:def 1;

 hence x = y & x = {} ;

 end;

 thus N is trivial;

 thus N is DeMorgan by A1;

 thus N is involutive by A1;

 thus N is bounded distributive

 proof

 reconsider E = {} as Element of N by TARSKI:def 1;

 for x be Element of N holds (E "\/" x) = E & (x "\/" E) = E & (x "/\" E) = E & (E "/\" x) = E by TARSKI:def 1;

 then N is lower-bounded upper-bounded;

 hence N is bounded;

 let x,y,z be Element of N;

 thus (x "/\" (y "\/" z)) = ((x "/\" y) "\/" (x "/\" z)) by A1;

 end;

 N is join-commutative join-associative meet-absorbing meet-commutative meet-associative join-absorbing by A1;

 hence thesis;

 end;

 end

 definition

 let L be non empty NelsonStr, a,b be Element of L;

 :: NELSON_1:def2

 func a => b -> Element of L equals (the Iimpl of L . (a,b));

 coherence ;

 end

 definition

 let L be non empty NelsonStr, a,b be Element of L;

 :: NELSON_1:def3

 pred a b) = ( Top L);

 end

 definition

 let L be non empty NelsonStr, a,b be Element of L;

 :: NELSON_1:def4

 pred a <= b means a = (a "/\" b);

 end

 definition

 let L be non empty NelsonStr, a be Element of L;

 :: NELSON_1:def5

 func ! a -> Element of L equals (the Nnegation of L . a);

 coherence ;

 end

 definition

 let L be non empty NelsonStr, a,b be Element of L;

 :: NELSON_1:def6

 func a =-> b -> Element of L equals (the impl of L . (a,b));

 coherence ;

 end

 begin

 definition

 let L be non empty NelsonStr;

 :: NELSON_1:def7

 attr L is satisfying_A1 means

 : Def2: for a be Element of L holds a < a;

 :: NELSON_1:def8

 attr L is satisfying_A1b means

 : Def3: for a,b,c be Element of L holds a < b & b < c implies a < c;

 end

 definition

 let L be bounded Lattice-like non empty NelsonStr;

 :: NELSON_1:def9

 attr L is satisfying_A2 means L is DeMorgan involutive distributive;

 end

 registration

 cluster satisfying_A2 -> DeMorgan involutive distributive for bounded Lattice-like non empty NelsonStr;

 coherence ;

 cluster DeMorgan involutive distributive -> satisfying_A2 for bounded Lattice-like non empty NelsonStr;

 coherence ;

 end

 definition

 let L be non empty NelsonStr;

 :: NELSON_1:def10

 attr L is satisfying_N3 means

 : Def4: for x,a,b be Element of L holds (a "/\" x) b);

 :: NELSON_1:def11

 attr L is satisfying_N4 means

 : Def5: for a,b be Element of L holds (a =-> b) = ((a => b) "/\" (( - b) => ( - a)));

 :: NELSON_1:def12

 attr L is satisfying_N5 means

 : Def6: for a,b be Element of L holds (a =-> b) = ( Top L) iff (a "/\" b) = a;

 :: NELSON_1:def13

 attr L is satisfying_N6 means

 : Def7: for a,b,c be Element of L holds a < c & b < c implies (a "\/" b) < c;

 :: NELSON_1:def14

 attr L is satisfying_N7 means

 : Def8: for a,b,c be Element of L holds a b));

 :: NELSON_1:def16

 attr L is satisfying_N9 means

 : Def10: for a,b be Element of L holds ( - (a => b)) < (a "/\" ( - b));

 :: NELSON_1:def17

 attr L is satisfying_N10 means

 : Def11: for a be Element of L holds a < ( - ( ! a));

 :: NELSON_1:def18

 attr L is satisfying_N11 means

 : Def12: for a be Element of L holds ( - ( ! a)) < a;

 :: NELSON_1:def19

 attr L is satisfying_N12 means

 : Def13: for a,b be Element of L holds (a "/\" ( - a)) < b;

 :: NELSON_1:def20

 attr L is satisfying_N13 means

 : Def14: for a be Element of L holds ( ! a) = (a => ( - ( Top L)));

 end

 registration

 cluster satisfying_A1 satisfying_A1b satisfying_A2 satisfying_N3 satisfying_N4 satisfying_N5 satisfying_N6 satisfying_N7 satisfying_N8 satisfying_N9 satisfying_N10 satisfying_N11 satisfying_N12 satisfying_N13 for bounded Lattice-like non empty NelsonStr;

 existence

 proof

 set L = the trivial non empty NelsonStr;

 reconsider LL = L as bounded Lattice-like non empty NelsonStr;



 A1: LL is satisfying_A1

 proof

 let a be Element of LL;

 thus thesis by STRUCT_0:def 10;

 end;



 A2: LL is satisfying_A1b by STRUCT_0:def 10;



 A3: LL is satisfying_N8

 proof

 let a,b be Element of LL;

 thus thesis by STRUCT_0:def 10;

 end;



 A4: LL is satisfying_N9

 proof

 let a,b be Element of LL;

 thus thesis by STRUCT_0:def 10;

 end;



 A5: LL is satisfying_A2 satisfying_N4 satisfying_N6 satisfying_N7 satisfying_N5 by STRUCT_0:def 10;



 A6: LL is satisfying_N10

 proof

 let a be Element of LL;

 thus thesis by STRUCT_0:def 10;

 end;



 A7: LL is satisfying_N11

 proof

 let a be Element of LL;

 thus thesis by STRUCT_0:def 10;

 end;



 A8: LL is satisfying_N12

 proof

 let a be Element of LL;

 thus thesis by STRUCT_0:def 10;

 end;



 A9: LL is satisfying_N3

 proof

 let x,a,b be Element of LL;

 thus thesis by STRUCT_0:def 10;

 end;

 LL is satisfying_N13 by STRUCT_0:def 10;

 hence thesis by A1, A2, A3, A4, A5, A6, A7, A8, A9;

 end;

 end

 definition

 mode Nelson_Algebra is satisfying_A1 satisfying_A1b satisfying_A2 satisfying_N3 satisfying_N4 satisfying_N5 satisfying_N6 satisfying_N7 satisfying_N8 satisfying_N9 satisfying_N10 satisfying_N11 satisfying_N12 satisfying_N13 bounded Lattice-like non empty NelsonStr;

 end

 definition

 let L be satisfying_N4 bounded non empty NelsonStr, a,b be Element of L;

 :: original: =->

 redefine

 :: NELSON_1:def21

 func a =-> b equals ((a => b) "/\" (( - b) => ( - a)));

 compatibility by Def5;

 end

 reserve L for Nelson_Algebra,

a,b,c,d,x,y,z for Element of L;

 theorem :: NELSON_1:6

 a [= b iff a <= b by LATTICES: 4;

 theorem :: NELSON_1:7



 Th3: a <= b & b <= a iff a = b

 proof

 thus a <= b & b <= a implies a = b

 proof

 assume a <= b & b <= a;

 then a [= b & b [= a by LATTICES: 4;

 hence thesis by LATTICES: 8;

 end;

 thus thesis;

 end;

 theorem :: NELSON_1:8



 Th4: (a "/\" b) = ( Top L) iff a = ( Top L) & b = ( Top L)

 proof

 hereby

 assume

 A1: (a "/\" b) = ( Top L);

 then ( Top L) [= a by LATTICES: 6;

 hence a = ( Top L);

 ( Top L) [= b by A1, LATTICES: 6;

 hence b = ( Top L);

 end;

 thus thesis;

 end;

 theorem :: NELSON_1:9



 Th5: a <= b iff a b) = ( Top L) by Def6;

 hence a b) = ( Top L);

 hence thesis by Def6;

 end;

 theorem :: NELSON_1:10



 Th6: (a "/\" b) < a

 proof

 (a "/\" b) <= a by LATTICES: 4, LATTICES: 6;

 hence thesis by Th5;

 end;

 theorem :: NELSON_1:11



 Th7: a < (a "\/" b)

 proof

 a <= (a "\/" b) by LATTICES: 4, LATTICES: 5;

 hence thesis by Th5;

 end;

 theorem :: NELSON_1:12

 a <= b iff (a =-> b) = ( Top L) by Def6;

 theorem :: NELSON_1:13



 Th8: ( - (a "/\" b)) = (( - a) "\/" ( - b))

 proof



 thus ( - (a "/\" b)) = ( - (( - ( - a)) "/\" b)) by ROBBINS3:def 6

 .= ( - (( - ( - a)) "/\" ( - ( - b)))) by ROBBINS3:def 6

 .= ( - ( - (( - a) "\/" ( - b)))) by Th1

 .= (( - a) "\/" ( - b)) by ROBBINS3:def 6;

 end;

 theorem :: NELSON_1:14

 ((a "/\" ( - a)) "/\" (b "\/" ( - b))) = (a "/\" ( - a))

 proof

 (( - b) "/\" ( - ( - b))) < (( - a) "\/" a) by Def13;

 then ( - (b "\/" ( - b))) < (( - a) "\/" a) by Th1;

 then ( - (b "\/" ( - b))) < (( - a) "\/" ( - ( - a))) by ROBBINS3:def 6;

 then ( - (b "\/" ( - b))) < ( - (a "/\" ( - a))) by Th8;

 then (a "/\" ( - a)) <= (b "\/" ( - b)) by Th5, Def13;

 hence thesis;

 end;



 Lm1: b < c implies (a "\/" b) < (a "\/" c) & (a "/\" b) < (a "/\" c)

 proof

 assume

 A1: b < c;



 A2: a < (a "\/" c) by Th7;

 c < (a "\/" c) by Th7;

 then

 A3: b < (a "\/" c) by A1, Def3;



 A4: (a "/\" b) < a by Th6;

 (a "/\" b) < b by Th6;

 then (a "/\" b) < c by A1, Def3;

 hence thesis by A3, A4, Def8, A2, Def7;

 end;

 theorem :: NELSON_1:15



 Th9: a <= b & b <= c implies a <= c

 proof

 assume a <= b & b <= c;

 then a [= b & b [= c by LATTICES: 4;

 hence thesis by LATTICES: 4, LATTICES: 7;

 end;

 theorem :: NELSON_1:16



 Th10: b <= c implies (a "\/" b) <= (a "\/" c) & (a "/\" b) <= (a "/\" c)

 proof

 assume

 A1: b <= c;



 A2: (a "\/" b) < (a "\/" c)

 proof

 b < c by A1, Th5;

 hence thesis by Lm1;

 end;



 A3: ( - (a "\/" c)) < ( - (a "\/" b))

 proof

 ( - c) < ( - b) by A1, Th5;

 then (( - a) "/\" ( - c)) < (( - a) "/\" ( - b)) by Lm1;

 then ( - (a "\/" c)) < (( - a) "/\" ( - b)) by Th1;

 hence thesis by Th1;

 end;



 A4: (a "/\" b) < (a "/\" c)

 proof

 b < c by A1, Th5;

 hence thesis by Lm1;

 end;

 ( - (a "/\" c)) < ( - (a "/\" b))

 proof

 ( - c) < ( - b) by A1, Th5;

 then (( - a) "\/" ( - c)) < (( - a) "\/" ( - b)) by Lm1;

 then ( - (a "/\" c)) < (( - a) "\/" ( - b)) by Th8;

 hence thesis by Th8;

 end;

 hence thesis by A4, Th5, A2, A3;

 end;

 theorem :: NELSON_1:17



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

 proof

 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 Def4;

 (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 thesis by A5, Th9;

 end;

 theorem :: NELSON_1:18



 Th12: ((a => b) "/\" (( - a) "\/" b)) = (( - a) "\/" b)

 proof



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

 proof



 A2: ( - (( - a) "\/" b)) = (( - ( - a)) "/\" ( - b)) by Th1;



 A3: (( - ( - a)) "/\" ( - b)) = (a "/\" ( - b)) by ROBBINS3:def 6;

 (a "/\" ( - b)) < ( - (a => b)) by Def9;

 then (( - (( - a) "\/" b)) "\/" ( - (( - a) "\/" b))) < (( - (a => b)) "\/" ( - (( - a) "\/" b))) by A2, A3, Lm1;

 hence thesis by Th8;

 end;



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

 proof

 (( - a) "\/" b) <= (a => b) by Th11;

 hence thesis;

 end;

 ((a => b) "/\" (( - a) "\/" b)) <= (( - a) "\/" b) by Th6, A1, Th5;

 hence thesis by A4, Th3;

 end;

 theorem :: NELSON_1:19



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

 proof

 ((a => b) "/\" (( - a) "\/" b)) = (( - a) "\/" b) by Th12;

 then (( - a) "\/" b) <= (a => b);

 hence thesis by Th5;

 end;

 theorem :: NELSON_1:20



 Th14: (a "/\" (a => b)) = (a "/\" (( - a) "\/" b))

 proof



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

 proof

 (a => b) < (a => b) by Def2;

 then

 A2: (a "/\" (a => b)) b)) < (( - a) "\/" b) by A2, Def3;

 (a "/\" (a => b)) < a by Th6;

 hence thesis by A3, Def8;

 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 thesis by A5, A6, A7, A11, Def7;

 end;



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

 proof

 (( - a) "\/" b) < (a => b) by Th13;

 hence thesis by Lm1;

 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 thesis by Th8;

 end;



 A14: (a "/\" (( - a) "\/" b)) <= (a "/\" (a => b)) by A12, A13, Th5;

 (a "/\" (a => b)) <= (a "/\" (( - a) "\/" b)) by A1, A4, Th5;

 hence thesis by A14, Th3;

 end;



 Lm2: a < b & c < d implies (a "\/" c) < (b "\/" d) & (a "/\" c) < (b "/\" d)

 proof

 assume a < b & c < d;

 then (a "\/" c) < (a "\/" d) & (a "/\" c) < (a "/\" d) & (a "\/" d) < (b "\/" d) & (a "/\" d) < (b "/\" d) by Lm1;

 hence thesis by Def3;

 end;

 theorem :: NELSON_1:21



 Th15: ( - x) < ( - y) implies ( - (z => x)) < ( - (z => y))

 proof

 assume

 A1: ( - x) < ( - y);



 A2: ( - (z => x)) < (z "/\" ( - x)) by Def10;

 (z "/\" ( - x)) < (z "/\" ( - y)) by A1, Lm1;

 then

 A3: ( - (z => x)) < (z "/\" ( - y)) by A2, Def3;

 (z "/\" ( - y)) < ( - (z => y)) by Def9;

 hence thesis by A3, Def3;

 end;

 theorem :: NELSON_1:22



 Th16: x < y implies (a "/\" (a => x)) < y

 proof

 assume

 A1: x < y;



 A2: (a "/\" (a => x)) = (a "/\" (( - a) "\/" x)) by Th14;



 A3: (a "/\" (( - a) "\/" x)) = ((a "/\" ( - a)) "\/" (a "/\" x)) by LATTICES:def 11;



 A4: (a "/\" x) < x by Th6;

 (a "/\" ( - a)) < x by Def13;

 then (a "/\" (a => x)) < x by A3, A2, A4, Def7;

 hence thesis by A1, Def3;

 end;

 theorem :: NELSON_1:23



 Th16bis: x < y implies (a => x) < (a => y)

 proof

 assume x < y;

 then (a "/\" (a => x)) < y by Th16;

 hence thesis by Def4;

 end;

 theorem :: NELSON_1:24

 (a => (b "/\" c)) = ((a => b) "/\" (a => c))

 proof



 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 thesis by Th8;

 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 thesis by A9, Def3;

 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 thesis by A12, Def8;

 end;



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

 proof

 (a => b) < (a => b) by Def2;

 then

 A14: (a "/\" (a => b)) 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 thesis by Def4;

 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 thesis by A15, Th3;

 end;



 Lm3: (a => (b => c)) = ((a "/\" b) => c)

 proof



 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 thesis by Def4;

 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 thesis by A11, A12, Def3;

 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 thesis by Def4;

 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 thesis by A17, Def3;

 end;



 A19: (a => (b => c)) <= ((a "/\" b) => c) by Th5, A1, A14;

 ((a "/\" b) => c) <= (a => (b => c)) by Th5, A13, A9;

 hence thesis by A19, Th3;

 end;

 begin

 theorem :: NELSON_1:25

 (a =-> a) = ( Top L)

 proof

 (a "/\" a) = a;

 hence thesis by Def6;

 end;

 theorem :: NELSON_1:26

 (a =-> b) = ( Top L) & (b =-> c) = ( Top L) implies (a =-> c) = ( Top L)

 proof

 assume (a =-> b) = ( Top L) & (b =-> c) = ( Top L);

 then (a "/\" b) = a & (b "/\" c) = b by Def6;

 then (a "/\" c) = a by LATTICES:def 7;

 hence thesis by Def6;

 end;

 theorem :: NELSON_1:27

 (a =-> b) = ( Top L) & (b =-> a) = ( Top L) implies a = b

 proof

 assume (a =-> b) = ( Top L) & (b =-> a) = ( Top L);

 then (a "/\" b) = a & (b "/\" a) = b by Def6;

 hence thesis;

 end;

 theorem :: NELSON_1:28

 (a =-> ( Top L)) = ( Top L)

 proof

 (a "/\" ( Top L)) = a;

 hence thesis by Def6;

 end;

 theorem :: NELSON_1:29



 Th16ter: (a => a) = ( Top L)

 proof

 a < a by Def2;

 hence thesis;

 end;

 theorem :: NELSON_1:30

 (a => b) = ( Top L) & (b => c) = ( Top L) implies (a => c) = ( Top L)

 proof

 assume

 A1: (a => b) = ( Top L) & (b => c) = ( Top L);



 A2: a < b by A1;



 A3: b < c by A1;

 a < c by Def3, A2, A3;

 hence thesis;

 end;

 theorem :: NELSON_1:31

 b < c implies (a "\/" b) < (a "\/" c) & (a "/\" b) < (a "/\" c) by Lm1;

 theorem :: NELSON_1:32

 a b)) b) < (a => b) by Def2;

 hence thesis by Def4;

 end;

 theorem :: NELSON_1:34

 (a => (b => c)) = ((a "/\" b) => c) by Lm3;

 theorem :: NELSON_1:35



 Th18: (a => (b => c)) = (b => (a => c))

 proof

 (a => (b => c)) = ((a "/\" b) => c) by Lm3

 .= (b => (a => c)) by Lm3;

 hence thesis;

 end;

 theorem :: NELSON_1:36



 Th19: a < ((a => b) => b)

 proof

 (a "/\" (a => b)) (a "/\" b))

 proof

 (b "/\" a) <= (a "/\" b);

 then (b "/\" a) < (a "/\" b) by Th5;

 hence thesis by Def4;

 end;

 theorem :: NELSON_1:38

 (a "/\" ( - a)) <= (b "\/" ( - b))

 proof

 ( - (b "\/" ( - b))) = (( - b) "/\" ( - ( - b))) by Th1

 .= (b "/\" ( - b)) by ROBBINS3:def 6;

 then ( - (b "\/" ( - b))) < ( - (a "/\" ( - a))) by Def13;

 hence thesis by Def13, Th5;

 end;



 Lm4: ((( - a) "\/" ( - b)) "/\" a) < ( - b)

 proof

 (( - b) "/\" a) <= ( - b) by LATTICES: 4, LATTICES: 6;

 then

 A1: (( - b) "/\" a) < ( - b) by Th5;

 (( - a) "/\" a) < ( - b) by Def13;

 then ((( - a) "/\" a) "\/" (( - b) "/\" a)) < (( - b) "\/" ( - b)) by A1, Lm2;

 hence thesis by LATTICES:def 11;

 end;



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

 proof

 ((( - a) "\/" ( - b)) "/\" a) < ( - b) by Lm4;

 then a < ((( - a) "\/" ( - b)) => ( - b)) by Def4;

 hence thesis by Th8;

 end;



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

 proof



 A1: ((( - b) "\/" ( - a)) "/\" b) < ( - a) by Lm4;

 then

 A2: (( - (a "/\" b)) "/\" b) < ( - a) by Th8;

 ( - (( - (a "/\" b)) => ( - b))) < (( - (a "/\" b)) "/\" ( - ( - b))) by Def10;

 then ( - (( - (a "/\" b)) => ( - b))) < (( - (a "/\" b)) "/\" b) by ROBBINS3:def 6;

 then

 A3: ( - (( - (a "/\" b)) => ( - b))) < ( - a) by A2, Def3;



 A4: (b "/\" ( - (b "/\" a))) < ( - a) by A1, Th8;

 ( - (b => (a "/\" b))) < (b "/\" ( - (a "/\" b))) by Def10;

 then

 A5: ( - (b => (a "/\" b))) < ( - a) by A4, Def3;

 ( - (b =-> (a "/\" b))) = (( - (( - (a "/\" b)) => ( - b))) "\/" ( - (b => (a "/\" b)))) by Th8;

 hence thesis by A3, A5, Def7;

 end;

 theorem :: NELSON_1:39

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

 proof



 A1: a < (b => (b "/\" a)) & a < (( - (b "/\" a)) => ( - b)) by Lm5, Th19bis;

 ( - (b =-> (b "/\" a))) < ( - a) by Lm6;

 hence thesis by A1, Th5, Def8;

 end;

 theorem :: NELSON_1:40



 Th20: (a => ( ! b)) = (b => ( ! a))

 proof

 (a => ( ! b)) = (a => (b => ( - ( Top L)))) by Def14

 .= (b => (a => ( - ( Top L)))) by Th18

 .= (b => ( ! a)) by Def14;

 hence thesis;

 end;

 theorem :: NELSON_1:41



 Th21: (a => ( Top L)) = ( Top L)

 proof

 a <= ( Top L) by LATTICES: 4, LATTICES: 19;

 then a < ( Top L) by Th5;

 hence thesis;

 end;

 theorem :: NELSON_1:42



 Th22: (( Bottom L) => a) = ( Top L)

 proof

 ( Bottom L) <= a;

 then ( Bottom L) < a by Th5;

 hence thesis;

 end;

 theorem :: NELSON_1:43



 Th23: (( Top L) => b) = b

 proof

 (b "/\" ( Top L)) b) by Def4;

 ( - (( Top L) => b)) < (( Top L) "/\" ( - b)) by Def10;

 then

 A2: b <= (( Top L) => b) by A1, Th5;



 A3: (( Top L) "/\" (( Top L) => b)) b)) by Def9;

 then (( Top L) => b) <= b by Th5, A3;

 hence thesis by A2, Th3;

 end;

 theorem :: NELSON_1:44

 a = ( Top L) & (a => b) = ( Top L) implies b = ( Top L) by Th23;

 theorem :: NELSON_1:45



 Th24: (a => (b => a)) = ( Top L)

 proof

 (b "/\" a) <= a by LATTICES: 4, LATTICES: 6;

 then (b "/\" a) < a by Th5;

 then a < (b => a) by Def4;

 hence thesis;

 end;

 theorem :: NELSON_1:46



 Th25: ((a => (b => c)) => ((a => b) => (a => c))) = ( Top L)

 proof

 (a "/\" (a => b)) b)) "/\" (a => (b => c))) < (b "/\" (a => (b => c))) by Lm1;

 then ((a "/\" (a => b)) "/\" (a => (b => c))) < (b "/\" (b => (a => c))) by Th18;

 then

 A1: ((a "/\" (a => b)) "/\" (b => (a => c))) < (b "/\" (b => (a => c))) by Th18;



 A2: (b "/\" (b => (a => c))) < (a => c) by Th17;

 ((a "/\" (a => b)) "/\" (b => (a => c))) < (a => c) by Def3, A1, A2;

 then (a "/\" ((a "/\" (a => b)) "/\" (b => (a => c)))) < c by Def4;

 then (a "/\" (a "/\" ((a => b) "/\" (b => (a => c))))) < c by LATTICES:def 7;

 then ((a "/\" a) "/\" ((a => b) "/\" (b => (a => c)))) < c by LATTICES:def 7;

 then (a "/\" ((a => b) "/\" (a => (b => c)))) < c by Th18;

 then ((a => b) "/\" (a => (b => c))) < (a => c) by Def4;

 then (a => (b => c)) < ((a => b) => (a => c)) by Def4;

 hence thesis;

 end;

 theorem :: NELSON_1:47



 Th26: (a => (a "\/" b)) = ( Top L)

 proof

 a < (a "\/" b) by Th7;

 hence thesis;

 end;

 theorem :: NELSON_1:48



 Th27: (b => (a "\/" b)) = ( Top L)

 proof

 b < (a "\/" b) by Th7;

 hence thesis;

 end;

 theorem :: NELSON_1:49



 Th28: ((a => c) => ((b => c) => ((a "\/" b) => c))) = ( Top L)

 proof



 A1: (a "/\" (a => c)) < c by Th17;



 A2: (b "/\" (b => c)) < c by Th17;

 ((a "/\" (a => c)) "/\" (b => c)) < (a "/\" (a => c)) by Th6;

 then

 A3: ((a "/\" (a => c)) "/\" (b => c)) < c by A1, Def3;

 ((b "/\" (b => c)) "/\" (a => c)) < (b "/\" (b => c)) by Th6;

 then ((b "/\" (b => c)) "/\" (a => c)) < c by A2, Def3;

 then (((a "/\" (a => c)) "/\" (b => c)) "\/" ((b "/\" (b => c)) "/\" (a => c))) < c by Def7, A3;

 then ((a "/\" ((a => c) "/\" (b => c))) "\/" ((b "/\" (b => c)) "/\" (a => c))) < c by LATTICES:def 7;

 then ((a "/\" ((a => c) "/\" (b => c))) "\/" (b "/\" ((b => c) "/\" (a => c)))) < c by LATTICES:def 7;

 then (((b => c) "/\" (a => c)) "/\" (a "\/" b)) < c by LATTICES:def 11;

 then ((b => c) "/\" (a => c)) < ((a "\/" b) => c) by Def4;

 then (a => c) < ((b => c) => ((a "\/" b) => c)) by Def4;

 hence thesis;

 end;

 theorem :: NELSON_1:50



 Th29: ((a "/\" b) => a) = ( Top L)

 proof

 (a "/\" b) < a by Th6;

 hence thesis;

 end;

 theorem :: NELSON_1:51



 Th30: ((a "/\" b) => b) = ( Top L)

 proof

 (a "/\" b) b) => ((a => c) => (a => (b "/\" c)))) = ( Top L)

 proof



 A1: (a "/\" (a => c)) < c by Th17;



 A2: (a "/\" (a => b)) c)) "/\" (a "/\" (a => b))) < (c "/\" b) by Lm2, A1, A2;

 then ((((a => c) "/\" a) "/\" a) "/\" (a => b)) < (c "/\" b) by LATTICES:def 7;

 then (((a => c) "/\" (a "/\" a)) "/\" (a => b)) < (c "/\" b) by LATTICES:def 7;

 then (a "/\" ((a => c) "/\" (a => b))) < (b "/\" c) by LATTICES:def 7;

 then ((a => c) "/\" (a => b)) < (a => (b "/\" c)) by Def4;

 then (a => b) < ((a => c) => (a => (b "/\" c))) by Def4;

 hence thesis;

 end;

 theorem :: NELSON_1:53



 Th32: ((a => ( ! b)) => (b => ( ! a))) = ( Top L)

 proof

 (a => ( ! b)) = (b => ( ! a)) by Th20;

 hence thesis by Th16ter;

 end;

 theorem :: NELSON_1:54



 Th33: (( ! (a => a)) => b) = ( Top L)

 proof



 A1: (a => a) = ( Top L) by Th16ter;



 A2: ( ! ( Top L)) = (( Top L) => ( - ( Top L))) by Def14;

 (( ! (a => a)) => b) = ((( Top L) => ( Bottom L)) => b) by Th2, A2, A1

 .= (( Bottom L) => b) by Th23

 .= ( Top L) by Th22;

 hence thesis;

 end;

 theorem :: NELSON_1:55



 Th34: (( - a) => (a => b)) = ( Top L)

 proof

 (a "/\" ( - a)) b) by Def4;

 hence thesis;

 end;

 theorem :: NELSON_1:56



 Th35: ((( - (a => b)) => (a "/\" ( - b))) "/\" ((a "/\" ( - b)) => ( - (a => b)))) = ( Top L)

 proof



 A1: ( - (a => b)) < (a "/\" ( - b)) by Def10;

 (a "/\" ( - b)) < ( - (a => b)) by Def9;

 hence thesis by A1;

 end;

 theorem :: NELSON_1:57



 Th36: ((( - ( ! a)) => a) "/\" (a => ( - ( ! a)))) = ( Top L)

 proof



 A1: ( - ( ! a)) < a by Def12;

 a < ( - ( ! a)) by Def11;

 hence thesis by A1;

 end;

 theorem :: NELSON_1:58

 ( - ( - a)) = a by ROBBINS3:def 6;

 theorem :: NELSON_1:59



 Th37: ( - (a "\/" b)) = (( - a) "/\" ( - b))

 proof

 ((a "\/" b) ` ) = ((((a ` ) ` ) "\/" b) ` ) by ROBBINS3:def 6

 .= ((((a ` ) ` ) "\/" ((b ` ) ` )) ` ) by ROBBINS3:def 6

 .= ((((a ` ) "/\" (b ` )) ` ) ` ) by Def1

 .= ((a ` ) "/\" (b ` )) by ROBBINS3:def 6;

 hence thesis;

 end;

 theorem :: NELSON_1:60

 ( - (a "/\" b)) = (( - a) "\/" ( - b))

 proof

 ((a "/\" b) ` ) = ((((a ` ) ` ) "/\" b) ` ) by ROBBINS3:def 6

 .= ((((a ` ) ` ) "/\" ((b ` ) ` )) ` ) by ROBBINS3:def 6

 .= ((((a ` ) "\/" (b ` )) ` ) ` ) by Th1

 .= ((a ` ) "\/" (b ` )) by ROBBINS3:def 6;

 hence thesis;

 end;

 theorem :: NELSON_1:61



 Th38: a c) < (a => c) & (c => a) < (c => b)

 proof

 assume

 A1: a < 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 thesis by A1, A2, A3, A4, Th23, Def3;

 end;

 theorem :: NELSON_1:62

 ((a => b) => ((c => d) => ((a "/\" c) => (b "/\" d)))) = ( Top L)

 proof



 A1: (a "/\" (a => b)) d)) < d by Th17;

 then ((c "/\" (c => d)) "/\" (a "/\" (a => b))) < (b "/\" d) by Lm2, A1;

 then (((c "/\" (c => d)) "/\" a) "/\" (a => b)) < (d "/\" b) by LATTICES:def 7;

 then (((a "/\" c) "/\" (c => d)) "/\" (a => b)) < (b "/\" d) by LATTICES:def 7;

 then ((a "/\" c) "/\" ((c => d) "/\" (a => b))) < (b "/\" d) by LATTICES:def 7;

 then ((c => d) "/\" (a => b)) < ((a "/\" c) => (b "/\" d)) by Def4;

 then (a => b) < ((c => d) => ((a "/\" c) => (b "/\" d))) by Def4;

 hence thesis;

 end;

 theorem :: NELSON_1:63

 ((a => b) => ((c => d) => ((a "\/" c) => (b "\/" d)))) = ( Top L)

 proof

 ((c => d) "/\" (a => b)) < (a => b) by Th6;

 then

 A1: (((c => d) "/\" (a => b)) "/\" a) d) "/\" (a => b)) < (c => d) by Th6;

 then (c "/\" ((c => d) "/\" (a => b))) < d by Def4;

 then ((((c => d) "/\" (a => b)) "/\" a) "\/" (((c => d) "/\" (a => b)) "/\" c)) < (b "\/" d) by Lm2, A1;

 then (((c => d) "/\" (a => b)) "/\" (a "\/" c)) < (b "\/" d) by LATTICES:def 11;

 then ((c => d) "/\" (a => b)) < ((a "\/" c) => (b "\/" d)) by Def4;

 then (a => b) < ((c => d) => ((a "\/" c) => (b "\/" d))) by Def4;

 hence thesis;

 end;

 theorem :: NELSON_1:64

 ((b => a) => ((c => d) => ((a => c) => (b => d)))) = ( Top L)

 proof



 A1: (c "/\" (c => d)) < d by Th17;

 (a "/\" (a => c)) < c by Th17;

 then ((a "/\" (a => c)) "/\" (c => d)) < (c "/\" (c => d)) by Lm1;

 then

 A2: ((a "/\" (a => c)) "/\" (c => d)) < d by Def3, A1;

 (b "/\" (b => a)) < a by Th17;

 then ((a => c) "/\" (b "/\" (b => a))) < ((a => c) "/\" a) & ((a => c) "\/" (b "/\" (b => a))) < ((a => c) "\/" a) by Lm1;

 then (((a => c) "/\" (b "/\" (b => a))) "/\" (c => d)) < (((a => c) "/\" a) "/\" (c => d)) by Lm1;

 then (((a => c) "/\" (b "/\" (b => a))) "/\" (c => d)) < d by A2, Def3;

 then (((a => c) "/\" (c => d)) "/\" (b "/\" (b => a))) < d by LATTICES:def 7;

 then ((((a => c) "/\" (c => d)) "/\" b) "/\" (b => a)) < d by LATTICES:def 7;

 then ((((a => c) "/\" b) "/\" (c => d)) "/\" (b => a)) < d by LATTICES:def 7;

 then ((b "/\" (a => c)) "/\" ((c => d) "/\" (b => a))) < d by LATTICES:def 7;

 then (b "/\" ((a => c) "/\" ((c => d) "/\" (b => a)))) < d by LATTICES:def 7;

 then ((a => c) "/\" ((c => d) "/\" (b => a))) < (b => d) by Def4;

 then ((c => d) "/\" (b => a)) < ((a => c) => (b => d)) by Def4;

 then (b => a) < ((c => d) => ((a => c) => (b => d))) by Def4;

 hence thesis;

 end;

 begin

 definition

 let L be non empty NelsonStr;

 :: NELSON_1:def22

 attr L is satisfying_N0* means for a,b be Element of L holds a <= b iff (a =-> b) = ( Top L);

 :: NELSON_1:def23

 attr L is satisfying_N1* means for a,b be Element of L holds (a => (b => a)) = ( Top L);

 :: NELSON_1:def24

 attr L is satisfying_N2* means for a,b,c be Element of L holds ((a => (b => c)) => ((a => b) => (a => c))) = ( Top L);

 :: NELSON_1:def25

 attr L is satisfying_N3* means for a be Element of L holds (( Top L) => a) = a;

 :: NELSON_1:def26

 attr L is satisfying_N5* means for a,b be Element of L holds ((a =-> b) => ((b =-> a) => b)) = ((b =-> a) => ((a =-> b) => a));

 :: NELSON_1:def27

 attr L is satisfying_N6* means for a,b be Element of L holds (a => (a "\/" b)) = ( Top L);

 :: NELSON_1:def28

 attr L is satisfying_N7* means for a,b be Element of L holds (b => (a "\/" b)) = ( Top L);

 :: NELSON_1:def29

 attr L is satisfying_N8* means for a,b,c be Element of L holds ((a => c) => ((b => c) => ((a "\/" b) => c))) = ( Top L);

 :: NELSON_1:def30

 attr L is satisfying_N9* means for a,b be Element of L holds ((a "/\" b) => a) = ( Top L);

 :: NELSON_1:def31

 attr L is satisfying_N10* means for a,b be Element of L holds ((a "/\" b) => b) = ( Top L);

 :: NELSON_1:def32

 attr L is satisfying_N11* means for a,b,c be Element of L holds ((a => b) => ((a => c) => (a => (b "/\" c)))) = ( Top L);

 :: NELSON_1:def33

 attr L is satisfying_N12* means for a,b be Element of L holds ((a => ( ! b)) => (b => ( ! a))) = ( Top L);

 :: NELSON_1:def34

 attr L is satisfying_N13* means for a,b be Element of L holds (( ! (a => a)) => b) = ( Top L);

 :: NELSON_1:def35

 attr L is satisfying_N14* means for a,b be Element of L holds (( - a) => (a => b)) = ( Top L);

 :: NELSON_1:def36

 attr L is satisfying_N15* means for a,b be Element of L holds ((( - (a => b)) => (a "/\" ( - b))) "/\" ((a "/\" ( - b)) => ( - (a => b)))) = ( Top L);

 :: NELSON_1:def37

 attr L is satisfying_N17* means for a,b be Element of L holds ( - (a "\/" b)) = (( - a) "/\" ( - b));

 :: NELSON_1:def38

 attr L is satisfying_N19* means for a be Element of L holds ((( - ( ! a)) => a) "/\" (a => ( - ( ! a)))) = ( Top L);

 end

 notation

 let L be non empty NelsonStr;

 synonym L is satisfying_N4* for L is satisfying_N4;

 synonym L is satisfying_N16* for L is DeMorgan;

 synonym L is satisfying_N18* for L is involutive;

 end

 registration

 cluster -> satisfying_N1* satisfying_N2* satisfying_N3* satisfying_N4* satisfying_N5* satisfying_N6* satisfying_N7* satisfying_N8* satisfying_N9* satisfying_N10* satisfying_N11* satisfying_N12* satisfying_N13* satisfying_N14* satisfying_N15* satisfying_N16* satisfying_N17* satisfying_N18* satisfying_N19* for Nelson_Algebra;

 coherence

 proof

 let L be Nelson_Algebra;

 thus L is satisfying_N1* by Th24;

 thus L is satisfying_N2* by Th25;

 thus L is satisfying_N3* by Th23;

 thus L is satisfying_N4*;

 thus L is satisfying_N5*

 proof

 now

 let a,b be Element of L;

 set ab = (a =-> b);

 set ba = (b =-> a);



 A1: (ab => (ba => b)) < (ba => (ab => a))

 proof



 A2: b < ((b => a) => a) by Th19;



 A3: ((b => a) => a) < ((( - a) => ( - b)) => ((b => a) => a)) by Th24;



 A4: ((( - a) => ( - b)) => ((b => a) => a)) = (((( - a) => ( - b)) "/\" (b => a)) => a) by Lm3;

 b < (ba => a) by Def3, A2, A3, A4;

 then (ba => b) < (ba => (ba => a)) by Th38;

 then (ab => ((b =-> a) => b)) < (ab => (ba => (ba => a))) by Th38;

 then (ab => (ba => b)) < ((a =-> b) => ((ba "/\" ba) => a)) by Lm3;

 hence thesis by Th18;

 end;



 A5: (( - a) "/\" (( - a) => ( - b))) < ( - b) by Th17;



 A6: ( - (ba => (ab => a))) < ( - (ab => (ba => b)))

 proof



 A7: (ab "/\" ba) < (ab "/\" ba) by Def2;

 ((ab "/\" ba) "/\" (( - a) "/\" (( - a) => ( - b)))) = (((ab "/\" (b => a)) "/\" (( - a) => ( - b))) "/\" (( - a) "/\" (( - a) => ( - b)))) by LATTICES:def 7

 .= ((((ab "/\" (b => a)) "/\" (( - a) => ( - b))) "/\" (( - a) => ( - b))) "/\" ( - a)) by LATTICES:def 7

 .= (((ab "/\" (b => a)) "/\" ((( - a) => ( - b)) "/\" (( - a) => ( - b)))) "/\" ( - a)) by LATTICES:def 7

 .= ((ab "/\" ((b => a) "/\" (( - a) => ( - b)))) "/\" ( - a)) by LATTICES:def 7

 .= (ab "/\" (ba "/\" ( - a))) by LATTICES:def 7;

 then

 A8: (ab "/\" (ba "/\" ( - a))) < ((ab "/\" ba) "/\" ( - b)) by A7, Lm2, A5;

 ( - (ba => a)) < (ba "/\" ( - a)) by Def10;

 then

 A9: (ab "/\" ( - (ba => a))) < (ab "/\" (ba "/\" ( - a))) by Lm1;



 A10: ( - (ab => (ba => a))) < (ab "/\" ( - (ba => a))) by Def10;

 (ba "/\" ( - b)) < ( - (ba => b)) by Def9;

 then

 A11: (ab "/\" (ba "/\" ( - b))) < (ab "/\" ( - (ba => b))) by Lm1;

 (ab "/\" ( - (ba => b))) < ( - (ab => (ba => b))) by Def9;

 then (ab "/\" (ba "/\" ( - b))) < ( - (ab => (ba => b))) by Def3, A11;

 then ((ab "/\" ba) "/\" ( - b)) < ( - (ab => (ba => b))) by LATTICES:def 7;

 then (ab "/\" (ba "/\" ( - a))) < ( - (ab => (ba => b))) by Def3, A8;

 then (ab "/\" ( - (ba => a))) < ( - (ab => (ba => b))) by Def3, A9;

 then ( - (ab => (ba => a))) < ( - (ab => (ba => b))) by Def3, A10;

 hence thesis by Th18;

 end;



 A12: (ba => (ab => a)) < (ab => (ba => b))

 proof



 A13: a < ((a => b) => b) by Th19;



 A14: ((a => b) => b) < ((( - b) => ( - a)) => ((a => b) => b)) by Th24;



 A15: ((( - b) => ( - a)) => ((a => b) => b)) = (((( - b) => ( - a)) "/\" (a => b)) => b) by Lm3;

 a < (ab => b) by Def3, A13, A14, A15;

 then (ab => a) < (ab => (ab => b)) by Th38;

 then (ba => (ab => a)) < (ba => (ab => (ab => b))) by Th38;

 then (ba => (ab => a)) < (ba => ((ab "/\" ab) => b)) by Lm3;

 hence thesis by Th18;

 end;



 A16: ( - (ab => (ba => b))) < ( - (ba => (ab => a)))

 proof



 A17: (( - b) "/\" (( - b) => ( - a))) < ( - a) by Th17;



 A18: (ba "/\" ab) < (ba "/\" ab) by Def2;

 ((ba "/\" ab) "/\" (( - b) "/\" (( - b) => ( - a)))) = (((ba "/\" (a => b)) "/\" (( - b) => ( - a))) "/\" (( - b) "/\" (( - b) => ( - a)))) by LATTICES:def 7

 .= ((((ba "/\" (a => b)) "/\" (( - b) => ( - a))) "/\" (( - b) => ( - a))) "/\" ( - b)) by LATTICES:def 7

 .= (((ba "/\" (a => b)) "/\" ((( - b) => ( - a)) "/\" (( - b) => ( - a)))) "/\" ( - b)) by LATTICES:def 7

 .= ((ba "/\" ((a => b) "/\" (( - b) => ( - a)))) "/\" ( - b)) by LATTICES:def 7

 .= (ba "/\" (ab "/\" ( - b))) by LATTICES:def 7;

 then

 A19: (ba "/\" (ab "/\" ( - b))) < ((ba "/\" ab) "/\" ( - a)) by A18, Lm2, A17;

 ( - (ab => b)) < (ab "/\" ( - b)) by Def10;

 then

 A20: (ba "/\" ( - (ab => b))) < (ba "/\" (ab "/\" ( - b))) by Lm1;



 A21: ( - (ba => (ab => b))) < (ba "/\" ( - (ab => b))) by Def10;

 (ab "/\" ( - a)) < ( - (ab => a)) by Def9;

 then

 A22: (ba "/\" (ab "/\" ( - a))) < (ba "/\" ( - (ab => a))) by Lm1;

 (ba "/\" ( - (ab => a))) < ( - (ba => (ab => a))) by Def9;

 then (ba "/\" (ab "/\" ( - a))) < ( - (ba => (ab => a))) by Def3, A22;

 then ((ba "/\" ab) "/\" ( - a)) < ( - (ba => (ab => a))) by LATTICES:def 7;

 then (ba "/\" (ab "/\" ( - b))) < ( - (ba => (ab => a))) by Def3, A19;

 then (ba "/\" ( - (ab => b))) < ( - (ba => (ab => a))) by Def3, A20;

 then ( - (ba => (ab => b))) < ( - (ba => (ab => a))) by Def3, A21;

 hence thesis by Th18;

 end;



 A23: (ab => (ba => b)) <= (ba => (ab => a)) by A6, A1, Th5;

 (ba => (ab => a)) <= (ab => (ba => b)) by A12, A16, Th5;

 hence (ab => (ba => b)) = (ba => (ab => a)) by A23, Th3;

 end;

 hence thesis;

 end;

 thus L is satisfying_N6* by Th26;

 thus L is satisfying_N7* by Th27;

 thus L is satisfying_N8* by Th28;

 thus L is satisfying_N9* by Th29;

 thus L is satisfying_N10* by Th30;

 thus L is satisfying_N11* by Th31;

 thus L is satisfying_N12* by Th32;

 thus L is satisfying_N13* by Th33;

 thus L is satisfying_N14* by Th34;

 thus L is satisfying_N15* by Th35;

 thus L is satisfying_N16*;

 thus L is satisfying_N17* by Th37;

 thus L is satisfying_N18*;

 thus L is satisfying_N19* by Th36;

 end;

 end

 theorem :: NELSON_1:65

 for L be non empty NelsonStr st L is satisfying_N0* holds L is Nelson_Algebra iff L is satisfying_N1* satisfying_N2* satisfying_N3* satisfying_N4* satisfying_N5* satisfying_N6* satisfying_N7* satisfying_N8* satisfying_N9* satisfying_N10* satisfying_N11* satisfying_N12* satisfying_N13* satisfying_N14* satisfying_N15* satisfying_N16* satisfying_N17* satisfying_N18* satisfying_N19*

 proof

 let L be non empty NelsonStr;

 assume

 A1: L is satisfying_N0*;

 thus L is Nelson_Algebra implies L is satisfying_N1* satisfying_N2* satisfying_N3* satisfying_N4* satisfying_N5* satisfying_N6* satisfying_N7* satisfying_N8* satisfying_N9* satisfying_N10* satisfying_N11* satisfying_N12* satisfying_N13* satisfying_N14* satisfying_N15* satisfying_N16* satisfying_N17* satisfying_N18* satisfying_N19*;

 assume

 A2: L is satisfying_N1* satisfying_N2* satisfying_N3* satisfying_N4* satisfying_N5* satisfying_N6* satisfying_N7* satisfying_N8* satisfying_N9* satisfying_N10* satisfying_N11* satisfying_N12* satisfying_N13* satisfying_N14* satisfying_N15* satisfying_N16* satisfying_N17* satisfying_N18* satisfying_N19*;

 then

 reconsider L1 = L as DeMorgan non empty NelsonStr;



 A3: for a,b be Element of L1 holds (a "/\" b) = ( Top L1) implies a = ( Top L1) & b = ( Top L1)

 proof

 let a,b be Element of L1;

 assume (a "/\" b) = ( Top L1);

 then ( Top L1) < a & ( Top L1) w) = w by A2;

 then (w => ((w => w) => (w => (w "/\" w)))) = w by A2;

 then (w => (w => (w "/\" w))) = w by A4, A2;

 then (w => (w "/\" w)) = w by A2;

 then

 A5: (w "/\" w) = w by A2;



 A6: for a,b be Element of L1 holds a <= b iff a b) = ((a => b) "/\" (( - b) => ( - a))) by A2;

 thus a <= b implies a b) = ( Top L1) by A1;

 hence thesis by A3, A7;

 end;

 assume a < b & ( - b) < ( - a);

 hence thesis by A7, A5, A1;

 end;

 set d = (( Top L) ` );



 A8: for a be Element of L holds a <= ( Top L)

 proof

 let a be Element of L;

 (a => ( Top L)) = (( Top L) => (a => ( Top L))) by A2;

 then

 A9: a < ( Top L) by A2;

 (( - ( Top L)) => (( Top L) => ( - a))) = ( Top L) by A2;

 then ( - ( Top L)) < ( - a) by A2;

 hence thesis by A6, A9;

 end;



 A10: for a be Element of L holds d <= a

 proof

 let a be Element of L;

 (( - ( Top L)) => (( Top L) => a)) = ( Top L) by A2;

 then

 A11: ( - ( Top L)) < a by A2;

 ( - a) <= ( Top L) by A8;

 then ( - a) < ( Top L) by A2;

 then ( - a) < ( - d) by A2;

 hence thesis by A11, A6;

 end;



 A12: for a be Element of L holds (d "/\" a) = d

 proof

 let a be Element of L;

 d <= a by A10;

 hence thesis;

 end;



 A13: for a be Element of L1 holds (a => ( Top L1)) = ( Top L1)

 proof

 let a be Element of L1;

 (( Top L1) => (a => ( Top L1))) = ( Top L1) by A2;

 hence thesis by A2;

 end;



 A14: for a,b,c be Element of L1 holds (a => b) = ( Top L1) & (b => c) = ( Top L1) implies (a => c) = ( Top L1)

 proof

 let a,b,c be Element of L1;

 assume

 A15: (a => b) = ( Top L1) & (b => c) = ( Top L1);

 (a => c) = (( Top L1) => (a => c)) by A2

 .= (( Top L1) => (( Top L1) => (a => c))) by A2

 .= ((a => ( Top L1)) => (( Top L1) => (a => c))) by A13

 .= ( Top L1) by A2, A15;

 hence thesis;

 end;



 A16: L1 is satisfying_A1b

 proof

 let a,b,c be Element of L1;

 assume a c) => ((b => c) => ((a "\/" b) => c))) = ( Top L1) by A2;

 then ((b => c) => ((a "\/" b) => c)) = ( Top L1) by A18, A2;

 hence thesis by A2, A18;

 end;



 A19: for a be Element of L1 holds (a => a) = ( Top L1)

 proof

 let a be Element of L1;



 A20: ((a => ((a => a) => a)) => ((a => (a => a)) => (a => a))) = ( Top L1) by A2;

 (a => ((a => a) => a)) = ( Top L1) by A2;

 then

 A21: ((a => (a => a)) => (a => a)) = ( Top L1) by A20, A2;

 (a => (a => a)) = ( Top L1) by A2;

 hence thesis by A21, A2;

 end;



 A22: L1 is satisfying_N7

 proof

 let a,b,c be Element of L1;

 assume

 A23: a b) => ((a => c) => (a => (b "/\" c)))) = ( Top L1) by A2;

 then ((a => c) => (a => (b "/\" c))) = ( Top L1) by A23, A2;

 hence thesis by A2, A23;

 end;



 A24: for a,b be Element of L1 holds b < (a "\/" b) by A2;



 A25: for a,b be Element of L1 holds (a "/\" b) <= a

 proof

 let a,b be Element of L1;



 A26: ( - (a "/\" b)) = (( - a) "\/" ( - b)) by A2;



 A27: (a "/\" b) < a by A2;

 ( - a) < (( - a) "\/" ( - b)) by A2;

 hence thesis by A27, A6, A26;

 end;



 A28: for a,b be Element of L1 holds a <= (a "\/" b)

 proof

 let a,b be Element of L1;



 A29: (( - a) "/\" ( - b)) < ( - a) by A2;



 A30: a < (a "\/" b) by A2;

 ( - (a "\/" b)) = (( - a) "/\" ( - b)) by A2;

 hence thesis by A29, A30, A6;

 end;



 A31: for a,b be Element of L1 holds b <= (a "\/" b)

 proof

 let a,b be Element of L1;



 A32: b < (a "\/" b) by A2;



 A33: ( - (a "\/" b)) = (( - a) "/\" ( - b)) by A2;

 (( - a) "/\" ( - b)) < ( - b) by A2;

 hence thesis by A6, A32, A33;

 end;



 A34: for a,b be Element of L1 holds (a "/\" b) <= b

 proof

 let a,b be Element of L1;



 A35: ( - (a "/\" b)) = (( - a) "\/" ( - b)) by A2;



 A36: (a "/\" b) a) = ( Top L1)

 proof

 let a be Element of L1;

 (a =-> a) = ((a => a) "/\" (( - a) => ( - a))) by A2

 .= (( Top L1) "/\" (( - a) => ( - a))) by A19

 .= ( Top L1) by A19, A5;

 hence thesis;

 end;



 A38: for a,b be Element of L1 holds a = b iff (a =-> b) = ( Top L1) & (b =-> a) = ( Top L1)

 proof

 let a,b be Element of L1;

 (a =-> b) = ( Top L1) & (b =-> a) = ( Top L) implies a = b

 proof

 assume

 A39: (a =-> b) = ( Top L1) & (b =-> a) = ( Top L);

 then ((b =-> a) => ((a =-> b) => a)) = (( Top L1) => ((b =-> a) => b)) by A2;

 then ((b =-> a) => ((a =-> b) => a)) = (( Top L1) => b) by A2, A39;

 then ((b =-> a) => (( Top L1) => a)) = b by A39, A2;

 then (( Top L1) => a) = b by A39, A2;

 hence thesis by A2;

 end;

 hence thesis by A37;

 end;



 A40: for a,b be Element of L1 holds a <= b & b <= a iff a = b

 proof

 let a,b be Element of L1;

 thus a <= b & b <= a implies a = b

 proof

 assume a <= b & b <= a;

 then (a =-> b) = ( Top L) & (b =-> a) = ( Top L) by A1;

 hence thesis by A38;

 end;

 assume a = b;

 then (a =-> b) = ( Top L) & (b =-> a) = ( Top L) by A38;

 hence thesis by A1;

 end;



 A41: for b be Element of L1 holds ( Top L1) < b implies b = ( Top L1) by A2;



 A42: L1 is satisfying_A1

 proof

 let a be Element of L1;

 thus thesis by A19;

 end;



 A43: for a,b,c be Element of L1 holds a c) < (a => c) & (c => a) < (c => b)

 proof

 let a,b,c be Element of L1;

 assume

 A44: a < b;



 A45: (b => c) < (a => (b => c)) by A2;

 (a => (b => c)) < ((a => b) => (a => c)) by A2;

 then

 A46: (b => c) < ((a => b) => (a => c)) by A45, A16;

 ((c => ( Top L1)) => ((c => a) => (c => b))) = ( Top L1) by A2, A44;

 then (( Top L1) => ((c => a) => (c => b))) = ( Top L1) by A13;

 hence thesis by A46, A2, A44;

 end;



 A47: for a,b be Element of L1 holds (a => (b => (a "/\" b))) = ( Top L1)

 proof

 let a,b be Element of L1;

 (b => a) < ((b => b) => (b => (a "/\" b))) by A2;

 then (b => a) < (( Top L1) => (b => (a "/\" b))) by A19;

 then (b => a) < (b => (a "/\" b)) by A2;

 then (a => (b => a)) < (a => (b => (a "/\" b))) by A43;

 then ( Top L1) < (a => (b => (a "/\" b))) by A2;

 hence thesis by A2;

 end;



 A48: for a,b,c be Element of L1 st a < (b => c) holds b < (a => c)

 proof

 let a,b,c be Element of L1;

 assume

 A49: a < (b => c);

 (a => (b => c)) < ((a => b) => (a => c)) by A2;

 then

 A50: (a => b) < (a => c) by A2, A49;

 b < (a => b) by A2;

 hence thesis by A50, A16;

 end;



 A51: for a,c be Element of L1 holds (a => (a => c)) < (a => c)

 proof

 let a,c be Element of L1;

 (a => (a => c)) < ((a => a) => (a => c)) by A2;

 then (a => (a => c)) < (( Top L1) => (a => c)) by A19;

 hence thesis by A2;

 end;



 A52: L1 is satisfying_N3

 proof

 let x,a,b be Element of L1;



 A53: (a "/\" x) b)

 proof

 assume (a "/\" x) < b;

 then (x => (a "/\" x)) < (x => b) by A43;

 then

 A54: (a => (x => (a "/\" x))) < (a => (x => b)) by A43;

 (a => (x => (a "/\" x))) = ( Top L1) by A47;

 then a < (x => b) by A2, A54;

 hence thesis by A48;

 end;

 x < (a => b) implies (a "/\" x) b);

 (a "/\" x) < x by A2;

 then (a "/\" x) < (a => b) by A55, A16;

 then

 A56: a < ((a "/\" x) => b) by A48;

 (a "/\" x) < a by A2;

 then (a "/\" x) < ((a "/\" x) => b) by A16, A56;

 hence thesis by A41, A51;

 end;

 hence thesis by A53;

 end;



 A57: for a,b,c be Element of L1 st b < c holds (a "/\" b) < (a "/\" c)

 proof

 let a,b,c be Element of L1;

 assume

 A58: b < c;

 (a "/\" b) < b by A2;

 then

 A59: (a "/\" b) < c by A58, A16;

 (a "/\" b) < a by A2;

 hence thesis by A22, A59;

 end;



 A58: for a,b,c be Element of L1 st b < c holds (a "\/" b) < (a "\/" c)

 proof

 let a,b,c be Element of L1;

 assume

 A60: b < c;



 A61: a < (a "\/" c) by A2;

 c < (a "\/" c) by A2;

 then b < (a "\/" c) by A60, A16;

 hence thesis by A61, A17;

 end;



 A62: for a,b,c be Element of L1 st a <= c & b <= c holds (a "\/" b) <= c

 proof

 let a,b,c be Element of L1;

 assume

 A63: a <= c & b <= c;

 then

 A64: a < c & ( - c) < ( - a) by A6;



 A65: b < c & ( - c) < ( - b) by A63, A6;

 ((( - c) => ( - a)) => ((( - c) => ( - b)) => (( - c) => (( - a) "/\" ( - b))))) = ( Top L1) by A2;

 then ((( - c) => ( - b)) => (( - c) => (( - a) "/\" ( - b)))) = ( Top L1) by A64, A2;

 then (( - c) => (( - a) "/\" ( - b))) = ( Top L1) by A65, A2;

 then ( - c) < ( - (a "\/" b)) by A2;

 hence thesis by A65, A64, A17, A6;

 end;



 A66: for a,b,c be Element of L1 st c <= a & c <= b holds c <= (a "/\" b)

 proof

 let a,b,c be Element of L1;

 assume

 A67: c <= a & c <= b;

 then

 A68: c < a & ( - a) < ( - c) by A6;



 A69: c ( - c)) => ((( - b) => ( - c)) => ((( - a) "\/" ( - b)) => ( - c)))) = ( Top L1) by A2;

 then ((( - b) => ( - c)) => ((( - a) "\/" ( - b)) => ( - c))) = ( Top L1) by A68, A2;

 then ((( - a) "\/" ( - b)) => ( - c)) = ( Top L1) by A69, A2;

 then ( - (a "/\" b)) < ( - c) by A2;

 hence thesis by A69, A68, A22, A6;

 end;



 A70: for a,b be Element of L1 holds (b "\/" a) <= (a "\/" b)

 proof

 let a,b be Element of L1;



 A71: a <= (a "\/" b) by A28;

 b <= (a "\/" b) by A31;

 hence thesis by A71, A62;

 end;



 A72: for a,b be Element of L1 holds (a "\/" b) = (b "\/" a)

 proof

 let a,b be Element of L1;



 A73: (a "\/" b) <= (b "\/" a) by A70;

 (b "\/" a) <= (a "\/" b) by A70;

 hence thesis by A73, A40;

 end;



 A74: for a,b be Element of L1 holds (a "/\" b) <= (b "/\" a)

 proof

 let a,b be Element of L1;



 A75: (a "/\" b) <= a by A25;

 (a "/\" b) <= b by A34;

 hence thesis by A75, A66;

 end;

 for a,b be Element of L1 holds (a "/\" b) = (b "/\" a)

 proof

 let a,b be Element of L1;



 A76: (a "/\" b) <= (b "/\" a) by A74;

 (b "/\" a) <= (a "/\" b) by A74;

 hence thesis by A40, A76;

 end;

 then

 reconsider L1 as DeMorgan meet-commutative join-commutative non empty NelsonStr by A72, LATTICES:def 4, LATTICES:def 6;



 A77: for a,b,c be Element of L1 holds a <= b implies (a "\/" c) <= (b "\/" c)

 proof

 let a,b,c be Element of L1;

 assume a <= b;

 then

 A78: a < b & ( - b) < ( - a) by A6;

 then (( - b) "/\" ( - c)) < (( - a) "/\" ( - c)) by A57;

 then ( - (b "\/" c)) < (( - a) "/\" ( - c)) by A2;

 then ( - (b "\/" c)) < ( - (a "\/" c)) by A2;

 hence thesis by A78, A58, A6;

 end;

 set d = ( - ( Top L1));



 A79: for a be Element of L1 holds (d "/\" a) = d & (a "/\" d) = d by A12;

 for a,b be Element of L1 holds b = ((a "/\" b) "\/" b)

 proof

 let a,b be Element of L1;



 A80: b <= ((a "/\" b) "\/" b) by A31;

 (a "/\" b) <= b & b <= b by A40, A25;

 then ((a "/\" b) "\/" b) <= b by A62;

 hence thesis by A80, A40;

 end;

 then

 A81: L1 is meet-absorbing;

 for a,b be Element of L1 holds (a "/\" (a "\/" b)) = a

 proof

 let a,b be Element of L1;

 a <= a & a <= (a "\/" b) by A40, A31;

 hence thesis;

 end;

 then

 A82: L1 is join-absorbing;



 A83: for a,b,c be Element of L1 holds b <= c implies (a "/\" b) <= (a "/\" c)

 proof

 let a,b,c be Element of L1;

 assume

 A84: b <= c;

 then

 A85: (a "/\" b) < (a "/\" c) by A57, A6;

 ( - (a "/\" c)) < ( - (a "/\" b))

 proof

 ( - c) < ( - b) by A84, A6;

 then (( - a) "\/" ( - c)) < (( - a) "\/" ( - b)) by A58;

 then ( - (a "/\" c)) < (( - a) "\/" ( - b)) by A2;

 hence thesis by A2;

 end;

 hence thesis by A85, A6;

 end;



 A86: for a,b,c be Element of L1 st a <= b & b <= c holds a <= c

 proof

 let a,b,c be Element of L1;

 assume a <= b & b <= c;

 then a < b & b < c & ( - c) < ( - b) & ( - b) < ( - a) by A6;

 then a < c & ( - c) < ( - a) by A14;

 hence thesis by A6;

 end;



 A87: for a,b,c be Element of L1 holds (a "/\" (b "/\" c)) = ((a "/\" b) "/\" c)

 proof

 let a,b,c be Element of L1;



 A88: (a "/\" (b "/\" c)) <= (a "/\" b) by A34, A83;



 A89: (a "/\" (b "/\" c)) <= (b "/\" c) by A34;

 (b "/\" c) <= c by A34;

 then (a "/\" (b "/\" c)) <= c by A86, A89;

 then

 A90: (a "/\" (b "/\" c)) <= ((a "/\" b) "/\" c) by A88, A66;



 A91: (a "/\" b) <= a by A25;

 ((a "/\" b) "/\" c) <= (a "/\" b) by A25;

 then

 A92: ((a "/\" b) "/\" c) <= a by A91, A86;

 ((a "/\" b) "/\" c) <= (b "/\" c) by A25, A83;

 then ((a "/\" b) "/\" c) <= (a "/\" (b "/\" c)) by A92, A66;

 hence thesis by A90, A40;

 end;

 for a,b,c be Element of L1 holds (a "\/" (b "\/" c)) = ((a "\/" b) "\/" c)

 proof

 let a,b,c be Element of L1;



 A93: a <= (a "\/" b) by A28;

 (a "\/" b) <= ((a "\/" b) "\/" c) by A28;

 then

 A94: a <= ((a "\/" b) "\/" c) by A86, A93;

 (b "\/" c) <= ((a "\/" b) "\/" c) by A28, A77;

 then

 A95: (a "\/" (b "\/" c)) <= ((a "\/" b) "\/" c) by A94, A62;



 A96: c <= (b "\/" c) by A28;

 (b "\/" c) <= (a "\/" (b "\/" c)) by A28;

 then

 A97: c <= (a "\/" (b "\/" c)) by A96, A86;

 (a "\/" b) <= (a "\/" (b "\/" c)) by A28, A77;

 then ((a "\/" b) "\/" c) <= (a "\/" (b "\/" c)) by A97, A62;

 hence thesis by A95, A40;

 end;

 then L1 is join-associative meet-associative by A87;

 then

 reconsider L1 as Lattice-like lower-bounded DeMorgan non empty NelsonStr by A81, A79, A82, LATTICES:def 13;

 set c = ( Top L1);

 for a be Element of L1 holds (c "\/" a) = c & (a "\/" c) = c

 proof

 let a be Element of L1;

 a <= c by A8;

 hence thesis by LATTICES: 4, LATTICES:def 3;

 end;

 then L is upper-bounded;

 then

 reconsider L1 as DeMorgan involutive bounded Lattice-like non empty NelsonStr by A2;



 A98: L1 is distributive

 proof

 let a,b,c be Element of L1;



 A99: b < (a => ((a "/\" b) "\/" (a "/\" c))) by A52, A24;

 c < (a => ((a "/\" b) "\/" (a "/\" c))) by A52, A24;

 then

 A100: (b "\/" c) < (a => ((a "/\" b) "\/" (a "/\" c))) by A99, A17;



 A101: for a,b,c be Element of L1 holds (a "/\" (b "\/" c)) < ((a "/\" b) "\/" (a "/\" c))

 proof

 let a,b,c be Element of L1;



 A102: b < (a => ((a "/\" b) "\/" (a "/\" c))) by A52, A24;

 c < (a => ((a "/\" b) "\/" (a "/\" c))) by A52, A24;

 then (b "\/" c) < (a => ((a "/\" b) "\/" (a "/\" c))) by A102, A17;

 hence thesis by A52;

 end;



 A103: ((( - a) "\/" ( - b)) "/\" (( - a) "\/" ( - c))) < (((( - a) "\/" ( - b)) "/\" ( - a)) "\/" ((( - a) "\/" ( - b)) "/\" ( - c))) by A101;



 A104: (((( - a) "\/" ( - b)) "/\" ( - a)) "\/" ((( - a) "\/" ( - b)) "/\" ( - c))) = (( - a) "\/" ((( - a) "\/" ( - b)) "/\" ( - c))) by LATTICES:def 9;

 (( - a) "\/" (( - c) "/\" (( - a) "\/" ( - b)))) < (( - a) "\/" ((( - c) "/\" ( - a)) "\/" (( - c) "/\" ( - b)))) by A101, A58;

 then

 A105: ((( - a) "\/" ( - b)) "/\" (( - a) "\/" ( - c))) < (( - a) "\/" ((( - a) "/\" ( - c)) "\/" (( - b) "/\" ( - c)))) by A16, A103, A104;

 (( - a) "\/" ((( - a) "/\" ( - c)) "\/" (( - b) "/\" ( - c)))) = ((( - a) "\/" (( - a) "/\" ( - c))) "\/" (( - b) "/\" ( - c))) by LATTICES:def 5

 .= (( - a) "\/" (( - b) "/\" ( - c))) by LATTICES:def 8

 .= (( - a) "\/" ( - (b "\/" c))) by A2;

 then ((( - a) "\/" ( - b)) "/\" ( - (a "/\" c))) < (( - a) "\/" ( - (b "\/" c))) by A2, A105;

 then (( - (a "/\" b)) "/\" ( - (a "/\" c))) < (( - a) "\/" ( - (b "\/" c))) by A2;

 then (( - (a "/\" b)) "/\" ( - (a "/\" c))) < ( - (a "/\" (b "\/" c))) by A2;

 then ( - ((a "/\" b) "\/" (a "/\" c))) < ( - (a "/\" (b "\/" c))) by A2;

 then

 A106: (a "/\" (b "\/" c)) <= ((a "/\" b) "\/" (a "/\" c)) by A6, A100, A52;



 A107: (a "/\" b) <= (a "/\" (b "\/" c)) by A28, A83;

 (a "/\" c) <= (a "/\" (b "\/" c)) by A28, A83;

 then ((a "/\" b) "\/" (a "/\" c)) <= (a "/\" (b "\/" c)) by A62, A107;

 hence thesis by A106, A40;

 end;

 reconsider L1 as DeMorgan involutive bounded distributive Lattice-like non empty NelsonStr by A98;



 A108: L1 is satisfying_N5

 proof

 let a,b be Element of L1;



 A109: (a =-> b) = ( Top L1) implies (a "/\" b) = a

 proof

 assume (a =-> b) = ( Top L1);

 then a <= b by A1;

 hence thesis;

 end;

 (a "/\" b) = a implies (a =-> b) = ( Top L1)

 proof

 assume (a "/\" b) = a;

 then a <= b;

 hence thesis by A1;

 end;

 hence thesis by A109;

 end;



 A110: L1 is satisfying_N8

 proof

 let a,b be Element of L1;

 ((( - (a => b)) => (a "/\" ( - b))) "/\" ((a "/\" ( - b)) => ( - (a => b)))) = ( Top L1) by A2;

 hence thesis by A3;

 end;



 A111: L1 is satisfying_N9

 proof

 let a,b be Element of L1;

 ((( - (a => b)) => (a "/\" ( - b))) "/\" ((a "/\" ( - b)) => ( - (a => b)))) = ( Top L1) by A2;

 hence thesis by A3;

 end;



 A112: L1 is satisfying_N10

 proof

 let a be Element of L1;

 ((( - ( ! a)) => a) "/\" (a => ( - ( ! a)))) = ( Top L1) by A2;

 hence thesis by A3;

 end;



 A113: L1 is satisfying_N11

 proof

 let a be Element of L1;

 ((( - ( ! a)) => a) "/\" (a => ( - ( ! a)))) = ( Top L1) by A2;

 hence thesis by A3;

 end;



 A114: L1 is satisfying_N12

 proof

 let a,b be Element of L1;

 ( - a) < (a => b) by A2;

 hence thesis by A52;

 end;



 A115: for a,b,c be Element of L1 holds ( ! ( Top L1)) = ( - ( Top L1))

 proof

 let a,b,c be Element of L1;



 A116: ( - ( Top L1)) <= ( ! ( Top L1)) by A10;

 ( ! ( Top L1)) <= ( - ( Top L1))

 proof

 (( ! (a => a)) => ( - ( Top L1))) = ( Top L1) by A2;

 then

 A117: ( ! ( Top L1)) < ( - ( Top L1)) by A19;



 A118: ( - ( - ( Top L1))) = ( Top L1) by A2;

 ( Top L1) < ( - ( ! ( Top L1))) by A112;

 hence thesis by A117, A118, A6;

 end;

 hence thesis by A116, A40;

 end;



 A119: for a,b be Element of L1 holds (a => ( ! b)) = (b => ( ! a))

 proof

 let a,b be Element of L1;



 A120: (a => ( ! b)) < (b => ( ! a)) by A2;



 A121: ( - (b => ( ! a))) < (b "/\" ( - ( ! a))) by A111;

 (b "/\" ( - ( ! a))) < (b "/\" a) by A113, A57;

 then

 A122: ( - (b => ( ! a))) < (a "/\" b) by A121, A16;



 A123: (a "/\" b) < (a "/\" ( - ( ! b))) by A112, A57;

 (a "/\" ( - ( ! b))) < ( - (a => ( ! b))) by A110;

 then (a "/\" b) < ( - (a => ( ! b))) by A123, A16;

 then ( - (b => ( ! a))) < ( - (a => ( ! b))) by A16, A122;

 then

 A124: (a => ( ! b)) <= (b => ( ! a)) by A120, A6;



 A125: (b => ( ! a)) < (a => ( ! b)) by A2;



 A126: ( - (a => ( ! b))) < (a "/\" ( - ( ! b))) by A111;

 (a "/\" ( - ( ! b))) < (a "/\" b) by A113, A57;

 then

 A127: ( - (a => ( ! b))) < (b "/\" a) by A126, A16;



 A128: (b "/\" a) < (b "/\" ( - ( ! a))) by A112, A57;

 (b "/\" ( - ( ! a))) < ( - (b => ( ! a))) by A110;

 then (b "/\" a) < ( - (b => ( ! a))) by A128, A16;

 then ( - (a => ( ! b))) < ( - (b => ( ! a))) by A16, A127;

 then (b => ( ! a)) <= (a => ( ! b)) by A125, A6;

 hence thesis by A124, A40;

 end;

 L1 is satisfying_N13

 proof

 let a be Element of L1;

 ( ! a) = (( Top L1) => ( ! a)) by A2

 .= (a => ( ! ( Top L1))) by A119

 .= (a => ( - ( Top L1))) by A115;

 hence thesis;

 end;

 hence thesis by A108, A42, A52, A2, A17, A22, A110, A111, A112, A113, A114, A16;

 end;