set c1 = the carrier of T1;
set c2 = the carrier of T2;
set t1 = the topology of T1;
set t2 = the topology of T2;
( bool the carrier of T1 c= bool (the carrier of T1 \/ the carrier of T2) & bool the carrier of T2 c= bool (the carrier of T1 \/ the carrier of T2) ) by XBOOLE_1:7, ZFMISC_1:79;
then ( the topology of T1 c= bool (the carrier of T1 \/ the carrier of T2) & the topology of T2 c= bool (the carrier of T1 \/ the carrier of T2) ) by XBOOLE_1:1;
then reconsider t = the topology of T1 \/ the topology of T2 as Subset-Family of (the carrier of T1 \/ the carrier of T2) by 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
A1: ( T is strict & 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 A1;
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 A1, Def5; :: thesis: verum