let p be Point of (TOP-REAL 2); :: thesis: for C being Subset of (TOP-REAL 2) holds LSeg (North-Bound p,C),(South-Bound p,C) is vertical
let C be Subset of (TOP-REAL 2); :: thesis: LSeg (North-Bound p,C),(South-Bound p,C) is vertical
( (North-Bound p,C) `1 = p `1 & (South-Bound p,C) `1 = p `1 ) by EUCLID:56;
hence LSeg (North-Bound p,C),(South-Bound p,C) is vertical by SPPOL_1:37; :: thesis: verum