let X be Subset of R^1; ( X is interval implies X is connected )
assume A1:
X is interval
; X is connected
A2:
X is Subset of REAL
by MEMBERED:3;
per cases
( 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.[ ) )
by A1, A2, Th29;
end;