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 )

( 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

hence
( x in open_dist_Segment (p,r) iff x is_between p,r )
; :: thesis: verum
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;then ex q being Element of M st

( x = q & q is_between p,r ) ;

hence x is_between p,r ; :: thesis: verum