let F, G be with_non-empty_elements with_proper_subsets Subset-Family of R^1; :: thesis: ( F is open & G is closed implies F misses G )
assume A1: ( F is open & G is closed ) ; :: thesis: F misses G
assume F meets G ; :: thesis: contradiction
then consider x being object such that
A2: x in F and
A3: x in G by XBOOLE_0:3;
reconsider x = x as Subset of R^1 by A2;
( x is open & x is closed ) by A1, A2, A3;
then ( x = {} or x = REAL ) by BORSUK_5:34;
hence contradiction by A2, SETFAM_1:def 12, TOPMETR:17; :: thesis: verum