let r, s be Real; :: 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 interval )
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 interval )
let Y be Subset of REAL; :: thesis: ( X = Y implies ( X is connected iff Y is interval ) )
assume A1: X = Y ; :: thesis: ( X is connected iff Y is interval )
reconsider Z = X as Subset of R^1 by A1, TOPMETR:17;
hereby :: thesis: ( Y is interval implies X is connected )
assume X is connected ; :: thesis: Y is interval
then Z is connected by CONNSP_1:23;
hence Y is interval by A1; :: thesis: verum
end;
assume Y is interval ; :: thesis: X is connected
then Z is connected by A1;
hence X is connected by CONNSP_1:23; :: thesis: verum