let T1, T2 be TopStruct ; :: thesis: ( the carrier of T1 = the carrier of T2 implies for T being Refinement of T1,T2 holds
( T is TopExtension of T1 & T is TopExtension of T2 ) )
assume A1: the carrier of T1 = the carrier of T2 ; :: thesis: for T being Refinement of T1,T2 holds
( T is TopExtension of T1 & T is TopExtension of T2 )
let T be Refinement of T1,T2; :: thesis: ( T is TopExtension of T1 & T is TopExtension of T2 )
A2: the carrier of T = the carrier of T1 \/ the carrier of T2 by Def6
.= the carrier of T1 by A1 ;
the topology of T1 \/ the topology of T2 is prebasis of T by Def6;
then ( the topology of T1 c= the topology of T1 \/ the topology of T2 & the topology of T2 c= the topology of T1 \/ the topology of T2 & the topology of T1 \/ the topology of T2 c= the topology of T ) by CANTOR_1:def 5, XBOOLE_1:7;
then ( the topology of T1 c= the topology of T & the topology of T2 c= the topology of T ) by XBOOLE_1:1;
hence ( T is TopExtension of T1 & T is TopExtension of T2 ) by A1, A2, Def5; :: thesis: verum