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 ;
A3: the topology of T1 \/ the topology of T2 is prebasis of T by Def6;
A4: the topology of T1 c= the topology of T1 \/ the topology of T2 by XBOOLE_1:7;
A5: the topology of T2 c= the topology of T1 \/ the topology of T2 by XBOOLE_1:7;
A6: the topology of T1 \/ the topology of T2 c= the topology of T by A3, TOPS_2:64;
then A7: the topology of T1 c= the topology of T by A4, XBOOLE_1:1;
the topology of T2 c= the topology of T by A5, A6, XBOOLE_1:1;
hence ( T is TopExtension of T1 & T is TopExtension of T2 ) by A1, A2, A7, Def5; :: thesis: verum