:: deftheorem defines TrivShefferOrthoLattStr SHEFFER1:def 10 :
TrivShefferOrthoLattStr = ShefferOrthoLattStr(# {0},op2,op2,op1,op2 #);