let S, T be TopSpace; :: thesis: for A being Subset of S
for B being Subset of T st A is connected & B is connected holds
[:A,B:] is connected
let A be Subset of S; :: thesis: for B being Subset of T st A is connected & B is connected holds
[:A,B:] is connected
let B be Subset of T; :: thesis: ( A is connected & B is connected implies [:A,B:] is connected )
assume ( S | A is connected & T | B is connected ) ; :: according to CONNSP_1:def 3 :: thesis: [:A,B:] is connected
then reconsider SA = S | A, TB = T | B as connected TopSpace ;
[:SA,TB:] is connected ;
hence [:S,T:] | [:A,B:] is connected by BORSUK_3:22; :: according to CONNSP_1:def 3 :: thesis: verum