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