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 2;
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 10;
reconsider p = e as Point of (TOP-REAL 2) by TOPREAL3:13;
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:18, XBOOLE_1:1; :: thesis: verum