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