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