theorem :: YELLOW_9:57

for T1, T2 being TopStruct st the carrier of T1 = the carrier of T2 holds
for T being Refinement of T1,T2 holds
( T is TopExtension of T1 & T is TopExtension of T2 )