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:52;

hence LSeg ((North-Bound (p,C)),(South-Bound (p,C))) is vertical by SPPOL_1:16; :: thesis: verum

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:52;

hence LSeg ((North-Bound (p,C)),(South-Bound (p,C))) is vertical by SPPOL_1:16; :: thesis: verum