let T1, T2 be non empty TopSpace; :: thesis: for D being Subset of [:T1,T2:] st D is open holds

for x1 being Point of T1

for x2 being Point of T2

for X1 being Subset of T1

for X2 being Subset of T2 holds

( ( X1 = (pr1 ( the carrier of T1, the carrier of T2)) .: (D /\ [: the carrier of T1,{x2}:]) implies X1 is open ) & ( X2 = (pr2 ( the carrier of T1, the carrier of T2)) .: (D /\ [:{x1}, the carrier of T2:]) implies X2 is open ) )

set cT1 = the carrier of T1;

set cT2 = the carrier of T2;

let D be Subset of [:T1,T2:]; :: thesis: ( D is open implies for x1 being Point of T1

for x2 being Point of T2

for X1 being Subset of T1

for X2 being Subset of T2 holds

( ( X1 = (pr1 ( the carrier of T1, the carrier of T2)) .: (D /\ [: the carrier of T1,{x2}:]) implies X1 is open ) & ( X2 = (pr2 ( the carrier of T1, the carrier of T2)) .: (D /\ [:{x1}, the carrier of T2:]) implies X2 is open ) ) )

assume D is open ; :: thesis: for x1 being Point of T1

for x2 being Point of T2

for X1 being Subset of T1

for X2 being Subset of T2 holds

( ( X1 = (pr1 ( the carrier of T1, the carrier of T2)) .: (D /\ [: the carrier of T1,{x2}:]) implies X1 is open ) & ( X2 = (pr2 ( the carrier of T1, the carrier of T2)) .: (D /\ [:{x1}, the carrier of T2:]) implies X2 is open ) )

then consider FA being Subset-Family of [:T1,T2:] such that

A1: D = union FA and

A2: for B being set st B in FA holds

ex B1 being Subset of T1 ex B2 being Subset of T2 st

( B = [:B1,B2:] & B1 is open & B2 is open ) by BORSUK_1:5;

let x1 be Point of T1; :: thesis: for x2 being Point of T2

for X1 being Subset of T1

for X2 being Subset of T2 holds

( ( X1 = (pr1 ( the carrier of T1, the carrier of T2)) .: (D /\ [: the carrier of T1,{x2}:]) implies X1 is open ) & ( X2 = (pr2 ( the carrier of T1, the carrier of T2)) .: (D /\ [:{x1}, the carrier of T2:]) implies X2 is open ) )

let x2 be Point of T2; :: thesis: for X1 being Subset of T1

for X2 being Subset of T2 holds

( ( X1 = (pr1 ( the carrier of T1, the carrier of T2)) .: (D /\ [: the carrier of T1,{x2}:]) implies X1 is open ) & ( X2 = (pr2 ( the carrier of T1, the carrier of T2)) .: (D /\ [:{x1}, the carrier of T2:]) implies X2 is open ) )

let X1 be Subset of T1; :: thesis: for X2 being Subset of T2 holds

( ( X1 = (pr1 ( the carrier of T1, the carrier of T2)) .: (D /\ [: the carrier of T1,{x2}:]) implies X1 is open ) & ( X2 = (pr2 ( the carrier of T1, the carrier of T2)) .: (D /\ [:{x1}, the carrier of T2:]) implies X2 is open ) )

let X2 be Subset of T2; :: thesis: ( ( X1 = (pr1 ( the carrier of T1, the carrier of T2)) .: (D /\ [: the carrier of T1,{x2}:]) implies X1 is open ) & ( X2 = (pr2 ( the carrier of T1, the carrier of T2)) .: (D /\ [:{x1}, the carrier of T2:]) implies X2 is open ) )

thus ( X1 = (pr1 ( the carrier of T1, the carrier of T2)) .: (D /\ [: the carrier of T1,{x2}:]) implies X1 is open ) :: thesis: ( X2 = (pr2 ( the carrier of T1, the carrier of T2)) .: (D /\ [:{x1}, the carrier of T2:]) implies X2 is open )

for x1 being Point of T1

for x2 being Point of T2

for X1 being Subset of T1

for X2 being Subset of T2 holds

