let M be non empty MetrStruct ; :: thesis: for p, r, x being Element of M holds

( x in close_dist_Segment (p,r) iff ( x is_between p,r or x = p or x = r ) )

let p, r, x be Element of M; :: thesis: ( x in close_dist_Segment (p,r) iff ( x is_between p,r or x = p or x = r ) )

A1: ( not x in close_dist_Segment (p,r) or x is_between p,r or x = p or x = r )

( x in close_dist_Segment (p,r) iff ( x is_between p,r or x = p or x = r ) )

let p, r, x be Element of M; :: thesis: ( x in close_dist_Segment (p,r) iff ( x is_between p,r or x = p or x = r ) )

A1: ( not x in close_dist_Segment (p,r) or x is_between p,r or x = p or x = r )

proof

assume
x in close_dist_Segment (p,r)
; :: thesis: ( x is_between p,r or x = p or x = r )

then ( x in { q where q is Element of M : q is_between p,r } or x in {p,r} ) by XBOOLE_0:def 3;

then ( ex q being Element of M st

( x = q & q is_between p,r ) or x = p or x = r ) by TARSKI:def 2;

hence ( x is_between p,r or x = p or x = r ) ; :: thesis: verum

end;then ( x in { q where q is Element of M : q is_between p,r } or x in {p,r} ) by XBOOLE_0:def 3;

then ( ex q being Element of M st

( x = q & q is_between p,r ) or x = p or x = r ) by TARSKI:def 2;

hence ( x is_between p,r or x = p or x = r ) ; :: thesis: verum

now :: thesis: ( ( x is_between p,r or x = p or x = r ) implies x in close_dist_Segment (p,r) )

hence
( x in close_dist_Segment (p,r) iff ( x is_between p,r or x = p or x = r ) )
by A1; :: thesis: verumassume
( x is_between p,r or x = p or x = r )
; :: thesis: x in close_dist_Segment (p,r)

then ( x in { q where q is Element of M : q is_between p,r } or x in {p,r} ) by TARSKI:def 2;

hence x in close_dist_Segment (p,r) by XBOOLE_0:def 3; :: thesis: verum

end;then ( x in { q where q is Element of M : q is_between p,r } or x in {p,r} ) by TARSKI:def 2;

hence x in close_dist_Segment (p,r) by XBOOLE_0:def 3; :: thesis: verum