theorem :: SRINGS_3:28

{ I where I is Interval : verum } is semialgebra_of_sets of REAL