let C be compact Subset of (TOP-REAL 2); ( 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
; contradiction
A3:
((N-bound C) + (N-bound (BDD C))) / 2 > N-bound C
by A2, XREAL_1:226;
now contradictionper 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
ex
q1 being
Point of
(TOP-REAL 2) st
(
q1 in BDD C &
q1 `2 > ((N-bound C) + (N-bound (BDD C))) / 2 )
;
contradictionthen consider q1 being
Point of
(TOP-REAL 2) such that A4:
q1 in BDD C
and A5:
q1 `2 > ((N-bound C) + (N-bound (BDD C))) / 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:52;
A7:
q1 `2 > N-bound C
by A3, A5, XXREAL_0:2;
north_halfline |[(q1 `1),(((N-bound C) + (q1 `2)) / 2)]| misses C
proof
A8:
|[(q1 `1),(((N-bound C) + (q1 `2)) / 2)]| `2 > N-bound C
by A7, A6, XREAL_1:226;
assume
(north_halfline |[(q1 `1),(((N-bound C) + (q1 `2)) / 2)]|) /\ C <> {}
;
XBOOLE_0:def 7 contradiction
then consider y being
object such that A9:
y in (north_halfline |[(q1 `1),(((N-bound C) + (q1 `2)) / 2)]|) /\ C
by XBOOLE_0:def 1;
A10:
y in C
by A9, XBOOLE_0:def 4;
A11:
y in north_halfline |[(q1 `1),(((N-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),(((N-bound C) + (q1 `2)) / 2)]| `2
by A11, TOPREAL1:def 10;
then
y `2 > N-bound C
by A8, XXREAL_0:2;
hence
contradiction
by A10, PSCOMP_1:24;
verum
end; then A12:
north_halfline |[(q1 `1),(((N-bound C) + (q1 `2)) / 2)]| c= UBD C
by JORDAN2C:129;
A13:
q1 `1 = |[(q1 `1),(((N-bound C) + (q1 `2)) / 2)]| `1
by EUCLID:52;
q1 `2 > |[(q1 `1),(((N-bound C) + (q1 `2)) / 2)]| `2
by A7, A6, XREAL_1:226;
then
q1 in north_halfline |[(q1 `1),(((N-bound C) + (q1 `2)) / 2)]|
by A13, TOPREAL1:def 10;
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;
verum end;
hence
contradiction
; verum