let M be non empty MetrSpace; for p, r, x being Element of M holds
( x in open_dist_Segment (p,r) iff x is_between p,r )
let p, r, x be Element of M; ( x in open_dist_Segment (p,r) iff x is_between p,r )
( x in open_dist_Segment (p,r) implies x is_between p,r )
hence
( x in open_dist_Segment (p,r) iff x is_between p,r )
; verum