begin
theorem Th1:
begin
:: deftheorem Def1 defines upper-bounded' SHEFFER1:def 1 :
:: deftheorem Def2 defines Top' SHEFFER1:def 2 :
:: deftheorem Def3 defines lower-bounded' SHEFFER1:def 3 :
:: deftheorem Def4 defines Bot' SHEFFER1:def 4 :
:: deftheorem Def5 defines distributive' SHEFFER1:def 5 :
:: deftheorem Def6 defines is_a_complement'_of SHEFFER1:def 6 :
:: deftheorem Def7 defines complemented' SHEFFER1:def 7 :
:: deftheorem Def8 defines `# SHEFFER1:def 8 :
theorem
canceled;
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
:: deftheorem Def9 defines meet-idempotent SHEFFER1:def 9 :
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem
theorem Th24:
theorem Th25:
theorem Th26:
begin
:: deftheorem defines TrivShefferOrthoLattStr SHEFFER1:def 10 :
:: deftheorem defines | SHEFFER1:def 11 :
:: deftheorem Def12 defines properly_defined SHEFFER1:def 12 :
:: deftheorem Def13 defines satisfying_Sheffer_1 SHEFFER1:def 13 :
:: deftheorem Def14 defines satisfying_Sheffer_2 SHEFFER1:def 14 :
:: deftheorem Def15 defines satisfying_Sheffer_3 SHEFFER1:def 15 :
theorem
theorem
theorem
:: deftheorem defines " SHEFFER1:def 16 :
theorem
theorem
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem