A1: 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 A1;
x' `1 is real ;
hence x `1 is real ; :: thesis: verum