begin
theorem Th1:
begin
:: deftheorem Def1 defines upper-bounded' SHEFFER1:def 1 :
for IT being non empty LattStr holds
( IT is upper-bounded' iff ex c being Element of IT st
for a being Element of IT holds
( c "/\" a = a & a "/\" c = a ) );
:: deftheorem Def2 defines Top' SHEFFER1:def 2 :
for L being non empty LattStr st L is upper-bounded' holds
for b2 being Element of L holds
( b2 = Top' L iff for a being Element of L holds
( b2 "/\" a = a & a "/\" b2 = a ) );
:: deftheorem Def3 defines lower-bounded' SHEFFER1:def 3 :
for IT being non empty LattStr holds
( IT is lower-bounded' iff ex c being Element of IT st
for a being Element of IT holds
( c "\/" a = a & a "\/" c = a ) );
:: deftheorem Def4 defines Bot' SHEFFER1:def 4 :
for L being non empty LattStr st L is lower-bounded' holds
for b2 being Element of L holds
( b2 = Bot' L iff for a being Element of L holds
( b2 "\/" a = a & a "\/" b2 = a ) );
:: deftheorem Def5 defines distributive' SHEFFER1:def 5 :
for IT being non empty LattStr holds
( IT is distributive' iff for a, b, c being Element of IT holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c) );
:: deftheorem Def6 defines is_a_complement'_of SHEFFER1:def 6 :
for L being non empty LattStr
for a, b being Element of L holds
( a is_a_complement'_of b iff ( b "\/" a = Top' L & a "\/" b = Top' L & b "/\" a = Bot' L & a "/\" b = Bot' L ) );
:: deftheorem Def7 defines complemented' SHEFFER1:def 7 :
for IT being non empty LattStr holds
( IT is complemented' iff for b being Element of IT ex a being Element of IT st a is_a_complement'_of b );
:: deftheorem Def8 defines `# SHEFFER1:def 8 :
for L being non empty LattStr
for x being Element of L st L is complemented' & L is distributive & L is upper-bounded' & L is meet-commutative holds
for b3 being Element of L holds
( b3 = x `# iff b3 is_a_complement'_of x );
theorem
canceled;
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
:: deftheorem Def9 defines meet-idempotent SHEFFER1:def 9 :
for G being non empty /\-SemiLattStr holds
( G is meet-idempotent iff for x being Element of G holds x "/\" x = x );
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 :
TrivShefferOrthoLattStr = ShefferOrthoLattStr(# 1,op2 ,op2 ,op1 ,op2 #);
:: deftheorem defines | SHEFFER1:def 11 :
for L being non empty ShefferStr
for x, y being Element of L holds x | y = the stroke of L . x,y;
:: deftheorem Def12 defines properly_defined SHEFFER1:def 12 :
for L being non empty ShefferOrthoLattStr holds
( L is properly_defined iff ( ( for x being Element of L holds x | x = x ` ) & ( for x, y being Element of L holds x "\/" y = (x | x) | (y | y) ) & ( for x, y being Element of L holds x "/\" y = (x | y) | (x | y) ) & ( for x, y being Element of L holds x | y = (x ` ) + (y ` ) ) ) );
:: deftheorem Def13 defines satisfying_Sheffer_1 SHEFFER1:def 13 :
for L being non empty ShefferStr holds
( L is satisfying_Sheffer_1 iff for x being Element of L holds (x | x) | (x | x) = x );
:: deftheorem Def14 defines satisfying_Sheffer_2 SHEFFER1:def 14 :
for L being non empty ShefferStr holds
( L is satisfying_Sheffer_2 iff for x, y being Element of L holds x | (y | (y | y)) = x | x );
:: deftheorem Def15 defines satisfying_Sheffer_3 SHEFFER1:def 15 :
for L being non empty ShefferStr holds
( L is satisfying_Sheffer_3 iff for x, y, z being Element of L holds (x | (y | z)) | (x | (y | z)) = ((y | y) | x) | ((z | z) | x) );
theorem
theorem
theorem
:: deftheorem defines " SHEFFER1:def 16 :
for L being non empty ShefferStr
for a being Element of L holds a " = a | a;
theorem
theorem
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem