for X being Subset of REAL holds
( ( not X is empty & X is closed_interval ) iff ex a, b being Real st
( a <= b & X = [.a,b.] ) ) by XXREAL_1:29, XXREAL_1:30;