( ( X1 = (pr1 ( the carrier of T1, the carrier of T2)) .: (D /\ [: the carrier of T1,{x2}:]) implies X1 is open ) & ( X2 = (pr2 ( the carrier of T1, the carrier of T2)) .: (D /\ [:{x1}, the carrier of T2:]) implies X2 is open ) )

set cT1 = the carrier of T1;

set cT2 = the carrier of T2;

let D be Subset of [:T1,T2:]; :: thesis: ( D is open implies for x1 being Point of T1

for x2 being Point of T2

for X1 being Subset of T1

for X2 being Subset of T2 holds

( ( X1 = (pr1 ( the carrier of T1, the carrier of T2)) .: (D /\ [: the carrier of T1,{x2}:]) implies X1 is open ) & ( X2 = (pr2 ( the carrier of T1, the carrier of T2)) .: (D /\ [:{x1}, the carrier of T2:]) implies X2 is open ) ) )

assume D is open ; :: thesis: for x1 being Point of T1

for x2 being Point of T2

for X1 being Subset of T1

for X2 being Subset of T2 holds

( ( X1 = (pr1 ( the carrier of T1, the carrier of T2)) .: (D /\ [: the carrier of T1,{x2}:]) implies X1 is open ) & ( X2 = (pr2 ( the carrier of T1, the carrier of T2)) .: (D /\ [:{x1}, the carrier of T2:]) implies X2 is open ) )

then consider FA being Subset-Family of [:T1,T2:] such that

A1: D = union FA and

A2: for B being set st B in FA holds

ex B1 being Subset of T1 ex B2 being Subset of T2 st

( B = [:B1,B2:] & B1 is open & B2 is open ) by BORSUK_1:5;

let x1 be Point of T1; :: thesis: for x2 being Point of T2

for X1 being Subset of T1

for X2 being Subset of T2 holds

( ( X1 = (pr1 ( the carrier of T1, the carrier of T2)) .: (D /\ [: the carrier of T1,{x2}:]) implies X1 is open ) & ( X2 = (pr2 ( the carrier of T1, the carrier of T2)) .: (D /\ [:{x1}, the carrier of T2:]) implies X2 is open ) )

let x2 be Point of T2; :: thesis: for X1 being Subset of T1

for X2 being Subset of T2 holds

( ( X1 = (pr1 ( the carrier of T1, the carrier of T2)) .: (D /\ [: the carrier of T1,{x2}:]) implies X1 is open ) & ( X2 = (pr2 ( the carrier of T1, the carrier of T2)) .: (D /\ [:{x1}, the carrier of T2:]) implies X2 is open ) )

let X1 be Subset of T1; :: thesis: for X2 being Subset of T2 holds

( ( X1 = (pr1 ( the carrier of T1, the carrier of T2)) .: (D /\ [: the carrier of T1,{x2}:]) implies X1 is open ) & ( X2 = (pr2 ( the carrier of T1, the carrier of T2)) .: (D /\ [:{x1}, the carrier of T2:]) implies X2 is open ) )

let X2 be Subset of T2; :: thesis: ( ( X1 = (pr1 ( the carrier of T1, the carrier of T2)) .: (D /\ [: the carrier of T1,{x2}:]) implies X1 is open ) & ( X2 = (pr2 ( the carrier of T1, the carrier of T2)) .: (D /\ [:{x1}, the carrier of T2:]) implies X2 is open ) )

thus ( X1 = (pr1 ( the carrier of T1, the carrier of T2)) .: (D /\ [: the carrier of T1,{x2}:]) implies X1 is open ) :: thesis: ( X2 = (pr2 ( the carrier of T1, the carrier of T2)) .: (D /\ [:{x1}, the carrier of T2:]) implies X2 is open )

proof

thus
( X2 = (pr2 ( the carrier of T1, the carrier of T2)) .: (D /\ [:{x1}, the carrier of T2:]) implies X2 is open )
:: thesis: verum
assume A3:
X1 = (pr1 ( the carrier of T1, the carrier of T2)) .: (D /\ [: the carrier of T1,{x2}:])
; :: thesis: X1 is open

for t being set holds

