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 )
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;
now :: thesis: ( ( x is_between p,r or x = p or x = r ) implies x in close_dist_Segment (p,r) )
assume ( 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;
hence ( x in close_dist_Segment (p,r) iff ( x is_between p,r or x = p or x = r ) ) by A1; :: thesis: verum