let D be non empty Subset of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) ex q being Point of (TOP-REAL 2) st
( q `2 > N-bound D & p <> q )
let p be Point of (TOP-REAL 2); :: thesis: ex q being Point of (TOP-REAL 2) st
( q `2 > N-bound D & p <> q )
take q = |[((p `1) - 1),((N-bound D) + 1)]|; :: thesis: ( q `2 > N-bound D & p <> q )
(N-bound D) + 1 > (N-bound D) + 0 by XREAL_1:6;
hence q `2 > N-bound D by EUCLID:52; :: thesis: p <> q
(p `1) - 1 < (p `1) - 0 by XREAL_1:15;
hence p <> q by EUCLID:52; :: thesis: verum