let T1, T2 be TopStruct ; :: thesis: for T being Refinement of T1,T2 holds T is Refinement of T2,T1
let T be Refinement of T1,T2; :: thesis: T is Refinement of T2,T1
A1: 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 T is Refinement of T2,T1 by A1, Def6; :: thesis: verum