theorem :: JORDAN2B:30

for p being Element of (TOP-REAL 2) holds
( p /. 1 = proj1 . p & p /. 2 = proj2 . p )