theorem :: YELLOW_9:56

for T1, T2 being TopStruct
for T being Refinement of T1,T2
for X being Subset-Family of T st X = the topology of T1 \/ the topology of T2 holds
the topology of T = UniCl (FinMeetCl X)