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