let C be compact Subset of (TOP-REAL 2); :: thesis: ( BDD C <> {} implies S-bound C <= S-bound (BDD C) )
set WC = S-bound C;
set WB = S-bound (BDD C);
set hal = ((S-bound (BDD C)) + (S-bound C)) / 2;
assume that
A1: BDD C <> {} and
A2: S-bound C > S-bound (BDD C) ; :: thesis: contradiction
A3: ((S-bound (BDD C)) + (S-bound C)) / 2 < S-bound C by A2, XREAL_1:226;

now :: thesis: contradiction

per cases ( for q1 being Point of (TOP-REAL 2) st q1 in BDD C holds
q1 `2 >= ((S-bound (BDD C)) + (S-bound C)) / 2 or ex q1 being Point of (TOP-REAL 2) st
( q1 in BDD C & q1 `2 < ((S-bound (BDD C)) + (S-bound C)) / 2 ) ) ;

suppose for q1 being Point of (TOP-REAL 2) st q1 in BDD C holds
q1 `2 >= ((S-bound (BDD C)) + (S-bound C)) / 2 ; :: thesis: contradiction

hence contradiction by A1, A2, Lm12, XREAL_1:226; :: thesis: verum

end;

suppose ex q1 being Point of (TOP-REAL 2) st
( q1 in BDD C & q1 `2 < ((S-bound (BDD C)) + (S-bound C)) / 2 ) ; :: thesis: contradiction

then consider q1 being Point of (TOP-REAL 2) such that
A4: q1 in BDD C and
A5: q1 `2 < ((S-bound (BDD C)) + (S-bound C)) / 2 ;
set Q = |[(q1 `1),(((S-bound C) + (q1 `2)) / 2)]|;
set WH = south_halfline |[(q1 `1),(((S-bound C) + (q1 `2)) / 2)]|;
A6: |[(q1 `1),(((S-bound C) + (q1 `2)) / 2)]| `2 = ((S-bound C) + (q1 `2)) / 2 by EUCLID:52;
A7: q1 `2 < S-bound C by A3, A5, XXREAL_0:2;
south_halfline |[(q1 `1),(((S-bound C) + (q1 `2)) / 2)]| misses C

proof

A8: |[(q1 `1),(((S-bound C) + (q1 `2)) / 2)]| `2 < S-bound C by A7, A6, XREAL_1:226;
assume (south_halfline |[(q1 `1),(((S-bound C) + (q1 `2)) / 2)]|) /\ C <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then consider y being object such that
A9: y in (south_halfline |[(q1 `1),(((S-bound C) + (q1 `2)) / 2)]|) /\ C by XBOOLE_0:def 1;
A10: y in C by A9, XBOOLE_0:def 4;
A11: y in south_halfline |[(q1 `1),(((S-bound C) + (q1 `2)) / 2)]| by A9, XBOOLE_0:def 4;
reconsider y = y as Point of (TOP-REAL 2) by A9;
y `2 <= |[(q1 `1),(((S-bound C) + (q1 `2)) / 2)]| `2 by A11, TOPREAL1:def 12;
then y `2 < S-bound C by A8, XXREAL_0:2;
hence contradiction by A10, PSCOMP_1:24; :: thesis: verum

end;

then A12: south_halfline |[(q1 `1),(((S-bound C) + (q1 `2)) / 2)]| c= UBD C by JORDAN2C:128;
A13: q1 `1 = |[(q1 `1),(((S-bound C) + (q1 `2)) / 2)]| `1 by EUCLID:52;
q1 `2 < |[(q1 `1),(((S-bound C) + (q1 `2)) / 2)]| `2 by A7, A6, XREAL_1:226;
then q1 in south_halfline |[(q1 `1),(((S-bound C) + (q1 `2)) / 2)]| by A13, TOPREAL1:def 12;
then q1 in (BDD C) /\ (UBD C) by A4, A12, XBOOLE_0:def 4;
then BDD C meets UBD C ;
hence contradiction by JORDAN2C:24; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum