##
restart: with(geometry):
## Given 3 distinct points, T, U, V on a line that does not pass through the
## origin, O.  WLG let point U be between T and V.
assume((x__||(1..4), y__||(1..4)) >~ 0);
##
point(Op,[0,0]);
point(T,[x__1,y__1]);
point(U,[x__2,y__2]);
point(V,[x__3,y__3]);

## Construct lines OT, OU, and OV.
line(OT, [Op,T]);
line(OU, [Op,U]);
line(OV, [Op,V]);

## Let point B be any distinct point on line OU s.t. it is distinct from the
## origin.  WLG let point B be on the point U side of the origin.
point(B,[2*y__2,solve(subs(x=2*y__2,Equation(OU)),y)]);
IsOnLine(B,OU);

## Construct a line, AD through point B perpendicular to line OT,
## intersecting lines OT, OU, and OV at points A, B, and pD,
## respectively.
PerpendicularLine(AD,B,OT);
ArePerpendicular(AD,OT);
intersection(A,AD,OT);

## Let sTU be the distance from point T to point U, etc.  Consider
## length of line segments sTU, sUV, and sAB.  Mark point C on line AE
## s.t. point C is in the direction of point D from point B and the
## proportion sTU/sUV = sAB/sBC, where sBC is the distance from point
## B to C.
point(C,[x__4,y__4]);
sTU := distance(T,U):
sUV := distance(U,V):
sAB := distance(A,B):
PerpendicularLine(CE,C,AD);
## proportional distance calculation
sBC := sAB * sUV / sTU; ## distance(B,C)
## indets({distance(B,C) = sBC,subs({x=x__4,y=y__4},Equation(AD))});
sol := solve({ distance(B,C) = sBC,
               eval(Equation(AD),{x=x__4,y=y__4})},{x__4,y__4});
eval(Equation(AD),{x=x__4,y=y__4});
## redefine point C with the calculated coordinates
point(C,eval(coordinates(C),sol));
IsOnLine(C,AD);
IsOnLine(C,CE);
## Proportional line segments.  Construct two intersecting lines,
## intersecting at point M.  Mark point P on one line at distance sTU
## from M.  Mark point Q on line MP distance sUV from oint P
## s.t. point P is between points M and Q.  Mark point K on the other
## line at distance sAB.  Draw line PK.  Construct ine QL through
## point Q parallel to line PK, intersecting line MK at point L.
## Then, the distances sMP/sPQ = sMK/sKL.

## Construct a line CE perpendicular to line AD, intersecting line OV
## at point E.
PerpendicularLine(CE, C, AD);
sol := solve({Equation(CE),Equation(OV)},{x,y});
point(E,[eval(x,sol), eval(y,sol)]);
intersection(E, CE, OV);
## Draw line EF through points E and B, intersecting line OT at point
## F.
line(EF,[E,B]);

## Prove line EF is parallel to line TV.

## theta = angle TOU
## phi   = angle UOV

## by similar triangles, AOB and TOU, the respective angles are equal
## and the lines are parallel.

## by similar triangles, BOD and UOV, the respective angles are equal
## and the lines are parallel.

## QED