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 ; :: thesis: verum

assume S is empty ; :: thesis: S is open_interval

then S = ].0.,0..[ ;

hence S is open_interval ; :: thesis: verum