let V be RealLinearSpace; :: thesis: for P, Q being Element of V holds P,Q,Q are_collinear
let P, Q be Element of V; :: thesis: P,Q,Q are_collinear
( P in Line (P,Q) & Q in Line (P,Q) ) by RLTOPSP1:72;
hence P,Q,Q are_collinear ; :: thesis: verum