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 = [.(inf A),(sup A).] as Subset of R^1 by TOPMETR:24;
A is closed by A2;
then A4: B is closed by A1, Th79;
A5: A is bounded by A2, RCOMP_1:28;
then A6: Closed-Interval-TSpace (inf A),(sup A) is compact by A3, HEINE:11, SEQ_4:24;
A7: ( X = {} or X <> {} ) ;
Closed-Interval-TSpace (inf A),(sup A) = R^1 | X by A3, A5, SEQ_4:24, TOPMETR:26;
then X is compact by A6, A7, COMPTS_1:12;
hence B is compact by A1, A4, A5, Th24, COMPTS_1:18; :: thesis: verum

end;

end;

end;

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