theorem Th7: :: JGRAPH_2:7

( dom proj2 = the carrier of (TOP-REAL 2) & dom proj2 = REAL 2 )