:: deftheorem QLTEx1Def defines QLT_Ex1 LATQUASI:def 6 :
for b₁ being BinOp of {0,1,2} holds
( b₁ = QLT_Ex1 iff for x, y being Element of {0,1,2} holds
( ( x = y implies b₁ . (x,y) = x ) & ( x <> y implies b₁ . (x,y) = 0 ) ) );