:: deftheorem Def500 defines + BINARI_6:def 10 :
for A, B, b₃ being Element of Class EqBL2Nat holds
( b₃ = A + B iff ex x, y being Element of BOOLEAN * st
( x in A & y in B & b₃ = Class (EqBL2Nat,(x + y)) ) );