p in the carrier of [:S,T:] ;
then p in [:the carrier of S,the carrier of T:] by BORSUK_1:def 5;
then p `1 in the carrier of S by MCART_1:10;
hence p `1 is real ; :: thesis: verum