( t in X1 iff ex U being Subset of T1 st

( U is open & U c= X1 & t in U ) )

end;for t being set holds

( t in X1 iff ex U being Subset of T1 st

( U is open & U c= X1 & t in U ) )

proof

hence
X1 is open
by TOPS_1:25; :: thesis: verum
let t be set ; :: thesis: ( t in X1 iff ex U being Subset of T1 st

( U is open & U c= X1 & t in U ) )

( t in X1 implies ex U being Subset of T1 st

( U is open & U c= X1 & t in U ) )

( U is open & U c= X1 & t in U ) ) ; :: thesis: verum

end;( U is open & U c= X1 & t in U ) )

( t in X1 implies ex U being Subset of T1 st

( U is open & U c= X1 & t in U ) )

proof

hence
( t in X1 iff ex U being Subset of T1 st
assume
t in X1
; :: thesis: ex U being Subset of T1 st

( U is open & U c= X1 & t in U )

then consider tx being object such that

A4: tx in dom (pr1 ( the carrier of T1, the carrier of T2)) and

A5: tx in D /\ [: the carrier of T1,{x2}:] and

A6: t = (pr1 ( the carrier of T1, the carrier of T2)) . tx by A3, FUNCT_1:def 6;

tx in D by A5, XBOOLE_0:def 4;

then consider tX being set such that

A7: tx in tX and

A8: tX in FA by A1, TARSKI:def 4;

consider tX1 being Subset of T1, tX2 being Subset of T2 such that

A9: tX = [:tX1,tX2:] and

A10: tX1 is open and

tX2 is open by A2, A8;

take tX1 ; :: thesis: ( tX1 is open & tX1 c= X1 & t in tX1 )

thus tX1 is open by A10; :: thesis: ( tX1 c= X1 & t in tX1 )

consider tx1, tx2 being object such that

A11: ( tx1 in the carrier of T1 & tx2 in the carrier of T2 ) and

A12: tx = [tx1,tx2] by A4, ZFMISC_1:def 2;

thus tX1 c= X1 :: thesis: t in tX1

hence t in tX1 by A6, A12, A7, A9, ZFMISC_1:87; :: thesis: verum

end;( U is open & U c= X1 & t in U )

then consider tx being object such that

A4: tx in dom (pr1 ( the carrier of T1, the carrier of T2)) and

A5: tx in D /\ [: the carrier of T1,{x2}:] and

A6: t = (pr1 ( the carrier of T1, the carrier of T2)) . tx by A3, FUNCT_1:def 6;

tx in D by A5, XBOOLE_0:def 4;

then consider tX being set such that

A7: tx in tX and

A8: tX in FA by A1, TARSKI:def 4;

consider tX1 being Subset of T1, tX2 being Subset of T2 such that

A9: tX = [:tX1,tX2:] and

A10: tX1 is open and

tX2 is open by A2, A8;

take tX1 ; :: thesis: ( tX1 is open & tX1 c= X1 & t in tX1 )

thus tX1 is open by A10; :: thesis: ( tX1 c= X1 & t in tX1 )

consider tx1, tx2 being object such that

A11: ( tx1 in the carrier of T1 & tx2 in the carrier of T2 ) and

A12: tx = [tx1,tx2] by A4, ZFMISC_1:def 2;

thus tX1 c= X1 :: thesis: t in tX1

proof

(pr1 ( the carrier of T1, the carrier of T2)) . (tx1,tx2) = tx1
by A11, FUNCT_3:def 4;
tx in [: the carrier of T1,{x2}:]
by A5, XBOOLE_0:def 4;

then A13: tx2 = x2 by A12, ZFMISC_1:106;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in tX1 or a in X1 )

assume A14: a in tX1 ; :: thesis: a in X1

[a,x2] in [: the carrier of T1, the carrier of T2:] by A14, ZFMISC_1:87;

then A15: [a,x2] in dom (pr1 ( the carrier of T1, the carrier of T2)) by FUNCT_3:def 4;

tx2 in tX2 by A12, A7, A9, ZFMISC_1:87;

then [a,x2] in [:tX1,tX2:] by A14, A13, ZFMISC_1:87;

