let I be Subset of REAL; :: thesis: ( I = {} implies I is right_open_interval )
assume A1: I = {} ; :: thesis: I is right_open_interval
0 in REAL by NUMBERS:19;
then [.0,0.[ is right_open_interval by NUMBERS:31;
hence I is right_open_interval by A1; :: thesis: verum