let p be Point of ; :: thesis: for C being Subset of holds LSeg (North-Bound p,C),(South-Bound p,C) is vertical
let C be Subset of ; :: 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