let T1, T2 be non empty TopSpace; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: (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; :: thesis: verum