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