let S be Subset of REAL ; :: thesis: ( S is empty implies S is open_interval )
assume S is empty ; :: thesis: S is open_interval
then S = ].0. ,0. .[ ;
hence S is open_interval by Def5; :: thesis: verum