set c1 = the carrier of T1;
set c2 = the carrier of T2;
set t1 = the topology of T1;
set t2 = the topology of T2;
A1: bool the carrier of T1 c= bool ( the carrier of T1 \/ the carrier of T2) by XBOOLE_1:7, ZFMISC_1:67;
A2: bool the carrier of T2 c= bool ( the carrier of T1 \/ the carrier of T2) by XBOOLE_1:7, ZFMISC_1:67;
A3: the topology of T1 c= bool ( the carrier of T1 \/ the carrier of T2) by A1;
the topology of T2 c= bool ( the carrier of T1 \/ the carrier of T2) by A2;
then reconsider t = the topology of T1 \/ the topology of T2 as Subset-Family of ( the carrier of T1 \/ the carrier of T2) by A3, XBOOLE_1:8;
reconsider t = t as Subset-Family of ( the carrier of T1 \/ the carrier of T2) ;
set S = TopStruct(# ( the carrier of T1 \/ the carrier of T2),t #);
consider T being TopExtension of TopStruct(# ( the carrier of T1 \/ the carrier of T2),t #) such that
A4: T is strict and
A5: t is prebasis of T by Th53;
reconsider T = T as strict TopExtension of TopStruct(# ( the carrier of T1 \/ the carrier of T2),t #) by A4;
take T ; :: thesis: ( the carrier of T = the carrier of T1 \/ the carrier of T2 & the topology of T1 \/ the topology of T2 is prebasis of T )
thus ( the carrier of T = the carrier of T1 \/ the carrier of T2 & the topology of T1 \/ the topology of T2 is prebasis of T ) by A5, Def5; :: thesis: verum