:: 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 `) ) ) );