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 & C1 c= the topology of T1 & B2 c= the topology of T2 & C2 c= the topology of T2 & the carrier of T1 in the topology of T1 & the carrier of T2 in the topology of T2 ) by CANTOR_1:def 5, PRE_TOPC:def 1;
then A2: ( B1 \/ B2 c= B & B c= the topology of T & the carrier of T1 in B & the carrier of T2 in B ) by CANTOR_1:def 5, XBOOLE_0:def 3, XBOOLE_1:13;
then A3: ( B1 \/ B2 c= the topology of T & {the carrier of T1,the carrier of T2} c= the topology of T & {the carrier of T1,the carrier of T2} c= B ) by XBOOLE_1:1, ZFMISC_1:38;
then (B1 \/ B2) \/ {the carrier of T1,the carrier of T2} c= the topology of T by 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;
( the topology of T1 c= B & the topology of T2 c= B ) by XBOOLE_1:7;
then ( C1 c= B & C2 c= B ) by A1, XBOOLE_1:1;
then reconsider D1 = C1, D2 = C2 as Subset-Family of T by XBOOLE_1:1;
reconsider D1 = D1, D2 = D2 as Subset-Family of T ;
reconsider D1 = D1, D2 = D2 as Subset-Family of T ;
A4: UniCl (FinMeetCl BB) = UniCl (FinMeetCl (FinMeetCl BB)) by CANTOR_1:13
.= UniCl (FinMeetCl (UniCl (FinMeetCl BB))) by Th21 ;
( FinMeetCl B is Basis of T & FinMeetCl C1 is Basis of T1 & FinMeetCl C2 is Basis of T2 ) by Th23;
then A5: ( UniCl (FinMeetCl B) = the topology of T & UniCl (FinMeetCl C1) = the topology of T1 & UniCl (FinMeetCl C2) = the topology of T2 ) by Th22;
( B1 c= B1 \/ B2 & B2 c= B1 \/ B2 & {the carrier of T1} c= {the carrier of T1,the carrier of T2} & {the carrier of T2} c= {the carrier of T1,the carrier of T2} ) by XBOOLE_1:7, ZFMISC_1:12;
then ( D1 c= BB & D2 c= BB & BB c= B ) by A2, A3, XBOOLE_1:8, XBOOLE_1:13;
then A6: ( FinMeetCl BB c= FinMeetCl B & FinMeetCl D1 c= FinMeetCl BB & FinMeetCl D2 c= FinMeetCl BB ) by CANTOR_1:16;
then A7: ( UniCl (FinMeetCl BB) c= the topology of T & UniCl (FinMeetCl D1) c= UniCl (FinMeetCl BB) & UniCl (FinMeetCl D2) c= UniCl (FinMeetCl BB) ) by A5, CANTOR_1:9;
( the carrier of T1 in {the carrier of T1} & the carrier of T2 in {the carrier of T2} ) by TARSKI:def 1;
then ( the carrier of T1 in C1 & the carrier of T2 in C2 ) by XBOOLE_0:def 3;
then ( FinMeetCl D1 = {the carrier of T} \/ (FinMeetCl C1) & FinMeetCl D2 = {the carrier of T} \/ (FinMeetCl C2) ) by Th20;
then ( FinMeetCl C1 c= FinMeetCl D1 & FinMeetCl C2 c= FinMeetCl D2 ) by XBOOLE_1:7;
then ( FinMeetCl C1 c= FinMeetCl BB & FinMeetCl C2 c= FinMeetCl BB ) by A6, XBOOLE_1:1;
then ( the topology of T1 c= UniCl (FinMeetCl BB) & the topology of T2 c= UniCl (FinMeetCl BB) ) by A5, Th19;
then B c= UniCl (FinMeetCl BB) by XBOOLE_1:8;
then FinMeetCl B c= FinMeetCl (UniCl (FinMeetCl BB)) by CANTOR_1:16;
then the topology of T c= UniCl (FinMeetCl BB) by A4, A5, CANTOR_1:9;
then the topology of T = UniCl (FinMeetCl BB) by A7, XBOOLE_0:def 10;
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