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 ) )
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 A1:
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 ) )
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 ) )
set cT1 = the carrier of T1;
set cT2 = the carrier of T2;
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 ) )
consider FA being Subset-Family of [:T1,T2:] such that
A2:
( D = union FA & ( 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 A1, BORSUK_1:45;
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
set such that A4:
(
tx in dom (pr1 the carrier of T1,the carrier of T2) &
tx in D /\ [:the carrier of T1,{x2}:] &
t = (pr1 the carrier of T1,the carrier of T2) . tx )
by A3, FUNCT_1:def 12;
consider tx1,
tx2 being
set such that A5:
(
tx1 in the
carrier of
T1 &
tx2 in the
carrier of
T2 &
tx = [tx1,tx2] )
by A4, ZFMISC_1:def 2;
tx in D
by A4, XBOOLE_0:def 4;
then consider tX being
set such that A6:
(
tx in tX &
tX in FA )
by A2, TARSKI:def 4;
consider tX1 being
Subset of
T1,
tX2 being
Subset of
T2 such that A7:
(
tX = [:tX1,tX2:] &
tX1 is
open &
tX2 is
open )
by A2, A6;
take
tX1
;
:: thesis: ( tX1 is open & tX1 c= X1 & t in tX1 )
thus
tX1 is
open
by A7;
:: thesis: ( tX1 c= X1 & t in tX1 )
A8:
(
tx1 in tX1 &
(pr1 the carrier of T1,the carrier of T2) . tx1,
tx2 = tx1 )
by A5, A6, A7, FUNCT_3:def 5, ZFMISC_1:106;
thus
tX1 c= X1
:: thesis: t in tX1proof
let a be
set ;
:: according to TARSKI:def 3 :: thesis: ( not a in tX1 or a in X1 )
assume A9:
a in tX1
;
:: thesis: a in X1
tx in [:the carrier of T1,{x2}:]
by A4, XBOOLE_0:def 4;
then
(
tx2 = x2 &
tx2 in tX2 )
by A5, A6, A7, ZFMISC_1:106, ZFMISC_1:129;
then
(
[a,x2] in [:tX1,tX2:] &
[a,x2] in [:the carrier of T1,the carrier of T2:] )
by A9, ZFMISC_1:106;
then A10:
(
[a,x2] in union FA &
[a,x2] in [:the carrier of T1,{x2}:] &
[a,x2] in dom (pr1 the carrier of T1,the carrier of T2) )
by A6, A7, A9, FUNCT_3:def 5, TARSKI:def 4, ZFMISC_1:129;
then
[a,x2] in D /\ [:the carrier of T1,{x2}:]
by A2, 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}:]) &
(pr1 the carrier of T1,the carrier of T2) . a,
x2 = a )
by A9, A10, FUNCT_1:def 12, FUNCT_3:def 5;
hence
a in X1
by A3;
:: thesis: verum
end;
thus
t in tX1
by A4, A5, A8;
:: 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:57;
:: 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: verumproof
assume A11:
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
set such that A12:
(
tx in dom (pr2 the carrier of T1,the carrier of T2) &
tx in D /\ [:{x1},the carrier of T2:] &
t = (pr2 the carrier of T1,the carrier of T2) . tx )
by A11, FUNCT_1:def 12;
consider tx1,
tx2 being
set such that A13:
(
tx1 in the
carrier of
T1 &
tx2 in the
carrier of
T2 &
tx = [tx1,tx2] )
by A12, ZFMISC_1:def 2;
tx in D
by A12, XBOOLE_0:def 4;
then consider tX being
set such that A14:
(
tx in tX &
tX in FA )
by A2, TARSKI:def 4;
consider tX1 being
Subset of
T1,
tX2 being
Subset of
T2 such that A15:
(
tX = [:tX1,tX2:] &
tX1 is
open &
tX2 is
open )
by A2, A14;
A16:
(
tx2 in tX2 &
(pr2 the carrier of T1,the carrier of T2) . tx1,
tx2 = tx2 )
by A13, A14, A15, FUNCT_3:def 6, ZFMISC_1:106;
tX2 c= X2
proof
let a be
set ;
:: according to TARSKI:def 3 :: thesis: ( not a in tX2 or a in X2 )
assume A17:
a in tX2
;
:: thesis: a in X2
tx in [:{x1},the carrier of T2:]
by A12, XBOOLE_0:def 4;
then
(
tx1 = x1 &
tx1 in tX1 )
by A13, A14, A15, ZFMISC_1:106, ZFMISC_1:128;
then
(
[x1,a] in [:tX1,tX2:] &
[x1,a] in [:the carrier of T1,the carrier of T2:] )
by A17, ZFMISC_1:106;
then A18:
(
[x1,a] in union FA &
[x1,a] in [:{x1},the carrier of T2:] &
[x1,a] in dom (pr2 the carrier of T1,the carrier of T2) )
by A14, A15, A17, FUNCT_3:def 6, TARSKI:def 4, ZFMISC_1:128;
then
[x1,a] in D /\ [:{x1},the carrier of T2:]
by A2, 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:]) &
(pr2 the carrier of T1,the carrier of T2) . x1,
a = a )
by A17, A18, FUNCT_1:def 12, FUNCT_3:def 6;
hence
a in X2
by A11;
:: thesis: verum
end;
hence
ex
U being
Subset of
T2 st
(
U is
open &
U c= X2 &
t in U )
by A12, A13, A15, A16;
:: 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:57;
:: thesis: verum
end;