for p1 being Point of (TOP-REAL 3) holds p1 <X> p1 = 0. (TOP-REAL 3) by Th4;