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