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 ; :: thesis: p <> q
thus p <> q ; :: thesis: verum