let S be Subset-Family of REAL; ( S = { I where I is Subset of REAL : I is left_open_interval } implies ( S is with_empty_element & S is semi-diff-closed & S is cap-closed ) )
assume
S = { I where I is Subset of REAL : I is left_open_interval }
; ( S is with_empty_element & S is semi-diff-closed & S is cap-closed )
then
( S is cap-closed & S is diff-finite-partition-closed & S is with_empty_element & S is with_countable_Cover )
by SRINGS_2:10;
hence
( S is with_empty_element & S is semi-diff-closed & S is cap-closed )
by th10; verum