let T1, T2 be non empty TopSpace; for B1 being Basis of T1
for B2 being Basis of T2
for T being Refinement of T1,T2 holds (B1 \/ B2) \/ (INTERSECTION (B1,B2)) is Basis of T
let B1 be Basis of T1; for B2 being Basis of T2
for T being Refinement of T1,T2 holds (B1 \/ B2) \/ (INTERSECTION (B1,B2)) is Basis of T
let B2 be Basis of T2; for T being Refinement of T1,T2 holds (B1 \/ B2) \/ (INTERSECTION (B1,B2)) is Basis of T
let T be Refinement of T1,T2; (B1 \/ B2) \/ (INTERSECTION (B1,B2)) is Basis of T
set BB = (B1 \/ B2) \/ (INTERSECTION (B1,B2));
reconsider B = the topology of T1 \/ the topology of T2 as prebasis of T by Def6;
A1:
FinMeetCl B is Basis of T
by Th23;
A2:
the carrier of T1 \/ the carrier of T2 = the carrier of T
by Def6;
A3:
B1 c= the topology of T1
by TOPS_2:64;
A4:
B2 c= the topology of T2
by TOPS_2:64;
A5:
the topology of T1 c= B
by XBOOLE_1:7;
A6:
the topology of T2 c= B
by XBOOLE_1:7;
A7:
B1 c= B
by A3, A5;
A8:
B2 c= B
by A4, A6;
A9:
B c= FinMeetCl B
by CANTOR_1:4;
then A10:
B1 c= FinMeetCl B
by A7;
A11:
B2 c= FinMeetCl B
by A8, A9;
A12:
B1 \/ B2 c= B
by A3, A4, XBOOLE_1:13;
A13:
INTERSECTION (B1,B2) c= FinMeetCl B
by A10, A11, CANTOR_1:13;
B1 \/ B2 c= FinMeetCl B
by A9, A12;
then A14:
(B1 \/ B2) \/ (INTERSECTION (B1,B2)) c= FinMeetCl B
by A13, XBOOLE_1:8;
A15:
FinMeetCl B c= the topology of T
by A1, TOPS_2:64;
reconsider BB = (B1 \/ B2) \/ (INTERSECTION (B1,B2)) as Subset-Family of T by A14, XBOOLE_1:1;
now for A being Subset of T st A is open holds
for p being Point of T st p in A holds
ex a being Subset of T st
( a in BB & p in a & a c= A )let A be
Subset of
T;
( A is open implies for p being Point of T st p in A holds
ex a being Subset of T st
( a in BB & p in a & a c= A ) )assume A16:
A is
open
;
for p being Point of T st p in A holds
ex a being Subset of T st
( a in BB & p in a & a c= A )let p be
Point of
T;
( p in A implies ex a being Subset of T st
( a in BB & p in a & a c= A ) )assume
p in A
;
ex a being Subset of T st
( a in BB & p in a & a c= A )then consider a being
Subset of
T such that A17:
a in FinMeetCl B
and A18:
p in a
and A19:
a c= A
by A1, A16, Th31;
consider Y being
Subset-Family of
T such that A20:
Y c= B
and A21:
Y is
finite
and A22:
a = Intersect Y
by A17, CANTOR_1:def 3;
reconsider Y1 =
Y /\ the
topology of
T1 as
Subset-Family of
T1 ;
reconsider Y2 =
Y /\ the
topology of
T2 as
Subset-Family of
T2 ;
A23:
Y =
B /\ Y
by A20, XBOOLE_1:28
.=
Y1 \/ Y2
by XBOOLE_1:23
;
the
carrier of
T1 c= the
carrier of
T1
;
then reconsider cT1 = the
carrier of
T1 as
Subset of
T1 ;
the
carrier of
T2 c= the
carrier of
T2
;
then reconsider cT2 = the
carrier of
T2 as
Subset of
T2 ;
A24:
cT1 in the
topology of
T1
by PRE_TOPC:def 1;
A25:
cT2 in the
topology of
T2
by PRE_TOPC:def 1;
A26:
cT1 is
open
by A24;
A27:
cT2 is
open
by A25;
thus
ex
a being
Subset of
T st
(
a in BB &
p in a &
a c= A )
verumproof
per cases
( ( Y1 \/ Y2 = {} & p in cT1 ) or ( Y1 \/ Y2 = {} & p in cT2 ) or ( Y1 = {} & Y2 <> {} & Y <> {} ) or ( Y1 <> {} & Y2 = {} & Y <> {} ) or ( Y1 <> {} & Y2 <> {} & Y <> {} ) )
by A2, XBOOLE_0:def 3;
suppose A38:
(
Y1 = {} &
Y2 <> {} &
Y <> {} )
;
ex a being Subset of T st
( a in BB & p in a & a c= A )then A39:
a =
meet Y2
by A22, A23, SETFAM_1:def 9
.=
Intersect Y2
by A38, SETFAM_1:def 9
;
Y2 c= the
topology of
T2
by XBOOLE_1:17;
then
a in FinMeetCl the
topology of
T2
by A21, A39, CANTOR_1:def 3;
then A40:
a in the
topology of
T2
by CANTOR_1:5;
the
topology of
T2 = UniCl B2
by Th22;
then consider Z being
Subset-Family of
T2 such that A41:
Z c= B2
and A42:
a = union Z
by A40, CANTOR_1:def 1;
consider z being
set such that A43:
p in z
and A44:
z in Z
by A18, A42, TARSKI:def 4;
z in B1 \/ B2
by A41, A44, XBOOLE_0:def 3;
then A45:
z in BB
by XBOOLE_0:def 3;
z c= a
by A42, A44, ZFMISC_1:74;
hence
ex
a being
Subset of
T st
(
a in BB &
p in a &
a c= A )
by A19, A43, A45, XBOOLE_1:1;
verum end; suppose A46:
(
Y1 <> {} &
Y2 = {} &
Y <> {} )
;
ex a being Subset of T st
( a in BB & p in a & a c= A )then A47:
a =
meet Y1
by A22, A23, SETFAM_1:def 9
.=
Intersect Y1
by A46, SETFAM_1:def 9
;
Y1 c= the
topology of
T1
by XBOOLE_1:17;
then
a in FinMeetCl the
topology of
T1
by A21, A47, CANTOR_1:def 3;
then A48:
a in the
topology of
T1
by CANTOR_1:5;
the
topology of
T1 = UniCl B1
by Th22;
then consider Z being
Subset-Family of
T1 such that A49:
Z c= B1
and A50:
a = union Z
by A48, CANTOR_1:def 1;
consider z being
set such that A51:
p in z
and A52:
z in Z
by A18, A50, TARSKI:def 4;
z in B1 \/ B2
by A49, A52, XBOOLE_0:def 3;
then A53:
z in BB
by XBOOLE_0:def 3;
z c= a
by A50, A52, ZFMISC_1:74;
hence
ex
a being
Subset of
T st
(
a in BB &
p in a &
a c= A )
by A19, A51, A53, XBOOLE_1:1;
verum end; suppose A54:
(
Y1 <> {} &
Y2 <> {} &
Y <> {} )
;
ex a being Subset of T st
( a in BB & p in a & a c= A )then A55:
a =
meet Y
by A22, SETFAM_1:def 9
.=
(meet Y1) /\ (meet Y2)
by A23, A54, SETFAM_1:9
.=
(meet Y1) /\ (Intersect Y2)
by A54, SETFAM_1:def 9
.=
(Intersect Y1) /\ (Intersect Y2)
by A54, SETFAM_1:def 9
;
A56:
Y1 c= the
topology of
T1
by XBOOLE_1:17;
A57:
Y2 c= the
topology of
T2
by XBOOLE_1:17;
A58:
Intersect Y1 in FinMeetCl the
topology of
T1
by A21, A56, CANTOR_1:def 3;
A59:
Intersect Y2 in FinMeetCl the
topology of
T2
by A21, A57, CANTOR_1:def 3;
A60:
Intersect Y1 in the
topology of
T1
by A58, CANTOR_1:5;
A61:
the
topology of
T1 = UniCl B1
by Th22;
A62:
Intersect Y2 in the
topology of
T2
by A59, CANTOR_1:5;
A63:
the
topology of
T2 = UniCl B2
by Th22;
consider Z1 being
Subset-Family of
T1 such that A64:
Z1 c= B1
and A65:
Intersect Y1 = union Z1
by A60, A61, CANTOR_1:def 1;
p in Intersect Y1
by A18, A55, XBOOLE_0:def 4;
then consider z1 being
set such that A66:
p in z1
and A67:
z1 in Z1
by A65, TARSKI:def 4;
consider Z2 being
Subset-Family of
T2 such that A68:
Z2 c= B2
and A69:
Intersect Y2 = union Z2
by A62, A63, CANTOR_1:def 1;
p in Intersect Y2
by A18, A55, XBOOLE_0:def 4;
then consider z2 being
set such that A70:
p in z2
and A71:
z2 in Z2
by A69, TARSKI:def 4;
A72:
z1 /\ z2 in INTERSECTION (
B1,
B2)
by A64, A67, A68, A71, SETFAM_1:def 5;
A73:
z1 c= union Z1
by A67, ZFMISC_1:74;
A74:
z2 c= union Z2
by A71, ZFMISC_1:74;
A75:
z1 /\ z2 in BB
by A72, XBOOLE_0:def 3;
A76:
z1 /\ z2 c= a
by A55, A65, A69, A73, A74, XBOOLE_1:27;
p in z1 /\ z2
by A66, A70, XBOOLE_0:def 4;
hence
ex
a being
Subset of
T st
(
a in BB &
p in a &
a c= A )
by A19, A75, A76, XBOOLE_1:1;
verum end;
end; end;
hence
(B1 \/ B2) \/ (INTERSECTION (B1,B2)) is Basis of T
by A14, A15, Th32, XBOOLE_1:1; verum