then A16: [a,x2] in union FA by A8, A9, TARSKI:def 4;

[a,x2] in [: the carrier of T1,{x2}:] by A14, ZFMISC_1:106;

then [a,x2] in D /\ [: the carrier of T1,{x2}:] by A1, A16, XBOOLE_0:def 4;

then (pr1 ( the carrier of T1, the carrier of T2)) . (a,x2) in (pr1 ( the carrier of T1, the carrier of T2)) .: (D /\ [: the carrier of T1,{x2}:]) by A15, FUNCT_1:def 6;

hence a in X1 by A3, A14, FUNCT_3:def 4; :: thesis: verum

end;then A13: tx2 = x2 by A12, ZFMISC_1:106;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in tX1 or a in X1 )

assume A14: a in tX1 ; :: thesis: a in X1

[a,x2] in [: the carrier of T1, the carrier of T2:] by A14, ZFMISC_1:87;

then A15: [a,x2] in dom (pr1 ( the carrier of T1, the carrier of T2)) by FUNCT_3:def 4;

tx2 in tX2 by A12, A7, A9, ZFMISC_1:87;

then [a,x2] in [:tX1,tX2:] by A14, A13, ZFMISC_1:87;

then A16: [a,x2] in union FA by A8, A9, TARSKI:def 4;

[a,x2] in [: the carrier of T1,{x2}:] by A14, ZFMISC_1:106;

then [a,x2] in D /\ [: the carrier of T1,{x2}:] by A1, A16, XBOOLE_0:def 4;

then (pr1 ( the carrier of T1, the carrier of T2)) . (a,x2) in (pr1 ( the carrier of T1, the carrier of T2)) .: (D /\ [: the carrier of T1,{x2}:]) by A15, FUNCT_1:def 6;

hence a in X1 by A3, A14, FUNCT_3:def 4; :: thesis: verum

hence t in tX1 by A6, A12, A7, A9, ZFMISC_1:87; :: thesis: verum

( U is open & U c= X1 & t in U ) ) ; :: thesis: verum

proof

assume A17:
X2 = (pr2 ( the carrier of T1, the carrier of T2)) .: (D /\ [:{x1}, the carrier of T2:])
; :: thesis: X2 is open

for t being set holds

( t in X2 iff ex U being Subset of T2 st

( U is open & U c= X2 & t in U ) )

end;for t being set holds

( t in X2 iff ex U being Subset of T2 st

( U is open & U c= X2 & t in U ) )

proof

hence
X2 is open
by TOPS_1:25; :: thesis: verum
let t be set ; :: thesis: ( t in X2 iff ex U being Subset of T2 st

( U is open & U c= X2 & t in U ) )

( t in X2 implies ex U being Subset of T2 st

( U is open & U c= X2 & t in U ) )

( U is open & U c= X2 & t in U ) ) ; :: thesis: verum

end;( U is open & U c= X2 & t in U ) )

( t in X2 implies ex U being Subset of T2 st

( U is open & U c= X2 & t in U ) )

proof

