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

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