let r, s be real number ; :: thesis: for X being Subset of (Closed-Interval-TSpace r,s)
for Y being Subset of REAL st X = Y holds
( X is connected iff Y is connected )
let X be Subset of (Closed-Interval-TSpace r,s); :: 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 )
reconsider Z = X as Subset of R^1 by A1, TOPMETR:24;

hereby :: thesis: ( Y is connected implies X is connected )

assume X is connected ; :: thesis: Y is connected
then Z is connected by CONNSP_1:24;
hence Y is connected by A1, Th52; :: thesis: verum

end;

assume Y is connected ; :: thesis: X is connected
then Z is connected by A1, Th52;
hence X is connected by CONNSP_1:24; :: thesis: verum