for r, s being Real holds |[r,s]| in Vertical_Line r