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

assume A2: A is compact ; :: thesis:

suppose A = {} ; :: thesis:

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

end;

suppose A <> {} ; :: thesis:

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:

end;

end;

end;

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