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 )
proof
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 ) )
proof
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 ) )
proof
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
proof
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;
(pr1 ( the carrier of T1, the carrier of T2)) . (tx1,tx2) = tx1 by A11, FUNCT_3:def 4;
hence t in tX1 by A6, A12, A7, A9, ZFMISC_1:87; :: thesis: verum
end;
hence ( t in X1 iff ex U being Subset of T1 st
( U is open & U c= X1 & t in U ) ) ; :: thesis: verum
end;
hence X1 is open by TOPS_1:25; :: thesis: verum
end;
thus ( X2 = (pr2 ( the carrier of T1, the carrier of T2)) .: (D /\ [:{x1}, the carrier of T2:]) implies X2 is open ) :: 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 ) )
proof
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 ) )
proof
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
proof
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;
tx2 in tX2 by A24, A21, A26, ZFMISC_1:87;
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;
hence ( t in X2 iff ex U being Subset of T2 st
( U is open & U c= X2 & t in U ) ) ; :: thesis: verum
end;
hence X2 is open by TOPS_1:25; :: thesis: verum
end;