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 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;
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 st X = left_closed_halfline a ; :: thesis: X is connected
then consider a being Real such that
A3: X = left_closed_halfline a ;
reconsider A = X as non empty interval Subset of R^1 by A3;
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 st X = left_open_halfline a ; :: thesis: X is connected
then consider a being Real such that
A4: X = left_open_halfline a ;
reconsider A = X as non empty interval Subset of R^1 by A4;
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 st X = right_closed_halfline a ; :: thesis: X is connected
then consider a being Real such that
A5: X = right_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 st X = right_open_halfline a ; :: thesis: X is connected
then consider a being Real such that
A6: X = right_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, b being Real 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 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 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 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;