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 `1 > E-bound D & p <> q )
let p be Point of (TOP-REAL 2); :: thesis: ex q being Point of (TOP-REAL 2) st
( q `1 > E-bound D & p <> q )
take q = |[((E-bound D) + 1),((p `2) - 1)]|; :: thesis: ( q `1 > E-bound D & p <> q )
(E-bound D) + 1 > (E-bound D) + 0 by XREAL_1:6;
hence q `1 > E-bound D ; :: thesis: p <> q
thus p <> q ; :: thesis: verum