let T1, T2 be non empty TopSpace; :: thesis: ( T1 is T_2 & T2 is T_2 implies [:T1,T2:] is T_2 )
assume that
A1: T1 is T_2 and
A2: T2 is T_2 ; :: thesis: [:T1,T2:] is T_2
set T = [:T1,T2:];
[:T1,T2:] is T_2

proof

let p, q be Point of [:T1,T2:]; :: according to PRE_TOPC:def 10 :: thesis: ( p = q or ex b₁, b₂ being Element of bool the carrier of [:T1,T2:] st
( b₁ is open & b₂ is open & p in b₁ & q in b₂ & b₁ misses b₂ ) )
assume A3: p <> q ; :: thesis: ex b₁, b₂ being Element of bool the carrier of [:T1,T2:] st
( b₁ is open & b₂ is open & p in b₁ & q in b₂ & b₁ misses b₂ )
q in the carrier of [:T1,T2:] ;
then q in [: the carrier of T1, the carrier of T2:] by BORSUK_1:def 2;
then consider z, v being set such that
A4: z in the carrier of T1 and
A5: v in the carrier of T2 and
A6: q = [z,v] by ZFMISC_1:def 2;
p in the carrier of [:T1,T2:] ;
then p in [: the carrier of T1, the carrier of T2:] by BORSUK_1:def 2;
then consider x, y being set such that
A7: x in the carrier of T1 and
A8: y in the carrier of T2 and
A9: p = [x,y] by ZFMISC_1:def 2;
reconsider y = y, v = v as Point of T2 by A8, A5;
reconsider x = x, z = z as Point of T1 by A7, A4;

per cases ( x <> z or x = z ) ;

suppose x <> z ; :: thesis: ex b₁, b₂ being Element of bool the carrier of [:T1,T2:] st
( b₁ is open & b₂ is open & p in b₁ & q in b₂ & b₁ misses b₂ )

then consider Y, V being Subset of T1 such that
A10: ( Y is open & V is open ) and
A11: ( x in Y & z in V ) and
A12: Y misses V by A1, PRE_TOPC:def 10;
reconsider Y = Y, V = V as Subset of T1 ;
reconsider X = [:Y,([#] T2):], Z = [:V,([#] T2):] as Subset of [:T1,T2:] ;
A13: X misses Z by A12, ZFMISC_1:104;
A14: ( X is open & Z is open ) by A10, BORSUK_1:6;
( p in X & q in Z ) by A8, A9, A5, A6, A11, ZFMISC_1:87;
hence ex b₁, b₂ being Element of bool the carrier of [:T1,T2:] st
( b₁ is open & b₂ is open & p in b₁ & q in b₂ & b₁ misses b₂ ) by A14, A13; :: thesis: verum

end;

suppose x = z ; :: thesis: ex b₁, b₂ being Element of bool the carrier of [:T1,T2:] st
( b₁ is open & b₂ is open & p in b₁ & q in b₂ & b₁ misses b₂ )

then consider Y, V being Subset of T2 such that
A15: ( Y is open & V is open ) and
A16: ( y in Y & v in V ) and
A17: Y misses V by A2, A3, A9, A6, PRE_TOPC:def 10;
reconsider Y = Y, V = V as Subset of T2 ;
reconsider X = [:([#] T1),Y:], Z = [:([#] T1),V:] as Subset of [:T1,T2:] ;
A18: X misses Z by A17, ZFMISC_1:104;
A19: ( X is open & Z is open ) by A15, BORSUK_1:6;
( p in X & q in Z ) by A7, A9, A4, A6, A16, ZFMISC_1:87;
hence ex b₁, b₂ being Element of bool the carrier of [:T1,T2:] st
( b₁ is open & b₂ is open & p in b₁ & q in b₂ & b₁ misses b₂ ) by A19, A18; :: thesis: verum

end;

end;

end;

hence [:T1,T2:] is T_2 ; :: thesis: verum