:: deftheorem Def5 defines pair_diff HEYTING1:def 5 :
for A being set
for b₂ being BinOp of [:(Fin A),(Fin A):] holds
( b₂ = pair_diff A iff for a, b being Element of [:(Fin A),(Fin A):] holds b₂ . (a,b) = a \ b );