for GX being TopStruct
for T being Subset of GX holds Fr T = ((Cl (T `)) /\ T) \/ ((Cl T) \ T)