( the carrier of T c= the carrier of [:I[01] ,I[01] :] & x in the carrier of T ) by BORSUK_1:35;
then reconsider x9 = x as Point of [:I[01] ,I[01] :] ;
x9 `2 is real ;
hence x `2 is real ; :: thesis: verum