let X be Subset of R^1 ; :: thesis: ( X is interval implies X is connected )
assume A1: X is interval ; :: thesis: 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 number st X = left_closed_halfline a or ex a being real number st X = left_open_halfline a or ex a being real number st X = right_closed_halfline a or ex a being real number st X = right_open_halfline a or ex a, b being real number st
( a <= b & X = [.a,b.] ) or ex a, b being real number st
( a < b & X = [.a,b.[ ) or ex a, b being real number st
( a < b & X = ].a,b.] ) or ex a, b being real number st
( a < b & X = ].a,b.[ ) ) by A1, A2, Th41;

suppose X is empty ; :: thesis: X is connected

then reconsider A = X as empty Subset of R^1 ;
A is interval ;
hence X is connected ; :: thesis: verum

end;

suppose X = REAL ; :: thesis: X is connected

then reconsider A = X as non empty interval Subset of R^1 ;
R^1 | A is connected ;
hence R^1 | X is connected ; :: according to CONNSP_1:def 3 :: thesis: verum

end;

suppose ex a being real number st X = left_closed_halfline a ; :: thesis: X is connected

then consider a being real number such that
A5: X = left_closed_halfline a ;
reconsider A = X as non empty interval Subset of R^1 by A5;
R^1 | A is connected ;
hence R^1 | X is connected ; :: according to CONNSP_1:def 3 :: thesis: verum

end;

suppose ex a being real number st X = left_open_halfline a ; :: thesis: X is connected

then consider a being real number such that
A6: X = left_open_halfline a ;
reconsider A = X as non empty interval Subset of R^1 by A6;
R^1 | A is connected ;
hence R^1 | X is connected ; :: according to CONNSP_1:def 3 :: thesis: verum

end;

suppose ex a being real number st X = right_closed_halfline a ; :: thesis: X is connected

then consider a being real number such that
A7: X = right_closed_halfline a ;
reconsider A = X as non empty interval Subset of R^1 by A7;
R^1 | A is connected ;
hence R^1 | X is connected ; :: according to CONNSP_1:def 3 :: thesis: verum

end;

suppose ex a being real number st X = right_open_halfline a ; :: thesis: X is connected

then consider a being real number such that
A8: X = right_open_halfline a ;
reconsider A = X as non empty interval Subset of R^1 by A8;
R^1 | A is connected ;
hence R^1 | X is connected ; :: according to CONNSP_1:def 3 :: thesis: verum

end;

suppose ex a, b being real number st
( a <= b & X = [.a,b.] ) ; :: thesis: X is connected

then reconsider A = X as non empty interval Subset of R^1 by XXREAL_1:1;
R^1 | A is connected ;
hence R^1 | X is connected ; :: according to CONNSP_1:def 3 :: thesis: verum

end;

suppose ex a, b being real number st
( a < b & X = [.a,b.[ ) ; :: thesis: X is connected

then reconsider A = X as non empty interval Subset of R^1 by XXREAL_1:3;
R^1 | A is connected ;
hence R^1 | X is connected ; :: according to CONNSP_1:def 3 :: thesis: verum

end;

suppose ex a, b being real number st
( a < b & X = ].a,b.] ) ; :: thesis: X is connected

then reconsider A = X as non empty interval Subset of R^1 by XXREAL_1:2;
R^1 | A is connected ;
hence R^1 | X is connected ; :: according to CONNSP_1:def 3 :: thesis: verum

end;

suppose ex a, b being real number st
( a < b & X = ].a,b.[ ) ; :: thesis: X is connected

then reconsider A = X as non empty interval Subset of R^1 by XXREAL_1:33;
R^1 | A is connected ;
hence R^1 | X is connected ; :: according to CONNSP_1:def 3 :: thesis: verum

end;

end;