theorem Th6: :: JGRAPH_2:6

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