theorem Th29: :: RCOMP_3:29

for X being interval Subset of REAL holds
( X is empty or X = REAL or ex a being Real st X = left_closed_halfline a or ex a being Real st X = left_open_halfline a or ex a being Real st X = right_closed_halfline a or ex a being Real st X = right_open_halfline a or ex a, b being Real st
( a <= b & X = [.a,b.] ) or ex a, b being Real st
( a < b & X = [.a,b.[ ) or ex a, b being Real st
( a < b & X = ].a,b.] ) or ex a, b being Real st
( a < b & X = ].a,b.[ ) )