theorem :: YELLOW_9:55

for T1, T2 being TopStruct
for T being Refinement of T1,T2 holds T is Refinement of T2,T1