theorem :: BORSUK_5:72

for A being Subset of R^1 st REAL = A ` holds
A = {}