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 )
hereby :: thesis: ( p is_Between q,r implies 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;
assume p is_Between q,r ; :: thesis: A in LSeg (B,C)
then p is_between q,r by A1, METRIC_1:def 22;
hence A in LSeg (B,C) by A1, A2, Th11; :: thesis: verum