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 set 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;
A4: x is open by A1, A2, TOPS_2:def 1;
x is closed by A1, A3, TOPS_2:def 2;
then ( x = {} or x = REAL ) by A4, BORSUK_5:57;
hence contradiction by A2, SETFAM_1:def 13, TOPMETR:24; :: thesis: verum