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