thus dom proj2 = the carrier of (TOP-REAL 2) by FUNCT_2:def 1; :: thesis: dom proj2 = REAL 2
hence dom proj2 = REAL 2 by EUCLID:22; :: thesis: verum