theorem Th5: :: JORDAN5A:5

for X being Subset of REAL holds
( X in Family_open_set RealSpace iff X is open ) by Lm3, Lm4;