let T1, T2 be TopStruct ; :: thesis: for T, T' being Refinement of T1,T2 holds TopStruct(# the carrier of T,the topology of T #) = TopStruct(# the carrier of T',the topology of T' #)
let T, T' be Refinement of T1,T2; :: thesis: TopStruct(# the carrier of T,the topology of T #) = TopStruct(# the carrier of T',the topology of T' #)
A1: the carrier of T = the carrier of T1 \/ the carrier of T2 by Def6;
A2: the topology of T1 \/ the topology of T2 is prebasis of T by Def6;
A3: the carrier of T' = the carrier of T1 \/ the carrier of T2 by Def6;
the topology of T1 \/ the topology of T2 is prebasis of T' by Def6;
hence TopStruct(# the carrier of T,the topology of T #) = TopStruct(# the carrier of T',the topology of T' #) by A1, A2, A3, Th26; :: thesis: verum