theorem Th8: :: JGRAPH_2:8

for p being Point of (TOP-REAL 2) holds p = |[(proj1 . p),(proj2 . p)]|