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

proof

assume A2: A is compact ; :: thesis: B is compact

per cases ( A = {} or A <> {} ) ;

suppose A = {} ; :: thesis: B is compact

then reconsider C = B as empty Subset of R^1 by A1;
C is compact ;
hence B is compact ; :: thesis: verum

end;

suppose A <> {} ; :: thesis: B is compact

then reconsider A = A as non empty real-bounded Subset of REAL by A2, RCOMP_1:10;
reconsider i = inf A, s = sup A as Real ;
reconsider X = [.i,s.] as Subset of R^1 by TOPMETR:17;
A3: i <= s by XXREAL_2:40;
then A4: Closed-Interval-TSpace (i,s) = R^1 | X by TOPMETR:19;
A5: B is closed by A1, A2, Th23;
A6: X <> {} by A3, XXREAL_1:30;
A7: B c= X by A1, XXREAL_2:69;
Closed-Interval-TSpace (i,s) is compact by A3, HEINE:4;
then X is compact by A6, A4, COMPTS_1:3;
hence B is compact by A5, A7, COMPTS_1:9; :: thesis: verum

end;

end;

end;

assume B is compact ; :: thesis: A is compact
then [#] B is compact by WEIERSTR:13;
hence A is compact by A1, WEIERSTR:def 1; :: thesis: verum