for F, G being with_non-empty_elements with_proper_subsets Subset-Family of R^1 st F is open & G is closed holds
F misses G