for TS being TopSpace
for GX being TopStruct
for P being Subset of TS
for R being Subset of GX holds
( ( R is open implies Int R = R ) & ( Int P = P implies P is open ) )