the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by BORSUK_1:def 2;
hence x `2 is Element of T by MCART_1:10; :: thesis: verum