theorem :: SRINGS_2:9

for S being Subset-Family of REAL st S = { ].a,b.] where a, b is Real : a <= b } holds
( S is cap-closed & S is diff-finite-partition-closed & S is with_empty_element & S is with_countable_Cover ) by THS0, THS1, THS2, LemmA1;