let I be Subset of REAL; :: thesis: ( I is open_interval implies I is open )
assume A1: I is open_interval ; :: thesis: I is open

now :: thesis: ( not I is empty implies I is open )

assume not I is empty ; :: thesis: I is open
then I = ].(inf I),(sup I).[ by A1, MEASURE6:16;
hence I is open by FDIFF_12:2; :: thesis: verum

end;

hence I is open ; :: thesis: verum