theorem Th37: :: YELLOW12:37

for T being non empty TopSpace holds id the carrier of T = { p where p is Point of [:T,T:] : (pr1 ( the carrier of T, the carrier of T)) . p = (pr2 ( the carrier of T, the carrier of T)) . p }