theorem :: SRINGS_3:27

for S being Subset-Family of REAL st S = { I where I is Subset of REAL : I is right_open_interval } holds
( S is with_empty_element & S is semi-diff-closed & S is cap-closed )