hence
( t in X2 iff ex U being Subset of T2 st
assume
t in X2
; :: thesis: ex U being Subset of T2 st

( U is open & U c= X2 & t in U )

then consider tx being object such that

A18: tx in dom (pr2 ( the carrier of T1, the carrier of T2)) and

A19: tx in D /\ [:{x1}, the carrier of T2:] and

A20: t = (pr2 ( the carrier of T1, the carrier of T2)) . tx by A17, FUNCT_1:def 6;

tx in D by A19, XBOOLE_0:def 4;

then consider tX being set such that

A21: tx in tX and

A22: tX in FA by A1, TARSKI:def 4;

consider tx1, tx2 being object such that

A23: ( tx1 in the carrier of T1 & tx2 in the carrier of T2 ) and

A24: tx = [tx1,tx2] by A18, ZFMISC_1:def 2;

A25: (pr2 ( the carrier of T1, the carrier of T2)) . (tx1,tx2) = tx2 by A23, FUNCT_3:def 5;

consider tX1 being Subset of T1, tX2 being Subset of T2 such that

A26: tX = [:tX1,tX2:] and

tX1 is open and

A27: tX2 is open by A2, A22;

A28: tX2 c= X2

hence ex U being Subset of T2 st

( U is open & U c= X2 & t in U ) by A20, A24, A27, A25, A28; :: thesis: verum

end;( U is open & U c= X2 & t in U )

then consider tx being object such that

A18: tx in dom (pr2 ( the carrier of T1, the carrier of T2)) and

A19: tx in D /\ [:{x1}, the carrier of T2:] and

A20: t = (pr2 ( the carrier of T1, the carrier of T2)) . tx by A17, FUNCT_1:def 6;

tx in D by A19, XBOOLE_0:def 4;

then consider tX being set such that

A21: tx in tX and

A22: tX in FA by A1, TARSKI:def 4;

consider tx1, tx2 being object such that

A23: ( tx1 in the carrier of T1 & tx2 in the carrier of T2 ) and

A24: tx = [tx1,tx2] by A18, ZFMISC_1:def 2;

A25: (pr2 ( the carrier of T1, the carrier of T2)) . (tx1,tx2) = tx2 by A23, FUNCT_3:def 5;

consider tX1 being Subset of T1, tX2 being Subset of T2 such that

A26: tX = [:tX1,tX2:] and

tX1 is open and

A27: tX2 is open by A2, A22;

A28: tX2 c= X2

proof

tx2 in tX2
by A24, A21, A26, ZFMISC_1:87;
tx in [:{x1}, the carrier of T2:]
by A19, XBOOLE_0:def 4;

then A29: tx1 = x1 by A24, ZFMISC_1:105;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in tX2 or a in X2 )

assume A30: a in tX2 ; :: thesis: a in X2

[x1,a] in [: the carrier of T1, the carrier of T2:] by A30, ZFMISC_1:87;

then A31: [x1,a] in dom (pr2 ( the carrier of T1, the carrier of T2)) by FUNCT_3:def 5;

tx1 in tX1 by A24, A21, A26, ZFMISC_1:87;

then [x1,a] in [:tX1,tX2:] by A30, A29, ZFMISC_1:87;

then A32: [x1,a] in union FA by A22, A26, TARSKI:def 4;

[x1,a] in [:{x1}, the carrier of T2:] by A30, ZFMISC_1:105;

then [x1,a] in D /\ [:{x1}, the carrier of T2:] by A1, A32, XBOOLE_0:def 4;

then (pr2 ( the carrier of T1, the carrier of T2)) . (x1,a) in (pr2 ( the carrier of T1, the carrier of T2)) .: (D /\ [:{x1}, the carrier of T2:]) by A31, FUNCT_1:def 6;

hence a in X2 by A17, A30, FUNCT_3:def 5; :: thesis: verum

end;then A29: tx1 = x1 by A24, ZFMISC_1:105;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in tX2 or a in X2 )

assume A30: a in tX2 ; :: thesis: a in X2

[x1,a] in [: the carrier of T1, the carrier of T2:] by A30, ZFMISC_1:87;

then A31: [x1,a] in dom (pr2 ( the carrier of T1, the carrier of T2)) by FUNCT_3:def 5;

tx1 in tX1 by A24, A21, A26, ZFMISC_1:87;

then [x1,a] in [:tX1,tX2:] by A30, A29, ZFMISC_1:87;

then A32: [x1,a] in union FA by A22, A26, TARSKI:def 4;

[x1,a] in [:{x1}, the carrier of T2:] by A30, ZFMISC_1:105;

then [x1,a] in D /\ [:{x1}, the carrier of T2:] by A1, A32, XBOOLE_0:def 4;

then (pr2 ( the carrier of T1, the carrier of T2)) . (x1,a) in (pr2 ( the carrier of T1, the carrier of T2)) .: (D /\ [:{x1}, the carrier of T2:]) by A31, FUNCT_1:def 6;

hence a in X2 by A17, A30, FUNCT_3:def 5; :: thesis: verum

hence ex U being Subset of T2 st

( U is open & U c= X2 & t in U ) by A20, A24, A27, A25, A28; :: thesis: verum

( U is open & U c= X2 & t in U ) ) ; :: thesis: verum