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