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 `2 in the carrier of T by MCART_1:10;
hence p `2 is real ; :: thesis: verum