let p1, p2, p3, p be Point of (TOP-REAL 2); :: thesis: ( p in LSeg (p1,p2) & p <> p2 implies ( |((p3 - p),(p2 - p1))| = 0 iff |((p3 - p),(p2 - p))| = 0 ) )
assume p in LSeg (p1,p2) ; :: thesis: ( not p <> p2 or ( |((p3 - p),(p2 - p1))| = 0 iff |((p3 - p),(p2 - p))| = 0 ) )
then p in LSeg (p2,p1) ;
then consider l being Real such that
A1: p = ((1 - l) * p2) + (l * p1) and
0 <= l and
l <= 1 ;
assume A2: p <> p2 ; :: thesis: ( |((p3 - p),(p2 - p1))| = 0 iff |((p3 - p),(p2 - p))| = 0 )
A3: p2 - p = (p2 - ((1 - l) * p2)) - (l * p1) by A1, RLVECT_1:27
.= (p2 - ((1 * p2) - (l * p2))) - (l * p1) by RLVECT_1:35
.= (p2 - (p2 - (l * p2))) - (l * p1) by RLVECT_1:def 8
.= ((p2 - p2) + (l * p2)) - (l * p1) by RLVECT_1:29
.= ((0. (TOP-REAL 2)) + (l * p2)) - (l * p1) by RLVECT_1:5
.= (l * p2) - (l * p1) by RLVECT_1:4
.= l * (p2 - p1) by RLVECT_1:34 ;

hereby :: thesis: ( |((p3 - p),(p2 - p))| = 0 implies |((p3 - p),(p2 - p1))| = 0 )

assume A4: |((p3 - p),(p2 - p1))| = 0 ; :: thesis: |((p3 - p),(p2 - p))| = 0
thus |((p3 - p),(p2 - p))| = l * |((p3 - p),(p2 - p1))| by A3, EUCLID_2:20
.= 0 by A4 ; :: thesis: verum

end;

assume |((p3 - p),(p2 - p))| = 0 ; :: thesis: |((p3 - p),(p2 - p1))| = 0
then A5: l * |((p3 - p),(p2 - p1))| = 0 by A3, EUCLID_2:20;

per cases ( l = 0 or |((p3 - p),(p2 - p1))| = 0 ) by A5;

suppose l = 0 ; :: thesis: |((p3 - p),(p2 - p1))| = 0

then p = (1 * p2) + (0. (TOP-REAL 2)) by A1, RLVECT_1:10
.= 1 * p2 by RLVECT_1:4
.= p2 by RLVECT_1:def 8 ;
hence |((p3 - p),(p2 - p1))| = 0 by A2; :: thesis: verum

end;

suppose |((p3 - p),(p2 - p1))| = 0 ; :: thesis: |((p3 - p),(p2 - p1))| = 0

hence |((p3 - p),(p2 - p1))| = 0 ; :: thesis: verum

end;

end;