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