let P be Subset of (TOP-REAL 2); :: thesis: ( P is Bounded & P is closed implies P is compact )
assume A1: ( P is Bounded & P is closed ) ; :: thesis: P is compact
then reconsider C = P as bounded Subset of (Euclid 2) by JORDAN2C:def 1;
consider r being Real, e being Point of (Euclid 2) such that
0 < r and
A2: C c= Ball (e,r) by METRIC_6:def 3;
reconsider p = e as Point of (TOP-REAL 2) by TOPREAL3:8;
A3: ].((p `2) - r),((p `2) + r).[ c= [.((p `2) - r),((p `2) + r).] by XXREAL_1:25;
A4: Ball (e,r) c= product ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) by Th50;
].((p `1) - r),((p `1) + r).[ c= [.((p `1) - r),((p `1) + r).] by XXREAL_1:25;
then product ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) c= product ((1,2) --> ([.((p `1) - r),((p `1) + r).],[.((p `2) - r),((p `2) + r).])) by A3, Th29;
then A5: Ball (e,r) c= product ((1,2) --> ([.((p `1) - r),((p `1) + r).],[.((p `2) - r),((p `2) + r).])) by A4, XBOOLE_1:1;
product ((1,2) --> ([.((p `1) - r),((p `1) + r).],[.((p `2) - r),((p `2) + r).])) is compact Subset of (TOP-REAL 2) by Th87;
hence P is compact by A1, A2, A5, COMPTS_1:9, XBOOLE_1:1; :: thesis: verum