let r, s be Real; :: thesis: |[r,s]| in Vertical_Line r
|[r,s]| `1 = r by EUCLID:52;
hence |[r,s]| in Vertical_Line r by Th8; :: thesis: verum