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