:: deftheorem Def4 defines diffX1_X2_2 JORDAN:def 4 :
for b₁ being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] holds
( b₁ = diffX1_X2_2 iff for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b₁ . x = ((x `1) `2) - ((x `2) `2) );