let T1, T2 be non empty TopSpace; 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:]; ( 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
; 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; 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; 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; 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; ( ( 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 )
( 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}:])
;
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 ;
( 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
;
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
;
( tX1 is open & tX1 c= X1 & t in tX1 )
thus
tX1 is
open
by A10;
( 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
t in tX1proof
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 ;
TARSKI:def 3 ( not a in tX1 or a in X1 )
assume A14:
a in tX1
;
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;
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;
verum
end;
hence
(
t in X1 iff ex
U being
Subset of
T1 st
(
U is
open &
U c= X1 &
t in U ) )
;
verum
end;
hence
X1 is
open
by TOPS_1:25;
verum
end;
thus
( X2 = (pr2 ( the carrier of T1, the carrier of T2)) .: (D /\ [:{x1}, the carrier of T2:]) implies X2 is open )
verumproof
assume A17:
X2 = (pr2 ( the carrier of T1, the carrier of T2)) .: (D /\ [:{x1}, the carrier of T2:])
;
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 ;
( 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
;
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 ;
TARSKI:def 3 ( not a in tX2 or a in X2 )
assume A30:
a in tX2
;
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;
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;
verum
end;
hence
(
t in X2 iff ex
U being
Subset of
T2 st
(
U is
open &
U c= X2 &
t in U ) )
;
verum
end;
hence
X2 is
open
by TOPS_1:25;
verum
end;