let S1, S2, T1, T2 be non empty TopSpace; for R being Refinement of [:S1,T1:],[:S2,T2:] st the carrier of S1 = the carrier of S2 & the carrier of T1 = the carrier of T2 holds
{ ([:U1,V1:] /\ [:U2,V2:]) where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : ( U1 is open & U2 is open & V1 is open & V2 is open ) } is Basis of R
let R be Refinement of [:S1,T1:],[:S2,T2:]; ( the carrier of S1 = the carrier of S2 & the carrier of T1 = the carrier of T2 implies { ([:U1,V1:] /\ [:U2,V2:]) where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : ( U1 is open & U2 is open & V1 is open & V2 is open ) } is Basis of R )
assume A1:
( the carrier of S1 = the carrier of S2 & the carrier of T1 = the carrier of T2 )
; { ([:U1,V1:] /\ [:U2,V2:]) where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : ( U1 is open & U2 is open & V1 is open & V2 is open ) } is Basis of R
set Y = { ([:U1,V1:] /\ [:U2,V2:]) where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : ( U1 is open & U2 is open & V1 is open & V2 is open ) } ;
A2:
the carrier of [:S2,T2:] = [: the carrier of S2, the carrier of T2:]
by BORSUK_1:def 2;
A3:
the carrier of [:S1,T1:] = [: the carrier of S1, the carrier of T1:]
by BORSUK_1:def 2;
then reconsider BST = INTERSECTION ( the topology of [:S1,T1:], the topology of [:S2,T2:]) as Basis of R by A1, A2, YELLOW_9:60;
A4: the carrier of R =
the carrier of [:S1,T1:] \/ the carrier of [:S2,T2:]
by YELLOW_9:def 6
.=
[: the carrier of S1, the carrier of T1:] \/ [: the carrier of S2, the carrier of T2:]
by A3, BORSUK_1:def 2
.=
[: the carrier of S1, the carrier of T1:]
by A1
;
{ ([:U1,V1:] /\ [:U2,V2:]) where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : ( U1 is open & U2 is open & V1 is open & V2 is open ) } c= bool the carrier of R
proof
let c be
object ;
TARSKI:def 3 ( not c in { ([:U1,V1:] /\ [:U2,V2:]) where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : ( U1 is open & U2 is open & V1 is open & V2 is open ) } or c in bool the carrier of R )
assume
c in { ([:U1,V1:] /\ [:U2,V2:]) where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : ( U1 is open & U2 is open & V1 is open & V2 is open ) }
;
c in bool the carrier of R
then
ex
U1 being
Subset of
S1 ex
U2 being
Subset of
S2 ex
V1 being
Subset of
T1 ex
V2 being
Subset of
T2 st
(
c = [:U1,V1:] /\ [:U2,V2:] &
U1 is
open &
U2 is
open &
V1 is
open &
V2 is
open )
;
hence
c in bool the
carrier of
R
by A1, A2, A4;
verum
end;
then reconsider C1 = { ([:U1,V1:] /\ [:U2,V2:]) where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : ( U1 is open & U2 is open & V1 is open & V2 is open ) } as Subset-Family of R ;
reconsider C1 = C1 as Subset-Family of R ;
A5:
the topology of [:S2,T2:] = { (union A) where A is Subset-Family of [:S2,T2:] : A c= { [:X1,Y1:] where X1 is Subset of S2, Y1 is Subset of T2 : ( X1 in the topology of S2 & Y1 in the topology of T2 ) } }
by BORSUK_1:def 2;
A6:
the topology of [:S1,T1:] = { (union A) where A is Subset-Family of [:S1,T1:] : A c= { [:X1,Y1:] where X1 is Subset of S1, Y1 is Subset of T1 : ( X1 in the topology of S1 & Y1 in the topology of T1 ) } }
by BORSUK_1:def 2;
A7:
for A being Subset of R st A is open holds
for p being Point of R st p in A holds
ex a being Subset of R st
( a in C1 & p in a & a c= A )
proof
let A be
Subset of
R;
( A is open implies for p being Point of R st p in A holds
ex a being Subset of R st
( a in C1 & p in a & a c= A ) )
assume A8:
A is
open
;
for p being Point of R st p in A holds
ex a being Subset of R st
( a in C1 & p in a & a c= A )
let p be
Point of
R;
( p in A implies ex a being Subset of R st
( a in C1 & p in a & a c= A ) )
assume
p in A
;
ex a being Subset of R st
( a in C1 & p in a & a c= A )
then consider X being
Subset of
R such that A9:
X in BST
and A10:
p in X
and A11:
X c= A
by A8, YELLOW_9:31;
consider X1,
X2 being
set such that A12:
X1 in the
topology of
[:S1,T1:]
and A13:
X2 in the
topology of
[:S2,T2:]
and A14:
X = X1 /\ X2
by A9, SETFAM_1:def 5;
consider F1 being
Subset-Family of
[:S1,T1:] such that A15:
X1 = union F1
and A16:
F1 c= { [:K1,L1:] where K1 is Subset of S1, L1 is Subset of T1 : ( K1 in the topology of S1 & L1 in the topology of T1 ) }
by A6, A12;
p in X1
by A10, A14, XBOOLE_0:def 4;
then consider G1 being
set such that A17:
p in G1
and A18:
G1 in F1
by A15, TARSKI:def 4;
A19:
G1 in { [:K1,L1:] where K1 is Subset of S1, L1 is Subset of T1 : ( K1 in the topology of S1 & L1 in the topology of T1 ) }
by A16, A18;
consider F2 being
Subset-Family of
[:S2,T2:] such that A20:
X2 = union F2
and A21:
F2 c= { [:K2,L2:] where K2 is Subset of S2, L2 is Subset of T2 : ( K2 in the topology of S2 & L2 in the topology of T2 ) }
by A5, A13;
p in X2
by A10, A14, XBOOLE_0:def 4;
then consider G2 being
set such that A22:
p in G2
and A23:
G2 in F2
by A20, TARSKI:def 4;
G2 in { [:K2,L2:] where K2 is Subset of S2, L2 is Subset of T2 : ( K2 in the topology of S2 & L2 in the topology of T2 ) }
by A21, A23;
then consider K2 being
Subset of
S2,
L2 being
Subset of
T2 such that A24:
G2 = [:K2,L2:]
and A25:
(
K2 in the
topology of
S2 &
L2 in the
topology of
T2 )
;
A26:
[:K2,L2:] c= X2
by A20, A23, A24, ZFMISC_1:74;
A27:
(
K2 is
open &
L2 is
open )
by A25;
consider K1 being
Subset of
S1,
L1 being
Subset of
T1 such that A28:
G1 = [:K1,L1:]
and A29:
(
K1 in the
topology of
S1 &
L1 in the
topology of
T1 )
by A19;
reconsider a =
[:K1,L1:] /\ [:K2,L2:] as
Subset of
R by A1, A4, BORSUK_1:def 2;
take
a
;
( a in C1 & p in a & a c= A )
(
K1 is
open &
L1 is
open )
by A29;
hence
a in C1
by A27;
( p in a & a c= A )
thus
p in a
by A17, A22, A28, A24, XBOOLE_0:def 4;
a c= A
[:K1,L1:] c= X1
by A15, A18, A28, ZFMISC_1:74;
then
a c= X
by A14, A26, XBOOLE_1:27;
hence
a c= A
by A11;
verum
end;
{ ([:U1,V1:] /\ [:U2,V2:]) where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : ( U1 is open & U2 is open & V1 is open & V2 is open ) } c= the topology of R
proof
let c be
object ;
TARSKI:def 3 ( not c in { ([:U1,V1:] /\ [:U2,V2:]) where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : ( U1 is open & U2 is open & V1 is open & V2 is open ) } or c in the topology of R )
A30:
BST c= the
topology of
R
by TOPS_2:64;
assume
c in { ([:U1,V1:] /\ [:U2,V2:]) where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : ( U1 is open & U2 is open & V1 is open & V2 is open ) }
;
c in the topology of R
then consider U1 being
Subset of
S1,
U2 being
Subset of
S2,
V1 being
Subset of
T1,
V2 being
Subset of
T2 such that A31:
c = [:U1,V1:] /\ [:U2,V2:]
and A32:
U1 is
open
and A33:
U2 is
open
and A34:
V1 is
open
and A35:
V2 is
open
;
[:U2,V2:] is
open
by A33, A35, BORSUK_1:6;
then A36:
[:U2,V2:] in the
topology of
[:S2,T2:]
;
[:U1,V1:] is
open
by A32, A34, BORSUK_1:6;
then
[:U1,V1:] in the
topology of
[:S1,T1:]
;
then
c in BST
by A31, A36, SETFAM_1:def 5;
hence
c in the
topology of
R
by A30;
verum
end;
hence
{ ([:U1,V1:] /\ [:U2,V2:]) where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : ( U1 is open & U2 is open & V1 is open & V2 is open ) } is Basis of R
by A7, YELLOW_9:32; verum