let T1, T2 be TopStruct ; :: thesis: for T, T9 being Refinement of T1,T2 holds TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of T9, the topology of T9 #)
let T, T9 be Refinement of T1,T2; :: thesis: TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of T9, the topology of T9 #)
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 T9 = the carrier of T1 \/ the carrier of T2 by Def6;
the topology of T1 \/ the topology of T2 is prebasis of T9 by Def6;
hence TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of T9, the topology of T9 #) by A1, A2, A3, Th26; :: thesis: verum