let S1, S2, T1, T2 be non empty TopSpace; for R being Refinement of [:S1,T1:],[:S2,T2:]
for R1 being Refinement of S1,S2
for R2 being Refinement of T1,T2 st the carrier of S1 = the carrier of S2 & the carrier of T1 = the carrier of T2 holds
( the carrier of [:R1,R2:] = the carrier of R & the topology of [:R1,R2:] = the topology of R )
let R be Refinement of [:S1,T1:],[:S2,T2:]; for R1 being Refinement of S1,S2
for R2 being Refinement of T1,T2 st the carrier of S1 = the carrier of S2 & the carrier of T1 = the carrier of T2 holds
( the carrier of [:R1,R2:] = the carrier of R & the topology of [:R1,R2:] = the topology of R )
let R1 be Refinement of S1,S2; for R2 being Refinement of T1,T2 st the carrier of S1 = the carrier of S2 & the carrier of T1 = the carrier of T2 holds
( the carrier of [:R1,R2:] = the carrier of R & the topology of [:R1,R2:] = the topology of R )
let R2 be Refinement of T1,T2; ( the carrier of S1 = the carrier of S2 & the carrier of T1 = the carrier of T2 implies ( the carrier of [:R1,R2:] = the carrier of R & the topology of [:R1,R2:] = the topology of R ) )
assume that
A1:
the carrier of S1 = the carrier of S2
and
A2:
the carrier of T1 = the carrier of T2
; ( the carrier of [:R1,R2:] = the carrier of R & the topology of [:R1,R2:] = the topology of R )
A3: the carrier of R1 =
the carrier of S1 \/ the carrier of S2
by YELLOW_9:def 6
.=
the carrier of S1
by A1
;
set C = { ([: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 ) } ;
reconsider BT = INTERSECTION ( the topology of T1, the topology of T2) as Basis of R2 by A2, YELLOW_9:60;
reconsider BS = INTERSECTION ( the topology of S1, the topology of S2) as Basis of R1 by A1, YELLOW_9:60;
reconsider Bpr = { [:a,b:] where a is Subset of R1, b is Subset of R2 : ( a in BS & b in BT ) } as Basis of [:R1,R2:] by YELLOW_9:40;
A4:
{ ([: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 ) } = Bpr
proof
hereby TARSKI:def 3,
XBOOLE_0:def 10 Bpr c= { ([: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 ) }
let c be
object ;
( 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 ) } implies c in Bpr )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 Bprthen consider U1 being
Subset of
S1,
U2 being
Subset of
S2,
V1 being
Subset of
T1,
V2 being
Subset of
T2 such that A5:
c = [:U1,V1:] /\ [:U2,V2:]
and A6:
(
U1 is
open &
U2 is
open )
and A7:
(
V1 is
open &
V2 is
open )
;
(
U1 in the
topology of
S1 &
U2 in the
topology of
S2 )
by A6;
then A8:
U1 /\ U2 in BS
by SETFAM_1:def 5;
(
V1 in the
topology of
T1 &
V2 in the
topology of
T2 )
by A7;
then A9:
V1 /\ V2 in BT
by SETFAM_1:def 5;
c = [:(U1 /\ U2),(V1 /\ V2):]
by A5, ZFMISC_1:100;
hence
c in Bpr
by A8, A9;
verum
end;
let c be
object ;
TARSKI:def 3 ( not c in Bpr or 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 ) } )
assume
c in Bpr
;
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 ) }
then consider a being
Subset of
R1,
b being
Subset of
R2 such that A10:
c = [:a,b:]
and A11:
a in BS
and A12:
b in BT
;
consider a1,
a2 being
set such that A13:
a1 in the
topology of
S1
and A14:
a2 in the
topology of
S2
and A15:
a = a1 /\ a2
by A11, SETFAM_1:def 5;
reconsider a2 =
a2 as
Subset of
S2 by A14;
reconsider a1 =
a1 as
Subset of
S1 by A13;
A16:
(
a1 is
open &
a2 is
open )
by A13, A14;
consider b1,
b2 being
set such that A17:
b1 in the
topology of
T1
and A18:
b2 in the
topology of
T2
and A19:
b = b1 /\ b2
by A12, SETFAM_1:def 5;
reconsider b2 =
b2 as
Subset of
T2 by A18;
reconsider b1 =
b1 as
Subset of
T1 by A17;
A20:
(
b1 is
open &
b2 is
open )
by A17, A18;
c = [:a1,b1:] /\ [:a2,b2:]
by A10, A15, A19, ZFMISC_1:100;
hence
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 ) }
by A16, A20;
verum
end;
A21: the carrier of R2 =
the carrier of T1 \/ the carrier of T2
by YELLOW_9:def 6
.=
the carrier of T1
by A2
;
A22:
the carrier of [:S1,T1:] = [: the carrier of S1, the carrier of T1:]
by BORSUK_1:def 2;
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 A22, BORSUK_1:def 2
.=
[: the carrier of S1, the carrier of T1:]
by A1, A2
;
hence A23:
the carrier of [:R1,R2:] = the carrier of R
by A3, A21, BORSUK_1:def 2; the topology of [:R1,R2:] = the topology of R
{ ([: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 A1, A2, Th48;
hence
the topology of [:R1,R2:] = the topology of R
by A23, A4, YELLOW_9:25; verum