:: Two Axiomatizations of {N}elson Algebras
::  by Adam Grabowski
:: 
:: Received April 19, 2015
:: Copyright (c) 2015-2019 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies LATTICES, BINOP_1, XBOOLE_0, EQREL_1, XBOOLEAN, XXREAL_0,
      REALSET1, SUBSET_1, STRUCT_0, XXREAL_2, FUNCT_1, ARYTM_3, ARYTM_1,
      ROBBINS1, NELSON_1, PBOOLE, ZFMISC_1, OPOSET_1;
 notations TARSKI, XBOOLE_0, LATTICES, SUBSET_1, BINOP_1, FUNCT_2, STRUCT_0,
      ROBBINS1, ROBBINS3;
 constructors BINOP_1, ROBBINS3;
 registrations STRUCT_0, LATTICES, LATTICE2, ROBBINS1, ROBBINS3, XBOOLE_0,
      ZFMISC_1, LATTAD_1;
 requirements SUBSET, BOOLE;
 definitions LATTICES, ROBBINS3;
 expansions ROBBINS1, ROBBINS3, LATTICES;
 theorems STRUCT_0, LATTICES, ROBBINS3, TARSKI;

begin :: De Morgan Algebras

definition let L be non empty OrthoLattStr;
  attr L is DeMorgan means :Def1:
    for x, y being 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 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 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
  (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
  x "/\" (x "/\" y) = x "/\" y
  proof
    thus x "/\" (x "/\" y) = (x "/\" x) "/\" y by LATTICES:def 7
                     .= x "/\" y;
  end;

theorem
  x "\/" (x "\/" y) = x "\/" y
  proof
    thus x "\/" (x "\/" y) = (x "\/" x) "\/" y by LATTICES:def 5
                     .= x "\/" y;
  end;

begin :: The Structure and Operators in Nelson Algebras

definition
  struct (OrthoLattStr) NelsonStr
                 (# carrier -> set,
                      unity -> Element of the carrier,
            Compl, Nnegation -> UnOp of the carrier,
       Iimpl, impl, L_join, L_meet -> BinOp of the carrier #);
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 being 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;
  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;
  pred a < b means
    a => b = Top L;
end;

:: Lattice-like ordering

definition let L be non empty NelsonStr,
               a, b be Element of L;
  pred a <= b means
    a = a "/\" b;
end;

:: Strong negation operator

definition let L be non empty NelsonStr,
               a be Element of L;
  func ! a -> Element of L equals
    (the Nnegation of L).a;
  coherence;
end;

:: Strong implication

definition let L be non empty NelsonStr,
               a, b be Element of L;
  func a =-> b -> Element of L equals
    (the impl of L).(a,b);
  coherence;
end;

begin :: The Non-Equational Axiomatization of Nelson Algebras

::NdR _A1, _A2 : quasi_ordering on A
definition let L be non empty NelsonStr;
  attr L is satisfying_A1 means :Def2:
    for a being Element of L holds
      a < a;

  attr L is satisfying_A1b means :Def3:
    for a, b, c being Element of L holds
      a < b & b < c implies a < c;
end;

definition let L be bounded Lattice-like non empty NelsonStr;
  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;

:: Axioms of N-algebras (according to Rasiowa)
:: These lattices are called Nelson algebras now, but Rasiowa used the name
:: either N-lattices or quasi-pseudo-boolean algebras.

definition let L be non empty NelsonStr;
  attr L is satisfying_N3 means :Def4:
    for x, a, b being Element of L holds
      a "/\" x < b iff x < (a => b);

  attr L is satisfying_N4 means :Def5:
    for a, b being Element of L holds
      a =-> b = (a => b) "/\" ((-b) => -a);

  attr L is satisfying_N5 means :Def6:
    for a, b being Element of L holds
      a =-> b = Top L iff a "/\" b = a;

  attr L is satisfying_N6 means :Def7:
    for a, b, c being Element of L holds
      a < c & b < c implies a "\/" b < c;

  attr L is satisfying_N7 means :Def8:
    for a, b, c being Element of L holds
      a < b & a < c implies a < b "/\" c;

  attr L is satisfying_N8 means :Def9:
    for a, b being Element of L holds
      (a "/\" -b) < -(a => b);

  attr L is satisfying_N9 means :Def10:
    for a, b being Element of L holds
      -(a => b) < (a "/\" -b);

  attr L is satisfying_N10 means :Def11:
    for a being Element of L holds
      a < -!a;

  attr L is satisfying_N11 means :Def12:
    for a being Element of L holds
      -!a < a;

  attr L is satisfying_N12 means :Def13:
    for a, b being Element of L holds
      a "/\" -a < b;

  attr L is satisfying_N13 means :Def14:
    for a being 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;
  redefine 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
  a [= b iff a <= b by LATTICES:4;

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

::NdR RasiowaNonClassical: p 69 1.1 (2) <=> (4)
theorem Th5: :: (2.1) (2.3 <=> 2.5)
  a <= b iff a < b & -b < -a
  proof
    thus a <= b implies a < b & -b < -a
    proof
      assume a <= b; then
      a =-> b = Top L by Def6;
      hence a < b & -b < -a by Th4;
    end;
    assume a < b & -b < -a; then
    a =-> b = Top L;
    hence thesis by Def6;
  end;

theorem Th6:
  a "/\" b < a
  proof
    a "/\" b <= a by LATTICES:4,6;
    hence thesis by Th5;
  end;

theorem Th7:
  a < a "\/" b
  proof
    a <= a "\/" b by LATTICES:4,5;
    hence thesis by Th5;
  end;

::NdR RasiowaNonClassical: p 69 1.1 (2) <=> (3)
theorem  :: (2.1) (2.3 <=> 2.4)
  a <= b iff a =-> b = Top L by Def6;

::NdR RasiowaNonClassical: p 70 (38)
theorem 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
  (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 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,7;
  end;

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

theorem 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 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 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 by Def4;
      b < b "\/" (-a) by Th7; then
A3:   a "/\" (a => 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 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 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 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
  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) < 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 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 :: Properties of Nelson Algebras
:: Proven properties from Rasiowa's "Algebraic Models of Logic"
:: Items 2.3, 2.4, p. 92
:: The same set of properties, but with different numbers is also
:: in Rasiowa's "An Algebraic Appproach to Non-Classical Logic"

::NdR RasiowaNonClassical: p 69 1.2 (5)
theorem  :: (2.7)
  a =-> a = Top L
  proof
    a "/\" a = a;
    hence thesis by Def6;
  end;

::NdR RasiowaNonClassical: p 69 1.2 (6)
theorem  :: (2.8)
  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;

::NdR RasiowaNonClassical: p 69 1.2 (7)
theorem  :: (2.9)
  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;

::NdR RasiowaNonClassical: p 69 1.2 (8)
theorem  :: (2.10)
  a =-> Top L = Top L
  proof
    a "/\" Top L = a;
    hence thesis by Def6;
  end;

::NdR RasiowaNonClassical: p 69 1.3 (9)
theorem Th16ter: :: (2.11)
  a => a = Top L
  proof
    a < a by Def2;
    hence thesis;
  end;

::NdR RasiowaNonClassical: p 69 1.3 (10)
theorem  :: (2.12)
  (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;

::NdR RasiowaNonClassical: p 69 1.3 (11)
theorem :: (2.13)
  b < c implies a "\/" b < a "\/" c & a "/\" b < a "/\" c by Lm1;

::NdR p 69 1.3 (12)
theorem :: (2.14)
  a < b & c < d implies a "\/" c < b "\/" d & a "/\" c < b "/\" d
    by Lm2;

::NdR RasiowaNonClassical: p 69 1.3 (13)
theorem Th17: :: (2.15)
  a "/\" (a => b) < b
  proof
    (a => b) < (a => b) by Def2;
    hence thesis by Def4;
  end;

::NdR RasiowaNonClassical: p 69 1.3 (14)
theorem  :: (2.16)
  a => (b => c) = (a "/\" b) => c by Lm3;

::NdR RasiowaNonClassical: p 69 1.3 (15)
theorem Th18: :: (2.17)
  a => (b => c) = b => (a => c)
  proof
    a => (b => c) = (a "/\" b) => c by Lm3
      .= b => (a => c) by Lm3;
    hence thesis;
  end;

::NdR RasiowaNonClassical: p 69 1.3 (16)
theorem Th19: :: (2.18)
  a < ((a => b) => b)
  proof
    a "/\" (a => b) < b by Th17;
    hence thesis by Def4;
  end;

::NdR RasiowaNonClassical: p 71 PROOF (50)
theorem Th19bis: :: (2.19)
  a < b => (a "/\" b)
  proof
    b "/\" a <= a "/\" b; then
    b "/\" a < a "/\" b by Th5;
    hence thesis by Def4;
  end;

::NdR RasiowaNonClassical: p 69 (18)
theorem :: RasiowaNonClassical: p 69 (17)
  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: ::RasiowaNonClassical: p 71 (51)
  (-a) "\/" (-b) "/\" a < -b
  proof
    ((-b) "/\" a) <= (-b) by LATTICES:4,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: ::RasiowaNonClassical: p 71 (52)
  a < (-( a "/\" b)) => -b
  proof
    (-a) "\/" (-b) "/\" a < -b by Lm4;
    then a < ((-a) "\/" (-b)) => -b by Def4;
    hence thesis by Th8;
  end;

Lm6: ::RasiowaNonClassical: p 72 (55)
  -(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 :: RasiowaNonClassical: p 69 (18)
  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;

::NdR RasiowaNonClassical: p 70 1.3 (19)
theorem Th20: :: (2.20)
  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;

::NdR RasiowaNonClassical: p 70 1.3 (20)
theorem Th21: :: (2.21)
  (a => Top L) = Top L
  proof
    a <= Top L by LATTICES:4,19; then
    a < Top L by Th5;
    hence thesis;
  end;

::NdR RasiowaNonClassical: p 70 1.3 (21)
theorem Th22: :: (2.22)
  ((Bottom L) => a) = Top L
  proof
    Bottom L <= a; then
    Bottom L < a by Th5;
    hence thesis;
  end;

::NdR RasiowaNonClassical: p 70 1.3 (22)
theorem Th23: :: (2.23)
  ((Top L) => b) = b
  proof
    (b "/\" (Top L)) < b by Def2; then
A1: 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 Th17;
    (Top L) "/\" -b < -((Top L) => b) by Def9; then
    ((Top L) => b) <= b by Th5,A3;
    hence thesis by A2,Th3;
  end;

::NdR RasiowaNonClassical: p 70 1.3 (23)
theorem  :: (2.24)
  a = Top L & a => b = Top L implies b = Top L by Th23;

::NdR RasiowaNonClassical: p 70 1.3 (24)
theorem Th24: :: (2.25)
  a => (b => a) = Top L
  proof
    b "/\" a <= a by LATTICES:4,6; then
    b "/\" a < a by Th5; then
    a < b => a by Def4;
    hence thesis;
  end;

::NdR RasiowaNonClassical: p 70 1.3 (25)
theorem Th25: :: (2.26)
  ((a => (b => c)) => ((a => b) => (a => c))) = Top L
  proof
    a "/\" (a => b) < b by Th17; then
    a "/\" (a => 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;

::NdR RasiowaNonClassical: p 70 1.3 (26)
theorem Th26: :: (2.27)
  (a => (a "\/" b)) = Top L
  proof
    a < a "\/" b by Th7;
    hence thesis;
  end;

::NdR RasiowaNonClassical: p 70 1.3 (27)
theorem Th27: :: (2.28)
  b => (a "\/" b) = Top L
  proof
    b < a "\/" b by Th7;
    hence thesis;
  end;

::NdR RasiowaNonClassical: p 70 1.3 (28)
theorem Th28: :: (2.29)
  (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;

::NdR RasiowaNonClassical: p 70 1.3 (29)
theorem Th29: :: (2.30)
  (a "/\" b) => a = Top L
  proof
    a "/\" b < a by Th6;
    hence thesis;
  end;

::NdR RasiowaNonClassical: p 70 1.3 (30)
theorem Th30: :: (2.31)
  (a "/\" b) => b = Top L
  proof
    a "/\" b < b by Th6;
    hence thesis;
  end;

::NdR RasiowaNonClassical: p 70 1.3 (31)
theorem Th31: :: (2.32)
  (a => b) => ((a => c) => (a => (b "/\" c))) = Top L
  proof
A1: a "/\" (a => c) < c by Th17;
A2: a "/\" (a => b) < b by Th17;
    (a "/\" (a => 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;

::NdR RasiowaNonClassical: p 70 1.3 (32)
theorem Th32: :: (2.33)
  (a => !b) => (b => !a) = Top L
  proof
    a => !b = b => !a by Th20;
    hence thesis by Th16ter;
  end;

::NdR RasiowaNonClassical: p 70 1.3 (33)
theorem Th33: :: (2.34)
  (!(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;

::NdR RasiowaNonClassical: p 70 1.3 (34)
theorem Th34: :: (2.35)
  (-a) => (a => b) = Top L
  proof
    a "/\" -a < b by Def13; then
    (-a) < (a => b) by Def4;
    hence thesis;
  end;

::NdR RasiowaNonClassical: p 70 1.3 (35)
theorem Th35: :: (2.36)
  ((-(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;

::NdR RasiowaNonClassical: p 70 1.3 (36)
theorem Th36: :: (2.37)
  ((-!a) => a) "/\" (a => (-!a)) = Top L
  proof
A1: -!a < a by Def12;
    a < -!a by Def11;
    hence thesis by A1;
  end;

::NdR RasiowaNonClassical: p 70 1.3 (37)
theorem  :: (2.38)
  --a = a by ROBBINS3:def 6;

::NdR RasiowaNonClassical: p 70 1.3 (39)
theorem Th37: :: (2.39)
  -(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;

::NdR RasiowaNonClassical: p 70 1.3 (38)
theorem  :: (2.40)
  -(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;

::NdR RasiowaNonClassical: p 70 1.3 (40)
theorem Th38: :: (2.41)
  a < b implies b => 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;

::NdR RasiowaNonClassical: p 70 1.3 (41)
theorem  :: (2.42)
  (a => b) => ((c => d) => ((a "/\" c) => (b "/\" d))) = Top L
  proof
A1: (a "/\" (a => b)) < b by Th17;
    (c "/\" (c => 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;

::NdR RasiowaNonClassical: p 70 1.3 (42)
theorem  :: (2.43)
  (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) < b by Def4;
    ((c => 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;

::NdR RasiowaNonClassical: p 70 1.3 (43)
theorem  :: (2.44)
  (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 :: Alternative Equational Axiomatics by Rasiowa

definition let L be non empty NelsonStr;
  attr L is satisfying_N0* means
    for a, b being Element of L holds
      a <= b iff a =-> b = Top L;

::NdR RasiowaNonClassical: p 75 qpB1*
  attr L is satisfying_N1* means
    for a, b being Element of L holds
      a => (b => a) = Top L;
::NdR RasiowaNonClassical: p 75 qpB2*
  attr L is satisfying_N2* means
    for a, b, c being Element of L holds
      (a => (b => c)) => ((a => b) => (a => c)) = Top L;
::NdR RasiowaNonClassical: p 76 qpB3*
  attr L is satisfying_N3* means
    for a being Element of L holds
      ((Top L) => a) = a;
::NdR RasiowaNonClassical: p 76 qpB5*
  attr L is satisfying_N5* means
    for a, b being Element of L holds
      ((a =-> b) => ((b =-> a) => b)) = ((b =-> a) => ((a =-> b) => a));
::NdR RasiowaNonClassical: p 76 qpB6*
  attr L is satisfying_N6* means
    for a, b being Element of L holds
      a => (a "\/" b) = Top L;
::NdR RasiowaNonClassical: p 76 qpB7*
  attr L is satisfying_N7* means
    for a, b being Element of L holds
      b => (a "\/" b) = Top L;
::NdR RasiowaNonClassical: p 77 qpB8*
  attr L is satisfying_N8* means
    for a, b, c being Element of L holds
      (a => c) => ((b => c) => ((a "\/" b) => c)) = Top L;
::NdR RasiowaNonClassical: p 77 qpB9*
  attr L is satisfying_N9* means
    for a, b being Element of L holds
      (a "/\" b) => a = Top L;
::NdR RasiowaNonClassical: p 77 qpB10*
  attr L is satisfying_N10* means
    for a, b being Element of L holds
      (a "/\" b) => b = Top L;
::NdR RasiowaNonClassical: p 77 qpB11*
  attr L is satisfying_N11* means
    for a, b, c being Element of L holds
      (a => b) => ((a => c) => (a => (b "/\" c))) = Top L;
::NdR RasiowaNonClassical: p 77 qpB12*
  attr L is satisfying_N12* means
    for a, b being Element of L holds
      (a => !b) => (b => !a) = Top L;
::NdR RasiowaNonClassical: p 77 qpB13*
  attr L is satisfying_N13* means
    for a, b being Element of L holds
      (!(a => a)) => b = Top L;
::NdR RasiowaNonClassical: p 77 qpB14*
  attr L is satisfying_N14* means
    for a, b being Element of L holds
      (-a) => (a => b) = Top L;
::NdR RasiowaNonClassical: p 77 qpB15*
  attr L is satisfying_N15* means
    for a, b being Element of L holds
      ((-(a => b)) => (a "/\" -b)) "/\" ((a "/\" -b) => -(a => b)) = Top L;
::NdR RasiowaNonClassical: p 77 qpB17*
  attr L is satisfying_N17* means
    for a, b being Element of L holds
      -(a "\/" b) = ((-a) "/\" (-b));
::NdR RasiowaNonClassical: p 77 qpB19*
  attr L is satisfying_N19* means
    for a being Element of L holds
      ((-!a) => a) "/\" (a => (-!a)) = Top L;
end;

notation
  let L be non empty NelsonStr;
::NdR RasiowaNonClassical: p 77 qpB4*
  synonym L is satisfying_N4* for L is satisfying_N4;
::NdR RasiowaNonClassical: p 77 qpB16*
  synonym L is satisfying_N16* for L is DeMorgan;
::NdR RasiowaNonClassical: p 77 qpB18*
  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
  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 being 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 < b by A2;
      hence thesis by A2;
    end;
    set w = Top L1;
A4: w => 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 being Element of L1 holds a <= b iff a < b & -b < -a
    proof
      let a, b be Element of L1;
A7:   a =-> b = (a => b) "/\" ((-b) => (-a)) by A2;
      thus a <= b implies a < b & -b < -a
      proof
        assume a <= b; then
        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 being 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 being 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 being Element of L holds d "/\" a = d
    proof
      let a be Element of L;
      d <= a by A10;
      hence thesis;
    end;
A13: for a being 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 being 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 < b & b < c;
      hence thesis by A14;
    end;
A17: L1 is satisfying_N6
    proof
      let a, b, c be Element of L1;
      assume
A18:  a < c & b < c;
      (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 being 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) => ((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 being Element of L1 holds b < a "\/" b by A2;
A25: for a, b being 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 being 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 being 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 being 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 < b by A2;
     -b < (-a) "\/" (-b) by A2;
     hence thesis by A35,A36,A6;
   end;

A37: for a being Element of L1 holds a =-> 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 being 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 being 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 being 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 being Element of L1 holds
      a < b implies b => 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 being 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 being 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 being 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 implies x < a => 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
     proof
       assume
A55:   x < a => 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 being 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 being 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 being 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 being 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 < b & -b < -c by A67,A6;
     ((-a) => (-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 being 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 being 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 being 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 being 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, def 6;

A77: for a, b, c being 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 being Element of L1 holds d "/\" a = d & a "/\" d = d by A12;
    for a, b being 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 being 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 being 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 being 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 being 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 being 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 being 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,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 being 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 being 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 being 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;