sheffer2.miz

    begin

    definition

      let L be non empty ShefferStr;

      :: SHEFFER2:def1

      attr L is satisfying_Sh_1 means

      : Def1: for x,y,z be Element of L holds ((x | ((y | x) | x)) | (y | (z | x))) = y;

    end

    registration

      cluster trivial -> satisfying_Sh_1 for non empty ShefferStr;

      coherence by STRUCT_0:def 10;

    end

    registration

      cluster satisfying_Sh_1 satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 for non empty ShefferStr;

      existence

      proof

        take TrivShefferOrthoLattStr ;

        thus thesis;

      end;

    end

    reserve L for satisfying_Sh_1 non empty ShefferStr;

    theorem :: SHEFFER2:1



     Th1: for x,y,z,u be Element of L holds (((x | (y | z)) | (x | (x | (y | z)))) | ((z | ((x | z) | z)) | (u | (x | (y | z))))) = (z | ((x | z) | z))

    proof

      let x,y,z,u be Element of L;

      set Y = (z | ((x | z) | z));

      set X = (x | (y | z));

      ((X | ((Y | X) | X)) | (Y | (u | X))) = Y by Def1;

      hence thesis by Def1;

    end;

    theorem :: SHEFFER2:2



     Th2: for x,y,z be Element of L holds (((x | y) | (((y | ((z | y) | y)) | (x | y)) | (x | y))) | z) = (y | ((z | y) | y))

    proof

      let x,y,z be Element of L;

      set X = (x | y);

      set Y = (y | ((z | y) | y));

      ((X | ((Y | X) | X)) | (Y | (z | X))) = Y by Def1;

      hence thesis by Def1;

    end;

    theorem :: SHEFFER2:3



     Th3: for x,y,z be Element of L holds ((x | ((y | x) | x)) | (y | (z | ((x | z) | z)))) = y

    proof

      let x,y,z be Element of L;

      set X = (x | z);

      set Y = (z | ((x | z) | z));

      ((X | ((Y | X) | X)) | x) = Y by Th2;

      hence thesis by Def1;

    end;

    theorem :: SHEFFER2:4



     Th4: for x,y be Element of L holds (x | ((x | ((x | x) | x)) | (y | (x | ((x | x) | x))))) = (x | ((x | x) | x))

    proof

      let x be Element of L;

      ((x | ((x | x) | x)) | (x | (x | ((x | x) | x)))) = x by Th3;

      hence thesis by Th1;

    end;

    theorem :: SHEFFER2:5



     Th5: for x be Element of L holds (x | ((x | x) | x)) = (x | x)

    proof

      let x be Element of L;

      ((x | ((x | x) | x)) | (x | (x | ((x | x) | x)))) = x by Th3;

      hence thesis by Th4;

    end;

    theorem :: SHEFFER2:6



     Th6: for x be Element of L holds ((x | ((x | x) | x)) | (x | x)) = x

    proof

      let x be Element of L;

      (x | ((x | x) | x)) = (x | x) by Th5;

      hence thesis by Def1;

    end;

    theorem :: SHEFFER2:7



     Th7: for x,y be Element of L holds ((x | x) | (x | (y | x))) = x

    proof

      let x,y be Element of L;

      (x | ((x | x) | x)) = (x | x) by Th5;

      hence thesis by Def1;

    end;

    theorem :: SHEFFER2:8



     Th8: for x,y be Element of L holds ((x | (((y | y) | x) | x)) | y) = (y | y)

    proof

      let x,y be Element of L;

      set Y = (y | y);

      set X = (x | y);

      (Y | (y | (X | y))) = y by Th7;

      hence thesis by Th3;

    end;

    theorem :: SHEFFER2:9



     Th9: for x,y be Element of L holds (((x | y) | (((x | y) | (x | y)) | (x | y))) | ((x | y) | (x | y))) = (y | ((((x | y) | (x | y)) | y) | y))

    proof

      let x,y be Element of L;

      ((y | ((((x | y) | (x | y)) | y) | y)) | (x | y)) = ((x | y) | (x | y)) by Th8;

      hence thesis by Th2;

    end;

    theorem :: SHEFFER2:10



     Th10: for x,y be Element of L holds (x | ((((y | x) | (y | x)) | x) | x)) = (y | x)

    proof

      let x,y be Element of L;

      (((y | x) | (((y | x) | (y | x)) | (y | x))) | ((y | x) | (y | x))) = (y | x) by Th6;

      hence thesis by Th9;

    end;

    theorem :: SHEFFER2:11



     Th11: for x,y be Element of L holds ((x | x) | (y | x)) = x

    proof

      let x,y be Element of L;

      set Y = (y | x);

      (x | (((Y | Y) | x) | x)) = Y by Th10;

      hence thesis by Th7;

    end;

    theorem :: SHEFFER2:12



     Th12: for x,y be Element of L holds (x | (y | (x | x))) = (x | x)

    proof

      let x,y be Element of L;

      set Y = (x | x);

      (Y | (x | x)) = x by Th11;

      hence thesis by Th11;

    end;

    theorem :: SHEFFER2:13



     Th13: for x,y be Element of L holds (((x | y) | (x | y)) | y) = (x | y)

    proof

      let x,y be Element of L;

      ((y | y) | (x | y)) = y by Th11;

      hence thesis by Th11;

    end;

    theorem :: SHEFFER2:14



     Th14: for x,y be Element of L holds (x | ((y | x) | x)) = (y | x)

    proof

      let x,y be Element of L;

      (((y | x) | (y | x)) | x) = (y | x) by Th13;

      hence thesis by Th10;

    end;

    theorem :: SHEFFER2:15



     Th15: for x,y,z be Element of L holds ((x | y) | (x | (z | y))) = x

    proof

      let x,y,z be Element of L;

      (y | ((x | y) | y)) = (x | y) by Th14;

      hence thesis by Def1;

    end;

    theorem :: SHEFFER2:16



     Th16: for x,y,z be Element of L holds ((x | (y | z)) | (x | z)) = x

    proof

      let x,y,z be Element of L;

      ((z | z) | (y | z)) = z by Th11;

      hence thesis by Th15;

    end;

    theorem :: SHEFFER2:17



     Th17: for x,y,z be Element of L holds (x | ((x | y) | (z | y))) = (x | y)

    proof

      let x,y,z be Element of L;

      ((x | y) | (x | (z | y))) = x by Th15;

      hence thesis by Th16;

    end;

    theorem :: SHEFFER2:18



     Th18: for x,y,z be Element of L holds (((x | (y | z)) | z) | x) = (x | (y | z))

    proof

      let x,y,z be Element of L;

      set X = (y | z);

      ((x | X) | (x | z)) = x by Th16;

      hence thesis by Th15;

    end;

    theorem :: SHEFFER2:19



     Th19: for x,y be Element of L holds (x | ((y | x) | x)) = (x | y)

    proof

      let x,y be Element of L;

      ((x | ((y | x) | x)) | (y | ((y | x) | x))) = y by Def1;

      hence thesis by Th17;

    end;

    theorem :: SHEFFER2:20



     Th20: for x,y be Element of L holds (x | y) = (y | x)

    proof

      let x,y be Element of L;

      (x | ((y | x) | x)) = (y | x) by Th14;

      hence thesis by Th19;

    end;

    theorem :: SHEFFER2:21



     Th21: for x,y be Element of L holds ((x | y) | (x | x)) = x

    proof

      let x,y be Element of L;

      set X = (x | y);

      (x | ((y | x) | x)) = X by Th19;

      hence thesis by Th16;

    end;

    theorem :: SHEFFER2:22



     Th22: for x,y,z be Element of L holds ((x | y) | (y | (z | x))) = y

    proof

      let x,y,z be Element of L;

      set Y = (x | ((y | x) | x));

      Y = (x | y) by Th19;

      hence thesis by Def1;

    end;

    theorem :: SHEFFER2:23



     Th23: for x,y,z be Element of L holds ((x | (y | z)) | (z | x)) = x

    proof

      let x,y,z be Element of L;

      (z | x) = (x | z) by Th20;

      hence thesis by Th16;

    end;

    theorem :: SHEFFER2:24



     Th24: for x,y,z be Element of L holds ((x | y) | (y | (x | z))) = y

    proof

      let x,y,z be Element of L;

      (z | x) = (x | z) by Th20;

      hence thesis by Th22;

    end;

    theorem :: SHEFFER2:25



     Th25: for x,y,z be Element of L holds ((x | (y | z)) | (y | x)) = x

    proof

      let x,y,z be Element of L;

      (z | y) = (y | z) by Th20;

      hence thesis by Th23;

    end;

    theorem :: SHEFFER2:26



     Th26: for x,y,z be Element of L holds (((x | y) | (x | z)) | z) = (x | z)

    proof

      let x,y,z be Element of L;

      ((x | z) | (z | (x | y))) = z by Th24;

      hence thesis by Th22;

    end;

    theorem :: SHEFFER2:27



     Th27: for x,y,z be Element of L holds (x | (y | (x | (y | z)))) = (x | (y | z))

    proof

      let x,y,z be Element of L;

      set Y = (y | x);

      ((x | (y | z)) | Y) = x by Th25;

      hence thesis by Th25;

    end;

    theorem :: SHEFFER2:28



     Th28: for x,y,z be Element of L holds ((x | (y | (x | z))) | y) = (y | (x | z))

    proof

      let x,y,z be Element of L;

      set Y = (y | (x | z));

      (Y | (x | y)) = y by Th25;

      hence thesis by Th24;

    end;

    theorem :: SHEFFER2:29



     Th29: for x,y,z,u be Element of L holds ((x | (y | z)) | (x | (u | (y | x)))) = ((x | (y | z)) | (y | x))

    proof

      let x,y,z,u be Element of L;

      set X = (x | (y | z));

      set Y = (y | x);

      (X | Y) = x by Th25;

      hence thesis by Th17;

    end;

    theorem :: SHEFFER2:30



     Th30: for x,y,z be Element of L holds ((x | (y | (x | z))) | y) = (y | (z | x))

    proof

      let x,y,z be Element of L;

      (z | x) = (x | z) by Th20;

      hence thesis by Th28;

    end;

    theorem :: SHEFFER2:31



     Th31: for x,y,z,u be Element of L holds ((x | (y | z)) | (x | (u | (y | x)))) = x

    proof

      let x,y,z be Element of L;

      ((x | (y | z)) | (y | x)) = x by Th25;

      hence thesis by Th29;

    end;

    theorem :: SHEFFER2:32



     Th32: for x,y be Element of L holds (x | (y | (x | y))) = (x | x)

    proof

      let x,y be Element of L;

      ((x | y) | (x | ((x | y) | y))) = x by Th15;

      hence thesis by Th30;

    end;

    theorem :: SHEFFER2:33



     Th33: for x,y,z be Element of L holds (x | (y | z)) = (x | (z | y))

    proof

      let x,y,z be Element of L;

      ((z | (x | (z | y))) | x) = (x | (z | y)) by Th28;

      hence thesis by Th30;

    end;

    theorem :: SHEFFER2:34



     Th34: for x,y,z be Element of L holds (x | (y | (x | (z | (y | x))))) = (x | x)

    proof

      let x,y,z be Element of L;

      ((x | (y | (x | (z | (y | x))))) | (x | (z | (y | x)))) = x by Th31;

      hence thesis by Th18;

    end;

    theorem :: SHEFFER2:35



     Th35: for x,y,z be Element of L holds ((x | (y | z)) | ((y | x) | x)) = ((x | (y | z)) | (x | (y | z)))

    proof

      let x,y,z be Element of L;

      set X = (x | (y | z));

      (X | (y | x)) = x by Th25;

      hence thesis by Th32;

    end;

    theorem :: SHEFFER2:36



     Th36: for x,y be Element of L holds ((x | (y | x)) | y) = (y | y)

    proof

      let x,y be Element of L;

      set X = x;

      set Y = y;

      (Y | (X | (Y | X))) = ((X | (Y | X)) | Y) by Th20;

      hence thesis by Th32;

    end;

    theorem :: SHEFFER2:37



     Th37: for x,y,z be Element of L holds ((x | y) | z) = (z | (y | x))

    proof

      let x,y,z be Element of L;

      set X = (x | y);

      (X | z) = (z | X) by Th20;

      hence thesis by Th33;

    end;

    theorem :: SHEFFER2:38



     Th38: for x,y,z be Element of L holds (x | (y | (z | (x | y)))) = (x | (y | y))

    proof

      let x,y,z be Element of L;

      set Y = z;

      (y | (x | (y | (Y | (x | y))))) = (y | y) by Th34;

      hence thesis by Th27;

    end;

    theorem :: SHEFFER2:39



     Th39: for x,y,z be Element of L holds (((x | y) | y) | (y | (z | x))) = ((y | (z | x)) | (y | (z | x)))

    proof

      let x,y,z be Element of L;

      set X = (y | (z | x));

      (X | (x | y)) = y by Th23;

      hence thesis by Th36;

    end;

    theorem :: SHEFFER2:40



     Th40: for x,y,z,u be Element of L holds ((x | y) | (z | u)) = ((u | z) | (y | x))

    proof

      let x,y,z,u be Element of L;

      ((x | y) | (z | u)) = ((x | y) | (u | z)) by Th33;

      hence thesis by Th37;

    end;

    theorem :: SHEFFER2:41



     Th41: for x,y,z be Element of L holds (x | (y | ((y | x) | z))) = (x | (y | y))

    proof

      let x,y,z be Element of L;

      (x | (y | (z | (x | y)))) = (x | (y | ((y | x) | z))) by Th37;

      hence thesis by Th38;

    end;

    theorem :: SHEFFER2:42



     Th42: for x,y be Element of L holds (x | (y | x)) = (x | (y | y))

    proof

      let x,y be Element of L;

      set Y = (x | (y | y));

      (Y | (x | y)) = x by Th16;

      hence thesis by Th38;

    end;

    theorem :: SHEFFER2:43



     Th43: for x,y be Element of L holds ((x | y) | y) = (y | (x | x))

    proof

      let x,y be Element of L;

      set X = x;

      set Y = y;

      (Y | (X | Y)) = ((X | Y) | Y) by Th20;

      hence thesis by Th42;

    end;

    theorem :: SHEFFER2:44



     Th44: for x,y be Element of L holds (x | (y | y)) = (x | (x | y))

    proof

      let x,y be Element of L;

      (x | (y | x)) = (x | (y | y)) by Th42;

      hence thesis by Th33;

    end;

    theorem :: SHEFFER2:45



     Th45: for x,y,z be Element of L holds ((x | (y | y)) | (x | (z | y))) = ((x | (z | y)) | (x | (z | y)))

    proof

      let x,y,z be Element of L;

      set Y = y;

      set X = x;

      ((Y | X) | X) = (X | (Y | Y)) by Th43;

      hence thesis by Th39;

    end;

    theorem :: SHEFFER2:46



     Th46: for x,y,z be Element of L holds ((x | (y | z)) | (x | (y | y))) = ((x | (y | z)) | (x | (y | z)))

    proof

      let x,y,z be Element of L;

      ((x | (y | z)) | ((y | x) | x)) = ((x | (y | z)) | (x | (y | y))) by Th43;

      hence thesis by Th35;

    end;

    theorem :: SHEFFER2:47



     Th47: for x,y,z be Element of L holds (x | ((y | y) | (z | (x | (x | y))))) = (x | ((y | y) | (y | y)))

    proof

      let x,y,z be Element of L;

      (x | (y | y)) = (x | (x | y)) by Th44;

      hence thesis by Th38;

    end;

    theorem :: SHEFFER2:48



     Th48: for x,y,z be Element of L holds (((x | (y | z)) | (x | (y | z))) | (y | y)) = (x | (y | y))

    proof

      let x,y,z be Element of L;

      set Z = (y | y);

      set Y = (y | z);

      ((x | Y) | (x | Y)) = ((x | Y) | (x | Z)) by Th46;

      hence thesis by Th26;

    end;

    theorem :: SHEFFER2:49



     Th49: for x,y,z be Element of L holds (x | ((y | y) | (z | (x | (x | y))))) = (x | y)

    proof

      let x,y,z be Element of L;

      ((y | y) | (y | y)) = y by Th21;

      hence thesis by Th47;

    end;

    theorem :: SHEFFER2:50



     Th50: for x,y,z be Element of L holds ((((x | y) | (x | y)) | ((z | ((x | y) | z)) | (x | y))) | (x | x)) = ((z | ((x | y) | z)) | (x | x))

    proof

      let x,y,z be Element of L;

      set Y = z;

      set X = (x | y);

      ((Y | (X | Y)) | X) = (X | X) by Th36;

      hence thesis by Th48;

    end;

    theorem :: SHEFFER2:51



     Th51: for x,y,z be Element of L holds ((x | ((y | z) | x)) | (y | y)) = ((y | z) | (y | y))

    proof

      let x,y,z be Element of L;

      set Y = (y | z);

      set X = (x | ((y | z) | x));

      ((Y | Y) | (X | Y)) = Y by Th11;

      hence thesis by Th50;

    end;

    theorem :: SHEFFER2:52



     Th52: for x,y,z be Element of L holds ((x | ((y | z) | x)) | (y | y)) = y

    proof

      let x,y,z be Element of L;

      ((y | z) | (y | y)) = y by Th21;

      hence thesis by Th51;

    end;

    theorem :: SHEFFER2:53



     Th53: for x,y,z be Element of L holds (x | ((y | ((x | z) | y)) | x)) = (y | ((x | z) | y))

    proof

      let x,y,z be Element of L;

      ((y | ((x | z) | y)) | (x | x)) = x by Th52;

      hence thesis by Th16;

    end;

    theorem :: SHEFFER2:54



     Th54: for x,y,z be Element of L holds (x | ((y | (y | (z | x))) | x)) = (y | ((x | (y | (x | z))) | y))

    proof

      let x,y,z be Element of L;

      set Z = (y | (x | z));

      ((x | Z) | y) = (y | (z | x)) by Th30;

      hence thesis by Th53;

    end;

    theorem :: SHEFFER2:55



     Th55: for x,y,z be Element of L holds (x | ((y | (y | (z | x))) | x)) = (y | (y | (z | x)))

    proof

      let x,y,z be Element of L;

      (y | (z | x)) = ((x | (y | (x | z))) | y) by Th30;

      hence thesis by Th54;

    end;

    theorem :: SHEFFER2:56



     Th56: for x,y,z,u be Element of L holds (x | (y | (z | (z | (u | (y | x)))))) = (x | (y | y))

    proof

      let x,y,z,u be Element of L;

      ((y | x) | ((z | (z | (u | (y | x)))) | (y | x))) = (z | (z | (u | (y | x)))) by Th55;

      hence thesis by Th41;

    end;

    theorem :: SHEFFER2:57



     Th57: for x,y,z be Element of L holds (x | (y | (y | (z | (x | y))))) = (x | (y | (x | x)))

    proof

      let x,y,z be Element of L;

      (y | (x | (y | (y | (z | (x | y)))))) = (y | (x | x)) by Th56;

      hence thesis by Th27;

    end;

    theorem :: SHEFFER2:58



     Th58: for x,y,z be Element of L holds (x | (y | (y | (z | (x | y))))) = (x | x)

    proof

      let x,y,z be Element of L;

      (x | (y | (x | x))) = (x | x) by Th12;

      hence thesis by Th57;

    end;

    theorem :: SHEFFER2:59



     Th59: for x,y be Element of L holds (x | (y | (y | y))) = (x | x)

    proof

      let x,y be Element of L;

      set Y = (y | (x | y));

      (Y | (x | y)) = y by Th25;

      hence thesis by Th58;

    end;

    theorem :: SHEFFER2:60



     Th60: for x,y,z be Element of L holds (x | (((y | (z | x)) | (y | (z | x))) | (z | z))) = (x | (y | (z | x)))

    proof

      let x,y,z be Element of L;

      set Y = (y | (z | x));

      (z | (x | (x | Y))) = (z | z) by Th58;

      hence thesis by Th49;

    end;

    theorem :: SHEFFER2:61



     Th61: for x,y,z be Element of L holds (x | (y | (z | z))) = (x | (y | (z | x)))

    proof

      let x,y,z be Element of L;

      (((y | (z | x)) | (y | (z | x))) | (z | z)) = (y | (z | z)) by Th48;

      hence thesis by Th60;

    end;

    theorem :: SHEFFER2:62



     Th62: for x,y,z be Element of L holds (x | (y | ((z | z) | x))) = (x | (y | z))

    proof

      let x,y,z be Element of L;

      set X = (z | z);

      (X | (z | z)) = z by Th21;

      hence thesis by Th61;

    end;

    theorem :: SHEFFER2:63



     Th63: for x,y,z be Element of L holds ((x | (y | y)) | (x | (z | ((y | y) | x)))) = ((x | (z | y)) | (x | (z | y)))

    proof

      let x,y,z be Element of L;

      (x | (z | ((y | y) | x))) = (x | (z | y)) by Th62;

      hence thesis by Th45;

    end;

    theorem :: SHEFFER2:64



     Th64: for x,y,z be Element of L holds ((x | (y | y)) | (x | (z | (x | (y | y))))) = ((x | (z | y)) | (x | (z | y)))

    proof

      let x,y,z be Element of L;

      (x | (y | y)) = ((y | y) | x) by Th37;

      hence thesis by Th63;

    end;

    theorem :: SHEFFER2:65



     Th65: for x,y,z be Element of L holds ((x | (y | y)) | (x | (z | z))) = ((x | (z | y)) | (x | (z | y)))

    proof

      let x,y,z be Element of L;

      set X = (x | (y | y));

      ((x | (y | y)) | (x | (z | z))) = ((x | (y | y)) | (x | (z | X))) by Th61;

      hence thesis by Th64;

    end;

    theorem :: SHEFFER2:66



     Th66: for x,y,z be Element of L holds (((x | x) | y) | ((z | z) | y)) = ((y | (x | z)) | (y | (x | z)))

    proof

      let x,y,z be Element of L;

      ((y | (z | z)) | (y | (x | x))) = (((x | x) | y) | ((z | z) | y)) by Th40;

      hence thesis by Th65;

    end;

    theorem :: SHEFFER2:67



     Th67: for L be non empty ShefferStr st L is satisfying_Sh_1 holds L is satisfying_Sheffer_1

    proof

      let L be non empty ShefferStr;

      assume L is satisfying_Sh_1;

      then for x be Element of L holds ((x | x) | (x | x)) = x by Th21;

      hence thesis by SHEFFER1:def 13;

    end;

    theorem :: SHEFFER2:68



     Th68: for L be non empty ShefferStr st L is satisfying_Sh_1 holds L is satisfying_Sheffer_2

    proof

      let L be non empty ShefferStr;

      assume L is satisfying_Sh_1;

      then for x,y be Element of L holds (x | (y | (y | y))) = (x | x) by Th59;

      hence thesis by SHEFFER1:def 14;

    end;

    theorem :: SHEFFER2:69



     Th69: for L be non empty ShefferStr st L is satisfying_Sh_1 holds L is satisfying_Sheffer_3

    proof

      let L be non empty ShefferStr;

      assume L is satisfying_Sh_1;

      then for x,y,z be Element of L holds ((x | (y | z)) | (x | (y | z))) = (((y | y) | x) | ((z | z) | x)) by Th66;

      hence thesis by SHEFFER1:def 15;

    end;

    registration

      cluster properly_defined Boolean well-complemented Lattice-like de_Morgan satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 satisfying_Sh_1 for non empty ShefferOrthoLattStr;

      existence

      proof

        take TrivShefferOrthoLattStr ;

        for x,y be Element of TrivShefferOrthoLattStr holds (x "/\" y) = (((x ` ) "\/" (y ` )) ` ) by STRUCT_0:def 10;

        hence thesis by ROBBINS1:def 23;

      end;

    end

    registration

      cluster satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 properly_defined -> Boolean Lattice-like for non empty ShefferOrthoLattStr;

      coherence by SHEFFER1: 37;

      cluster Boolean Lattice-like well-complemented properly_defined -> satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 for non empty ShefferOrthoLattStr;

      coherence by SHEFFER1: 26, SHEFFER1: 27, SHEFFER1: 28;

    end

    begin

    reserve L for satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 non empty ShefferStr;

    reserve v,q,p,w,z,y,x for Element of L;

    theorem :: SHEFFER2:70



     Th70: for x, w holds (w | ((x | x) | x)) = (w | w)

    proof

      let x, w;

      ((x | x) | (x | x)) = x by SHEFFER1:def 13;

      hence thesis by SHEFFER1:def 14;

    end;

    theorem :: SHEFFER2:71



     Th71: for p, x holds x = ((x | x) | (p | (p | p)))

    proof

      let p, x;

      ((x | x) | (x | x)) = x by SHEFFER1:def 13;

      hence thesis by SHEFFER1:def 14;

    end;

    theorem :: SHEFFER2:72



     Th72: for y, w holds ((w | w) | (w | (y | (y | y)))) = w

    proof

      let y, w;

      (w | w) = (w | (y | (y | y))) by SHEFFER1:def 14;

      hence thesis by SHEFFER1:def 13;

    end;

    theorem :: SHEFFER2:73



     Th73: for q, p, y, w holds (((w | (y | (y | y))) | p) | ((q | q) | p)) = ((p | (w | q)) | (p | (w | q)))

    proof

      let q, p, y, w;

      (w | w) = (w | (y | (y | y))) by SHEFFER1:def 14;

      hence thesis by SHEFFER1:def 15;

    end;

    theorem :: SHEFFER2:74



     Th74: for q, p, x holds ((x | p) | ((q | q) | p)) = ((p | ((x | x) | q)) | (p | ((x | x) | q)))

    proof

      let q, p, x;

      ((x | x) | (x | x)) = x by SHEFFER1:def 13;

      hence thesis by SHEFFER1:def 15;

    end;

    theorem :: SHEFFER2:75



     Th75: for w, p, y, q holds (((w | w) | p) | ((q | (y | (y | y))) | p)) = ((p | (w | q)) | (p | (w | q)))

    proof

      let w, p, y, q;

      (q | q) = (q | (y | (y | y))) by SHEFFER1:def 14;

      hence thesis by SHEFFER1:def 15;

    end;

    theorem :: SHEFFER2:76



     Th76: for p, x holds x = ((x | x) | ((p | p) | p))

    proof

      let p, x;

      ((x | x) | (x | x)) = x by SHEFFER1:def 13;

      hence thesis by Th70;

    end;

    theorem :: SHEFFER2:77



     Th77: for y, w holds ((w | w) | (w | ((y | y) | y))) = w

    proof

      let y, w;

      (w | w) = (w | ((y | y) | y)) by Th70;

      hence thesis by SHEFFER1:def 13;

    end;

    theorem :: SHEFFER2:78



     Th78: for y, w holds ((w | ((y | y) | y)) | (w | w)) = w

    proof

      let y, w;

      (w | w) = (w | ((y | y) | y)) by Th70;

      hence thesis by SHEFFER1:def 13;

    end;

    theorem :: SHEFFER2:79



     Th79: for p, y, w holds ((w | ((y | y) | y)) | (p | (p | p))) = w

    proof

      let p, y, w;

      (w | w) = (w | ((y | y) | y)) by Th70;

      hence thesis by Th71;

    end;

    theorem :: SHEFFER2:80



     Th80: for p, x, y holds (((y | (x | x)) | (y | (x | x))) | (p | (p | p))) = ((x | x) | y)

    proof

      let p, x, y;

      (((x | x) | y) | ((x | x) | y)) = ((y | (x | x)) | (y | (x | x))) by SHEFFER1:def 15;

      hence thesis by Th71;

    end;

    theorem :: SHEFFER2:81



     Th81: for x, y holds (y | (x | x)) = ((x | x) | y)

    proof

      now

        let p, x, y;

        (((y | (x | x)) | (y | (x | x))) | (p | (p | p))) = (y | (x | x)) by Th71;

        hence (y | (x | x)) = ((x | x) | y) by Th80;

      end;

      hence thesis;

    end;

    theorem :: SHEFFER2:82



     Th82: for y, w holds (w | y) = (((y | y) | (y | y)) | w)

    proof

      let y, w;

      ((y | y) | (y | y)) = y by SHEFFER1:def 13;

      hence thesis by Th81;

    end;

    theorem :: SHEFFER2:83



     Th83: for y, w holds (w | y) = (y | w)

    proof

      let y, w;

      ((y | y) | (y | y)) = y by SHEFFER1:def 13;

      hence thesis by Th82;

    end;

    theorem :: SHEFFER2:84



     Th84: for x, p holds ((p | x) | (p | ((x | x) | (x | x)))) = ((((x | x) | (x | x)) | p) | (((x | x) | (x | x)) | p))

    proof

      let x, p;

      ((x | x) | (x | x)) = x by SHEFFER1:def 13;

      hence thesis by SHEFFER1:def 15;

    end;

    theorem :: SHEFFER2:85



     Th85: for x, p holds ((p | x) | (p | x)) = ((((x | x) | (x | x)) | p) | (((x | x) | (x | x)) | p))

    proof

      let x, p;

      ((x | x) | (x | x)) = x by SHEFFER1:def 13;

      hence thesis by Th84;

    end;

    theorem :: SHEFFER2:86



     Th86: for x, p holds ((p | x) | (p | x)) = ((x | p) | (((x | x) | (x | x)) | p))

    proof

      let x, p;

      ((x | x) | (x | x)) = x by SHEFFER1:def 13;

      hence thesis by Th85;

    end;

    theorem :: SHEFFER2:87



     Th87: for x, p holds ((p | x) | (p | x)) = ((x | p) | (x | p))

    proof

      let x, p;

      ((x | x) | (x | x)) = x by SHEFFER1:def 13;

      hence thesis by Th86;

    end;

    theorem :: SHEFFER2:88



     Th88: for y, q, w holds (((w | q) | ((y | y) | y)) | ((w | q) | (w | q))) = (((w | w) | (w | q)) | ((q | q) | (w | q)))

    proof

      let y, q, w;

      ((w | q) | (w | q)) = ((w | q) | ((y | y) | y)) by Th70;

      hence thesis by SHEFFER1:def 15;

    end;

    theorem :: SHEFFER2:89



     Th89: for q, w holds (w | q) = (((w | w) | (w | q)) | ((q | q) | (w | q)))

    proof

      now

        let y, q, w;

        (((w | q) | ((y | y) | y)) | ((w | q) | (w | q))) = (w | q) by Th78;

        hence (w | q) = (((w | w) | (w | q)) | ((q | q) | (w | q))) by Th88;

      end;

      hence thesis;

    end;

    theorem :: SHEFFER2:90



     Th90: for q, p holds ((p | p) | (p | ((q | q) | q))) = ((((q | q) | (q | q)) | p) | ((q | q) | p))

    proof

      let q, p;

      (p | ((q | q) | q)) = (p | p) by Th70;

      hence thesis by SHEFFER1:def 15;

    end;

    theorem :: SHEFFER2:91



     Th91: for p, q holds p = ((((q | q) | (q | q)) | p) | ((q | q) | p))

    proof

      let p, q;

      ((p | p) | (p | ((q | q) | q))) = p by Th77;

      hence thesis by Th90;

    end;

    theorem :: SHEFFER2:92



     Th92: for p, q holds p = ((q | p) | ((q | q) | p))

    proof

      let p, q;

      ((q | q) | (q | q)) = q by SHEFFER1:def 13;

      hence thesis by Th91;

    end;

    theorem :: SHEFFER2:93



     Th93: for z, w, x holds ((((x | x) | w) | ((z | z) | w)) | ((w | (x | z)) | (w | (x | z)))) = (((w | w) | (w | (x | z))) | (((x | z) | (x | z)) | (w | (x | z))))

    proof

      let z, w, x;

      ((w | (x | z)) | (w | (x | z))) = (((x | x) | w) | ((z | z) | w)) by SHEFFER1:def 15;

      hence thesis by SHEFFER1:def 15;

    end;

    theorem :: SHEFFER2:94



     Th94: for z, w, x holds ((((x | x) | w) | ((z | z) | w)) | ((w | (x | z)) | (w | (x | z)))) = (w | (x | z))

    proof

      let z, w, x;

      (((w | w) | (w | (x | z))) | (((x | z) | (x | z)) | (w | (x | z)))) = (w | (x | z)) by Th89;

      hence thesis by Th93;

    end;

    theorem :: SHEFFER2:95



     Th95: for w, p holds ((p | p) | (p | (w | (w | w)))) = (((w | w) | p) | (((w | w) | (w | w)) | p))

    proof

      let w, p;

      (p | (w | (w | w))) = (p | p) by SHEFFER1:def 14;

      hence thesis by SHEFFER1:def 15;

    end;

    theorem :: SHEFFER2:96



     Th96: for p, w holds p = (((w | w) | p) | (((w | w) | (w | w)) | p))

    proof

      let p, w;

      ((p | p) | (p | (w | (w | w)))) = p by Th72;

      hence thesis by Th95;

    end;

    theorem :: SHEFFER2:97



     Th97: for p, w holds p = (((w | w) | p) | (w | p))

    proof

      let p, w;

      ((w | w) | (w | w)) = w by SHEFFER1:def 13;

      hence thesis by Th96;

    end;

    theorem :: SHEFFER2:98



     Th98: for z, q, x holds ((((x | x) | q) | ((z | z) | q)) | ((q | (x | z)) | (q | (x | z)))) = ((((z | z) | (z | z)) | ((x | x) | q)) | ((q | q) | ((x | x) | q)))

    proof

      let z, q, x;

      (((x | x) | q) | ((z | z) | q)) = ((q | (x | z)) | (q | (x | z))) by SHEFFER1:def 15;

      hence thesis by SHEFFER1:def 15;

    end;

    theorem :: SHEFFER2:99



     Th99: for q, z, x holds (q | (x | z)) = ((((z | z) | (z | z)) | ((x | x) | q)) | ((q | q) | ((x | x) | q)))

    proof

      let q, z, x;

      ((((x | x) | q) | ((z | z) | q)) | ((q | (x | z)) | (q | (x | z)))) = (q | (x | z)) by Th94;

      hence thesis by Th98;

    end;

    theorem :: SHEFFER2:100



     Th100: for q, z, x holds (q | (x | z)) = ((z | ((x | x) | q)) | ((q | q) | ((x | x) | q)))

    proof

      let q, z, x;

      ((z | z) | (z | z)) = z by SHEFFER1:def 13;

      hence thesis by Th99;

    end;

    theorem :: SHEFFER2:101



     Th101: for w, y holds (w | w) = (((y | y) | y) | w)

    proof

      let w, y;

      (w | ((y | y) | y)) = (w | w) by Th70;

      hence thesis by Th83;

    end;

    theorem :: SHEFFER2:102



     Th102: for w, p holds ((p | w) | ((w | w) | p)) = p

    proof

      let w, p;

      (w | p) = (p | w) by Th83;

      hence thesis by Th92;

    end;

    theorem :: SHEFFER2:103



     Th103: for y, w holds ((w | w) | ((w | w) | ((y | y) | y))) = ((y | y) | y)

    proof

      let y, w;

      (w | ((y | y) | y)) = (w | w) by Th70;

      hence thesis by Th92;

    end;

    theorem :: SHEFFER2:104



     Th104: for y, w holds ((w | w) | w) = ((y | y) | y)

    proof

      let y, w;

      ((w | w) | ((y | y) | y)) = w by Th76;

      hence thesis by Th103;

    end;

    theorem :: SHEFFER2:105



     Th105: for p, w holds ((w | p) | (p | (w | w))) = p

    proof

      let p, w;

      ((w | w) | p) = (p | (w | w)) by Th83;

      hence thesis by Th92;

    end;

    theorem :: SHEFFER2:106



     Th106: for w, p holds ((p | (w | w)) | (w | p)) = p

    proof

      let w, p;

      ((w | w) | p) = (p | (w | w)) by Th83;

      hence thesis by Th97;

    end;

    theorem :: SHEFFER2:107



     Th107: for p, w holds ((w | p) | (w | (p | p))) = w

    proof

      let p, w;

      ((p | p) | w) = (w | (p | p)) by Th83;

      hence thesis by Th102;

    end;

    theorem :: SHEFFER2:108



     Th108: for x, y holds (y | (((y | (x | x)) | (y | (x | x))) | (x | y))) = (x | y)

    proof

      let x, y;

      ((x | y) | (y | (x | x))) = y by Th105;

      hence thesis by Th102;

    end;

    theorem :: SHEFFER2:109



     Th109: for p, w holds ((w | (p | p)) | (w | p)) = w

    proof

      let p, w;

      (p | w) = (w | p) by Th83;

      hence thesis by Th106;

    end;

    theorem :: SHEFFER2:110



     Th110: for p, w, q, y holds ((((y | y) | y) | q) | ((w | w) | q)) = ((q | (((p | (p | p)) | (p | (p | p))) | w)) | (q | (((p | (p | p)) | (p | (p | p))) | w)))

    proof

      let p, w, q, y;

      (((p | (p | p)) | (p | (p | p))) | (p | (p | p))) = ((y | y) | y) by Th104;

      hence thesis by Th73;

    end;

    theorem :: SHEFFER2:111



     Th111: for q, w, p holds ((q | q) | ((w | w) | q)) = ((q | (((p | (p | p)) | (p | (p | p))) | w)) | (q | (((p | (p | p)) | (p | (p | p))) | w)))

    proof

      let q, w, p;

      ((((p | (p | p)) | (p | (p | p))) | (p | (p | p))) | q) = (q | q) by Th101;

      hence thesis by Th73;

    end;

    theorem :: SHEFFER2:112



     Th112: for w, y, p holds ((w | p) | (w | (p | (y | (y | y))))) = w

    proof

      let w, y, p;

      (p | p) = (p | (y | (y | y))) by SHEFFER1:def 14;

      hence thesis by Th107;

    end;

    theorem :: SHEFFER2:113



     Th113: for w, y, p holds ((w | (p | (y | (y | y)))) | (w | p)) = w

    proof

      let w, y, p;

      (p | p) = (p | (y | (y | y))) by SHEFFER1:def 14;

      hence thesis by Th109;

    end;

    theorem :: SHEFFER2:114



     Th114: for q, p, y holds ((((y | y) | y) | p) | ((q | q) | p)) = ((p | ((p | p) | q)) | (p | ((p | p) | q)))

    proof

      let q, p, y;

      (p | p) = (((y | y) | y) | p) by Th101;

      hence thesis by Th74;

    end;

    theorem :: SHEFFER2:115



     Th115: for q, z, x holds (((q | ((x | x) | z)) | (q | ((x | x) | z))) | ((x | q) | ((z | z) | q))) = ((((z | z) | (z | z)) | (x | q)) | ((q | q) | (x | q)))

    proof

      let q, z, x;

      ((x | q) | ((z | z) | q)) = ((q | ((x | x) | z)) | (q | ((x | x) | z))) by Th74;

      hence thesis by SHEFFER1:def 15;

    end;

    theorem :: SHEFFER2:116



     Th116: for q, z, x holds (((q | ((x | x) | z)) | (q | ((x | x) | z))) | ((x | q) | ((z | z) | q))) = ((z | (x | q)) | ((q | q) | (x | q)))

    proof

      let q, z, x;

      ((z | z) | (z | z)) = z by SHEFFER1:def 13;

      hence thesis by Th115;

    end;

    theorem :: SHEFFER2:117



     Th117: for w, q, z holds (((w | w) | ((z | z) | q)) | ((q | ((q | q) | z)) | (q | ((q | q) | z)))) = ((((z | z) | q) | (w | q)) | (((z | z) | q) | (w | q)))

    proof

      let w, q, z;

      ((q | q) | ((z | z) | q)) = ((q | ((q | q) | z)) | (q | ((q | q) | z))) by Th74;

      hence thesis by SHEFFER1:def 15;

    end;

    theorem :: SHEFFER2:118



     Th118: for q, p, x holds (((p | (x | p)) | (p | (x | p))) | (q | (q | q))) = ((x | x) | p)

    proof

      let q, p, x;

      (((x | x) | p) | ((p | p) | p)) = ((p | (x | p)) | (p | (x | p))) by SHEFFER1:def 15;

      hence thesis by Th79;

    end;

    theorem :: SHEFFER2:119



     Th119: for p, x holds (p | (x | p)) = ((x | x) | p)

    proof

      now

        let q, p, x;

        (((p | (x | p)) | (p | (x | p))) | (q | (q | q))) = (p | (x | p)) by Th71;

        hence (p | (x | p)) = ((x | x) | p) by Th118;

      end;

      hence thesis;

    end;

    theorem :: SHEFFER2:120



     Th120: for p, y holds ((y | p) | ((y | y) | p)) = ((p | p) | (y | p))

    proof

      let p, y;

      (p | (y | p)) = ((y | y) | p) by Th119;

      hence thesis by Th119;

    end;

    theorem :: SHEFFER2:121



     Th121: for x, y holds x = ((x | x) | (y | x))

    proof

      let x, y;

      ((y | x) | ((y | y) | x)) = x by Th92;

      hence thesis by Th120;

    end;

    theorem :: SHEFFER2:122



     Th122: for x, y holds ((y | x) | x) = (((x | (y | y)) | (x | (y | y))) | (y | x))

    proof

      let x, y;

      ((x | (y | y)) | (y | x)) = x by Th106;

      hence thesis by Th119;

    end;

    theorem :: SHEFFER2:123



     Th123: for x, z, y holds (((x | ((y | y) | z)) | (x | ((y | y) | z))) | ((y | x) | ((z | z) | x))) = ((z | (y | x)) | x)

    proof

      let x, z, y;

      ((x | x) | (y | x)) = x by Th121;

      hence thesis by Th116;

    end;

    theorem :: SHEFFER2:124



     Th124: for x, y, z holds ((x | (((z | (z | z)) | (z | (z | z))) | y)) | (x | (((z | (z | z)) | (z | (z | z))) | y))) = x

    proof

      let x, y, z;

      ((x | x) | ((y | y) | x)) = x by Th121;

      hence thesis by Th111;

    end;

    theorem :: SHEFFER2:125



     Th125: for x, z, y holds ((x | ((y | y) | z)) | z) = (z | (y | x))

    proof

      let x, z, y;

      ((z | z) | ((y | y) | z)) = z by Th121;

      hence thesis by Th100;

    end;

    theorem :: SHEFFER2:126



     Th126: for x, y holds (x | ((y | x) | x)) = (y | x)

    proof

      let x, y;

      (((x | (y | y)) | (x | (y | y))) | (y | x)) = ((y | x) | x) by Th122;

      hence thesis by Th108;

    end;

    theorem :: SHEFFER2:127



     Th127: for z, y, x holds y = ((((x | x) | x) | y) | ((z | z) | y))

    proof

      now

        let x, y, z, p;

        ((y | (((p | (p | p)) | (p | (p | p))) | z)) | (y | (((p | (p | p)) | (p | (p | p))) | z))) = y by Th124;

        hence y = ((((x | x) | x) | y) | ((z | z) | y)) by Th110;

      end;

      hence thesis;

    end;

    theorem :: SHEFFER2:128



     Th128: for z, y holds ((y | ((y | y) | z)) | (y | ((y | y) | z))) = y

    proof

      now

        let z, y, x;

        ((((x | x) | x) | y) | ((z | z) | y)) = y by Th127;

        hence ((y | ((y | y) | z)) | (y | ((y | y) | z))) = y by Th114;

      end;

      hence thesis;

    end;

    theorem :: SHEFFER2:129



     Th129: for x, z, y holds ((((y | y) | z) | (x | z)) | (((y | y) | z) | (x | z))) = (((x | x) | ((y | y) | z)) | z)

    proof

      let x, z, y;

      ((z | ((z | z) | y)) | (z | ((z | z) | y))) = z by Th128;

      hence thesis by Th117;

    end;

    theorem :: SHEFFER2:130



     Th130: for x, z, y holds ((((y | y) | z) | (x | z)) | (((y | y) | z) | (x | z))) = (z | (y | (x | x)))

    proof

      let x, z, y;

      (((x | x) | ((y | y) | z)) | z) = (z | (y | (x | x))) by Th125;

      hence thesis by Th129;

    end;

    theorem :: SHEFFER2:131



     Th131: for y, x holds (((x | y) | (x | y)) | x) = (x | y)

    proof

      let y, x;

      ((x | (y | y)) | (x | y)) = x by Th109;

      hence thesis by Th121;

    end;

    theorem :: SHEFFER2:132



     Th132: for p, w holds ((w | w) | (w | p)) = w

    proof

      let p, w;

      (p | w) = (w | p) by Th83;

      hence thesis by Th121;

    end;

    theorem :: SHEFFER2:133



     Th133: for w, p holds ((p | w) | (w | w)) = w

    proof

      let w, p;

      ((w | w) | (p | w)) = ((p | w) | (w | w)) by Th83;

      hence thesis by Th121;

    end;

    theorem :: SHEFFER2:134



     Th134: for p, y, w holds ((w | (y | (y | y))) | (w | p)) = w

    proof

      let p, y, w;

      (w | w) = (w | (y | (y | y))) by SHEFFER1:def 14;

      hence thesis by Th132;

    end;

    theorem :: SHEFFER2:135



     Th135: for p, w holds ((w | p) | (w | w)) = w

    proof

      let p, w;

      ((w | w) | (w | p)) = ((w | p) | (w | w)) by Th83;

      hence thesis by Th132;

    end;

    theorem :: SHEFFER2:136



     Th136: for y, p, w holds ((w | p) | (w | (y | (y | y)))) = w

    proof

      let y, p, w;

      (w | w) = (w | (y | (y | y))) by SHEFFER1:def 14;

      hence thesis by Th135;

    end;

    theorem :: SHEFFER2:137



     Th137: for p, q, w, y, x holds ((((x | (y | (y | y))) | w) | ((q | q) | w)) | ((w | (x | q)) | (w | (x | q)))) = (((w | (p | (p | p))) | (w | (x | q))) | (((x | q) | (x | q)) | (w | (x | q))))

    proof

      let p, q, w, y, x;

      ((w | (x | q)) | (w | (x | q))) = (((x | (y | (y | y))) | w) | ((q | q) | w)) by Th73;

      hence thesis by Th73;

    end;

    theorem :: SHEFFER2:138



     Th138: for q, w, y, x holds ((((x | (y | (y | y))) | w) | ((q | q) | w)) | ((w | (x | q)) | (w | (x | q)))) = (w | (((x | q) | (x | q)) | (w | (x | q))))

    proof

      now

        let y, p, w, q, x;

        ((w | (p | (p | p))) | (w | (x | q))) = w by Th134;

        hence ((((x | (y | (y | y))) | w) | ((q | q) | w)) | ((w | (x | q)) | (w | (x | q)))) = (w | (((x | q) | (x | q)) | (w | (x | q)))) by Th137;

      end;

      hence thesis;

    end;

    theorem :: SHEFFER2:139



     Th139: for q, w, y, x holds ((((x | (y | (y | y))) | w) | ((q | q) | w)) | ((w | (x | q)) | (w | (x | q)))) = (w | (x | q))

    proof

      let q, w, y, x;

      (((x | q) | (x | q)) | (w | (x | q))) = (x | q) by Th121;

      hence thesis by Th138;

    end;

    theorem :: SHEFFER2:140



     Th140: for z, p, q, y, x holds ((((x | (y | (y | y))) | q) | ((z | z) | q)) | ((q | (x | z)) | (q | (x | z)))) = ((((z | z) | (p | (p | p))) | ((x | (y | (y | y))) | q)) | ((q | q) | ((x | (y | (y | y))) | q)))

    proof

      let z, p, q, y, x;

      (((x | (y | (y | y))) | q) | ((z | z) | q)) = ((q | (x | z)) | (q | (x | z))) by Th73;

      hence thesis by Th73;

    end;

    theorem :: SHEFFER2:141



     Th141: for z, p, q, y, x holds (q | (x | z)) = ((((z | z) | (p | (p | p))) | ((x | (y | (y | y))) | q)) | ((q | q) | ((x | (y | (y | y))) | q)))

    proof

      let z, p, q, y, x;

      ((((x | (y | (y | y))) | q) | ((z | z) | q)) | ((q | (x | z)) | (q | (x | z)))) = (q | (x | z)) by Th139;

      hence thesis by Th140;

    end;

    theorem :: SHEFFER2:142



     Th142: for z, q, y, x holds (q | (x | z)) = ((z | ((x | (y | (y | y))) | q)) | ((q | q) | ((x | (y | (y | y))) | q)))

    proof

      now

        let p, z, q, y, x;

        ((z | z) | (p | (p | p))) = z by Th71;

        hence (q | (x | z)) = ((z | ((x | (y | (y | y))) | q)) | ((q | q) | ((x | (y | (y | y))) | q))) by Th141;

      end;

      hence thesis;

    end;

    theorem :: SHEFFER2:143



     Th143: for v, p, y, x holds (p | (x | v)) = ((v | ((x | (y | (y | y))) | p)) | p)

    proof

      let v, p, y, x;

      ((p | p) | ((x | (y | (y | y))) | p)) = p by Th121;

      hence thesis by Th142;

    end;

    theorem :: SHEFFER2:144



     Th144: for y, w, z, v, x holds ((w | (z | (x | v))) | (((x | (y | (y | y))) | z) | ((v | v) | z))) = (z | (x | v))

    proof

      let y, w, z, v, x;

      ((z | (x | v)) | (z | (x | v))) = (((x | (y | (y | y))) | z) | ((v | v) | z)) by Th73;

      hence thesis by Th133;

    end;

    theorem :: SHEFFER2:145



     Th145: for y, z, x holds (((y | ((x | x) | z)) | (y | ((x | x) | z))) | ((x | y) | ((z | z) | y))) = (y | ((x | x) | z))

    proof

      let y, z, x;

      ((y | ((x | x) | z)) | (y | ((x | x) | z))) = ((x | y) | ((z | z) | y)) by Th74;

      hence thesis by Th121;

    end;

    theorem :: SHEFFER2:146



     Th146: for z, y, x holds ((z | (x | y)) | y) = (y | ((x | x) | z))

    proof

      let z, y, x;

      (((y | ((x | x) | z)) | (y | ((x | x) | z))) | ((x | y) | ((z | z) | y))) = ((z | (x | y)) | y) by Th123;

      hence thesis by Th145;

    end;

    theorem :: SHEFFER2:147



     Th147: for x, w, y, z holds ((((x | x) | w) | ((z | (y | (y | y))) | w)) | w) = (w | (x | z))

    proof

      let x, w, y, z;

      ((w | (x | z)) | (w | (x | z))) = (((x | x) | w) | ((z | (y | (y | y))) | w)) by Th75;

      hence thesis by Th131;

    end;

    theorem :: SHEFFER2:148



     Th148: for z, w, x holds (w | (z | ((x | x) | w))) = (w | (x | z))

    proof

      now

        let x, w, p, z;

        ((((x | x) | w) | ((z | (p | (p | p))) | w)) | w) = (w | (z | ((x | x) | w))) by Th143;

        hence (w | (z | ((x | x) | w))) = (w | (x | z)) by Th147;

      end;

      hence thesis;

    end;

    theorem :: SHEFFER2:149



     Th149: for p, z, y, x holds (((z | (x | p)) | (z | (x | p))) | (((x | (y | (y | y))) | z) | ((p | p) | z))) = ((((p | p) | z) | ((x | (y | (y | y))) | z)) | (((p | p) | z) | ((x | (y | (y | y))) | z)))

    proof

      let p, z, y, x;

      (((x | (y | (y | y))) | z) | ((p | p) | z)) = ((z | (x | p)) | (z | (x | p))) by Th73;

      hence thesis by Th87;

    end;

    theorem :: SHEFFER2:150



     Th150: for p, z, y, x holds (z | (x | p)) = ((((p | p) | z) | ((x | (y | (y | y))) | z)) | (((p | p) | z) | ((x | (y | (y | y))) | z)))

    proof

      let p, z, y, x;

      (((z | (x | p)) | (z | (x | p))) | (((x | (y | (y | y))) | z) | ((p | p) | z))) = (z | (x | p)) by Th144;

      hence thesis by Th149;

    end;

    theorem :: SHEFFER2:151



     Th151: for z, p, y, x holds (z | (x | p)) = (z | (p | ((x | (y | (y | y))) | (x | (y | (y | y))))))

    proof

      let z, p, y, x;

      ((((p | p) | z) | ((x | (y | (y | y))) | z)) | (((p | p) | z) | ((x | (y | (y | y))) | z))) = (z | (p | ((x | (y | (y | y))) | (x | (y | (y | y)))))) by Th130;

      hence thesis by Th150;

    end;

    theorem :: SHEFFER2:152



     Th152: for z, p, x holds (z | (x | p)) = (z | (p | x))

    proof

      now

        let y, z, p, x;

        ((x | (y | (y | y))) | (x | (y | (y | y)))) = x by Th136;

        hence (z | (x | p)) = (z | (p | x)) by Th151;

      end;

      hence thesis;

    end;

    theorem :: SHEFFER2:153



     Th153: for w, q, p holds ((p | q) | w) = (w | (q | p))

    proof

      let w, q, p;

      (w | (p | q)) = ((p | q) | w) by Th83;

      hence thesis by Th152;

    end;

    theorem :: SHEFFER2:154



     Th154: for w, p, q holds (((q | p) | w) | q) = (q | ((p | p) | w))

    proof

      let w, p, q;

      (w | (p | q)) = ((q | p) | w) by Th153;

      hence thesis by Th146;

    end;

    theorem :: SHEFFER2:155



     Th155: for z, w, y, x holds (w | x) = (w | ((x | z) | (((x | (y | (y | y))) | (x | (y | (y | y)))) | w)))

    proof

      let z, w, y, x;

      ((x | (y | (y | y))) | (x | z)) = x by Th134;

      hence thesis by Th148;

    end;

    theorem :: SHEFFER2:156



     Th156: for w, z, x holds (w | x) = (w | ((x | z) | (x | w)))

    proof

      now

        let y, w, z, x;

        ((x | (y | (y | y))) | (x | (y | (y | y)))) = x by Th136;

        hence (w | x) = (w | ((x | z) | (x | w))) by Th155;

      end;

      hence thesis;

    end;

    theorem :: SHEFFER2:157



     Th157: for q, x, z, y holds ((x | y) | (((x | (y | (z | (z | z)))) | q) | x)) = ((x | y) | (x | (y | (z | (z | z)))))

    proof

      let q, x, z, y;

      ((x | (y | (z | (z | z)))) | (x | y)) = x by Th113;

      hence thesis by Th156;

    end;

    theorem :: SHEFFER2:158



     Th158: for x, q, z, y holds ((x | y) | (x | (((y | (z | (z | z))) | (y | (z | (z | z)))) | q))) = ((x | y) | (x | (y | (z | (z | z)))))

    proof

      let x, q, z, y;

      (((x | (y | (z | (z | z)))) | q) | x) = (x | (((y | (z | (z | z))) | (y | (z | (z | z)))) | q)) by Th154;

      hence thesis by Th157;

    end;

    theorem :: SHEFFER2:159



     Th159: for z, x, q, y holds ((x | y) | (x | (y | q))) = ((x | y) | (x | (y | (z | (z | z)))))

    proof

      let z, x, q, y;

      ((y | (z | (z | z))) | (y | (z | (z | z)))) = y by Th136;

      hence thesis by Th158;

    end;

    theorem :: SHEFFER2:160



     Th160: for x, q, y holds ((x | y) | (x | (y | q))) = x

    proof

      now

        let q, x, z, y;

        ((x | y) | (x | (y | (z | (z | z))))) = x by Th112;

        hence ((x | y) | (x | (y | q))) = x by Th159;

      end;

      hence thesis;

    end;

    theorem :: SHEFFER2:161



     Th161: L is satisfying_Sh_1

    proof

      given a,b,c be Element of L such that

       A1: ((a | ((b | a) | a)) | (b | (c | a))) <> b;



       A2: (a | ((b | a) | a)) = (b | a) by Th126;

       not ((a | ((b | a) | a)) | (b | (a | c))) = b by A1, Th83;

      hence thesis by A2, Th160;

    end;

    registration

      cluster satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 -> satisfying_Sh_1 for non empty ShefferStr;

      coherence by Th161;

      cluster satisfying_Sh_1 -> satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 for non empty ShefferStr;

      coherence by Th67, Th68, Th69;

    end

    registration

      cluster satisfying_Sh_1 properly_defined -> Boolean Lattice-like for non empty ShefferOrthoLattStr;

      coherence ;

      cluster Boolean Lattice-like well-complemented properly_defined -> satisfying_Sh_1 for non empty ShefferOrthoLattStr;

      coherence ;

    end