thus the carrier of (TOP-REAL 0) is real-membered by EUCLID:22, JORDAN2C:105; :: according to TOPMETR:def 8 :: thesis: verum