let X be Subset of R^1 ; :: thesis: for Y being Subset of REAL st X = Y holds
( X is connected iff Y is connected )
let Y be Subset of REAL ; :: thesis: ( X = Y implies ( X is connected iff Y is connected ) )
assume A1: X = Y ; :: thesis: ( X is connected iff Y is connected )
thus ( X is connected implies Y is connected ) :: thesis: ( Y is connected implies X is connected )

proof

assume A2: X is connected ; :: thesis: Y is connected
let a be real number ; :: according to JCT_MISC:def 1 :: thesis: for b₁ being set holds
( not a in Y or not b₁ in Y or [.a,b₁.] c= Y )
thus for b₁ being set holds
( not a in Y or not b₁ in Y or [.a,b₁.] c= Y ) by A1, A2, BORSUK_5:111; :: thesis: verum

end;

assume A3: Y is connected ; :: thesis: X is connected

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, A3, Th41;

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

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

end;

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

R^1 ([#] REAL ) = REAL by TOPREALB:def 3;
then reconsider A = X as non empty convex 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 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 ;
R^1 (left_closed_halfline a) = left_closed_halfline a by TOPREALB:def 3;
then reconsider A = X as non empty convex 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 ;
R^1 (left_open_halfline a) = left_open_halfline a by TOPREALB:def 3;
then reconsider A = X as non empty convex 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 ;
R^1 (right_closed_halfline a) = right_closed_halfline a by TOPREALB:def 3;
then reconsider A = X as non empty convex 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 ;
R^1 (right_open_halfline a) = right_open_halfline a by TOPREALB:def 3;
then reconsider A = X as non empty convex 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 convex Subset of R^1 by TOPALG_2:8, 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 convex Subset of R^1 by TOPALG_2:10, 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 convex Subset of R^1 by TOPALG_2:11, 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 convex Subset of R^1 by TOPALG_2:9, XXREAL_1:33;
R^1 | A is connected ;
hence R^1 | X is connected ; :: according to CONNSP_1:def 3 :: thesis: verum

end;

end;