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 A3: A <> {} ; :: thesis: B is compact

reconsider X = [.(lower_bound A),(upper_bound A).] as Subset of R^1 by TOPMETR:17;
A4: A is bounded by A2, RCOMP_1:10;
then A5: Closed-Interval-TSpace ((lower_bound A),(upper_bound A)) = R^1 | X by A3, SEQ_4:11, TOPMETR:19;
A6: B is closed by A1, A2, Th79;
A7: ( X = {} or X <> {} ) ;
Closed-Interval-TSpace ((lower_bound A),(upper_bound A)) is compact by A3, A4, HEINE:4, SEQ_4:11;
then X is compact by A7, A5, COMPTS_1:3;
hence B is compact by A1, A6, A4, Th24, 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