let T1, T2 be non empty TopSpace; for T being Refinement of T1,T2
for B1 being prebasis of T1
for B2 being prebasis of T2 holds (B1 \/ B2) \/ { the carrier of T1, the carrier of T2} is prebasis of T
let T be Refinement of T1,T2; for B1 being prebasis of T1
for B2 being prebasis of T2 holds (B1 \/ B2) \/ { the carrier of T1, the carrier of T2} is prebasis of T
let B1 be prebasis of T1; for B2 being prebasis of T2 holds (B1 \/ B2) \/ { the carrier of T1, the carrier of T2} is prebasis of T
let B2 be prebasis of T2; (B1 \/ B2) \/ { the carrier of T1, the carrier of T2} is prebasis of T
reconsider B = the topology of T1 \/ the topology of T2 as prebasis of T by Def6;
set cT1 = the carrier of T1;
set cT2 = the carrier of T2;
reconsider C1 = B1 \/ { the carrier of T1} as prebasis of T1 by Th29;
reconsider C2 = B2 \/ { the carrier of T2} as prebasis of T2 by Th29;
A1:
B1 c= the topology of T1
by TOPS_2:64;
A2:
C1 c= the topology of T1
by TOPS_2:64;
A3:
B2 c= the topology of T2
by TOPS_2:64;
A4:
C2 c= the topology of T2
by TOPS_2:64;
A5:
the carrier of T1 in the topology of T1
by PRE_TOPC:def 1;
A6:
the carrier of T2 in the topology of T2
by PRE_TOPC:def 1;
A7:
B1 \/ B2 c= B
by A1, A3, XBOOLE_1:13;
A8:
B c= the topology of T
by TOPS_2:64;
A9:
the carrier of T1 in B
by A5, XBOOLE_0:def 3;
A10:
the carrier of T2 in B
by A6, XBOOLE_0:def 3;
A11:
B1 \/ B2 c= the topology of T
by A7, A8;
A12:
{ the carrier of T1, the carrier of T2} c= the topology of T
by A8, A9, A10, ZFMISC_1:32;
A13:
{ the carrier of T1, the carrier of T2} c= B
by A9, A10, ZFMISC_1:32;
(B1 \/ B2) \/ { the carrier of T1, the carrier of T2} c= the topology of T
by A11, A12, XBOOLE_1:8;
then reconsider BB = (B1 \/ B2) \/ { the carrier of T1, the carrier of T2} as Subset-Family of T by XBOOLE_1:1;
A14:
the topology of T1 c= B
by XBOOLE_1:7;
A15:
the topology of T2 c= B
by XBOOLE_1:7;
A16:
C1 c= B
by A2, A14;
C2 c= B
by A4, A15;
then reconsider D1 = C1, D2 = C2 as Subset-Family of T by A16, XBOOLE_1:1;
reconsider D1 = D1, D2 = D2 as Subset-Family of T ;
reconsider D1 = D1, D2 = D2 as Subset-Family of T ;
A17: UniCl (FinMeetCl BB) =
UniCl (FinMeetCl (FinMeetCl BB))
by CANTOR_1:11
.=
UniCl (FinMeetCl (UniCl (FinMeetCl BB)))
by Th21
;
A18:
FinMeetCl B is Basis of T
by Th23;
A19:
FinMeetCl C1 is Basis of T1
by Th23;
A20:
FinMeetCl C2 is Basis of T2
by Th23;
A21:
UniCl (FinMeetCl B) = the topology of T
by A18, Th22;
A22:
UniCl (FinMeetCl C1) = the topology of T1
by A19, Th22;
A23:
UniCl (FinMeetCl C2) = the topology of T2
by A20, Th22;
A24:
B1 c= B1 \/ B2
by XBOOLE_1:7;
A25:
B2 c= B1 \/ B2
by XBOOLE_1:7;
A26:
{ the carrier of T1} c= { the carrier of T1, the carrier of T2}
by ZFMISC_1:7;
A27:
{ the carrier of T2} c= { the carrier of T1, the carrier of T2}
by ZFMISC_1:7;
A28:
D1 c= BB
by A24, A26, XBOOLE_1:13;
A29:
D2 c= BB
by A25, A27, XBOOLE_1:13;
BB c= B
by A7, A13, XBOOLE_1:8;
then A30:
FinMeetCl BB c= FinMeetCl B
by CANTOR_1:14;
A31:
FinMeetCl D1 c= FinMeetCl BB
by A28, CANTOR_1:14;
A32:
FinMeetCl D2 c= FinMeetCl BB
by A29, CANTOR_1:14;
A33:
UniCl (FinMeetCl BB) c= the topology of T
by A21, A30, CANTOR_1:9;
A34:
the carrier of T1 in { the carrier of T1}
by TARSKI:def 1;
A35:
the carrier of T2 in { the carrier of T2}
by TARSKI:def 1;
A36:
the carrier of T1 in C1
by A34, XBOOLE_0:def 3;
A37:
the carrier of T2 in C2
by A35, XBOOLE_0:def 3;
A38:
FinMeetCl D1 = { the carrier of T} \/ (FinMeetCl C1)
by A36, Th20;
A39:
FinMeetCl D2 = { the carrier of T} \/ (FinMeetCl C2)
by A37, Th20;
A40:
FinMeetCl C1 c= FinMeetCl D1
by A38, XBOOLE_1:7;
A41:
FinMeetCl C2 c= FinMeetCl D2
by A39, XBOOLE_1:7;
A42:
FinMeetCl C1 c= FinMeetCl BB
by A31, A40;
A43:
FinMeetCl C2 c= FinMeetCl BB
by A32, A41;
A44:
the topology of T1 c= UniCl (FinMeetCl BB)
by A22, A42, Th19;
the topology of T2 c= UniCl (FinMeetCl BB)
by A23, A43, Th19;
then
B c= UniCl (FinMeetCl BB)
by A44, XBOOLE_1:8;
then
FinMeetCl B c= FinMeetCl (UniCl (FinMeetCl BB))
by CANTOR_1:14;
then
the topology of T c= UniCl (FinMeetCl BB)
by A17, A21, CANTOR_1:9;
then
the topology of T = UniCl (FinMeetCl BB)
by A33;
then
FinMeetCl BB is Basis of T
by Th22;
hence
(B1 \/ B2) \/ { the carrier of T1, the carrier of T2} is prebasis of T
by Th23; verum