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

now

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

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

hence contradiction by A1, A2, Lm11, XREAL_1:228; :: thesis: verum

end;

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

then consider q1 being Point of (TOP-REAL 2) such that
A4: ( q1 in BDD C & q1 `2 > ((N-bound C) + (N-bound (BDD C))) / 2 ) ;
A5: q1 `2 > N-bound C by A3, A4, XXREAL_0:2;
set Q = |[(q1 `1 ),(((N-bound C) + (q1 `2 )) / 2)]|;
set WH = north_halfline |[(q1 `1 ),(((N-bound C) + (q1 `2 )) / 2)]|;
A6: |[(q1 `1 ),(((N-bound C) + (q1 `2 )) / 2)]| `2 = ((N-bound C) + (q1 `2 )) / 2 by EUCLID:56;
then ( q1 `1 = |[(q1 `1 ),(((N-bound C) + (q1 `2 )) / 2)]| `1 & q1 `2 > |[(q1 `1 ),(((N-bound C) + (q1 `2 )) / 2)]| `2 ) by A5, EUCLID:56, XREAL_1:228;
then A7: q1 in north_halfline |[(q1 `1 ),(((N-bound C) + (q1 `2 )) / 2)]| by TOPREAL1:def 12;
north_halfline |[(q1 `1 ),(((N-bound C) + (q1 `2 )) / 2)]| misses C

proof

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

end;

then north_halfline |[(q1 `1 ),(((N-bound C) + (q1 `2 )) / 2)]| c= UBD C by JORDAN2C:137;
then q1 in (BDD C) /\ (UBD C) by A4, A7, XBOOLE_0:def 4;
then BDD C meets UBD C by XBOOLE_0:4;
hence contradiction by JORDAN2C:28; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum