let A, B, C be Point of (TOP-REAL 2); :: thesis: for p, q, r being Element of (Euclid 2) st p,q,r are_mutually_distinct & p = A & q = B & r = C holds

( A in LSeg (B,C) iff p is_Between q,r )

let p, q, r be Element of (Euclid 2); :: thesis: ( p,q,r are_mutually_distinct & p = A & q = B & r = C implies ( A in LSeg (B,C) iff p is_Between q,r ) )

assume that

A1: p,q,r are_mutually_distinct and

A2: ( p = A & q = B & r = C ) ; :: thesis: ( A in LSeg (B,C) iff p is_Between q,r )

then p is_between q,r by A1, METRIC_1:def 22;

hence A in LSeg (B,C) by A1, A2, Th11; :: thesis: verum

( A in LSeg (B,C) iff p is_Between q,r )

let p, q, r be Element of (Euclid 2); :: thesis: ( p,q,r are_mutually_distinct & p = A & q = B & r = C implies ( A in LSeg (B,C) iff p is_Between q,r ) )

assume that

A1: p,q,r are_mutually_distinct and

A2: ( p = A & q = B & r = C ) ; :: thesis: ( A in LSeg (B,C) iff p is_Between q,r )

hereby :: thesis: ( p is_Between q,r implies A in LSeg (B,C) )

assume
p is_Between q,r
; :: thesis: A in LSeg (B,C)assume
A in LSeg (B,C)
; :: thesis: p is_Between q,r

then p is_between q,r by A1, A2, Th11;

hence p is_Between q,r by METRIC_1:def 22; :: thesis: verum

end;then p is_between q,r by A1, A2, Th11;

hence p is_Between q,r by METRIC_1:def 22; :: thesis: verum

then p is_between q,r by A1, METRIC_1:def 22;

hence A in LSeg (B,C) by A1, A2, Th11; :: thesis: verum