let M be non empty MetrSpace; :: thesis: 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; :: thesis: ( 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 )

proof

assume x in open_dist_Segment p,r ; :: thesis: x is_between p,r
then ex q being Element of M st
( x = q & q is_between p,r ) ;
hence x is_between p,r ; :: thesis: verum

end;

hence ( x in open_dist_Segment p,r iff x is_between p,r ) ; :: thesis: verum