for S being Subset-Family of REAL st S = { s where s is Subset of REAL : s is left_open_interval } holds
( S is cap-closed & S is diff-finite-partition-closed & S is with_empty_element & S is with_countable_Cover )