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