let r, s be real number ; :: thesis: |[r,s]| in Vertical_Line r
|[r,s]| `1 = r by EUCLID:56;
hence |[r,s]| in Vertical_Line r by Th17; :: thesis: verum