:: deftheorem Def9 defines Equality NOMIN_4:def 9 :
for A being set
for b₂ being Function of [:A,A:],BOOLEAN holds
( b₂ = Equality A iff for a, b being object st a in A & b in A holds
( ( a = b implies b₂ . (a,b) = TRUE ) & ( a <> b implies b₂ . (a,b) = FALSE ) ) );