theorem :: TOPS_1:29

for GX being TopStruct
for T being Subset of GX holds Fr T = Fr (T `) ;