let S, T be non empty TopSpace; :: thesis: for p being Point of [:S,T:] holds
( p `1 is Point of S & p `2 is Point of T )
let p be Point of [:S,T:]; :: thesis: ( p `1 is Point of S & p `2 is Point of T )
p in the carrier of [:S,T:] ;
then p in [: the carrier of S, the carrier of T:] by BORSUK_1:def 2;
hence ( p `1 is Point of S & p `2 is Point of T ) by MCART_1:10; :: thesis: verum