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