fact: Definition line_completeness := forall (Tm: Tarski_neutral_dimensionless) (Tm2 : Tarski_neutral_dimensionless_with_decidable_point_equality Tm) P Q (f : @Tpoint Tn -> @Tpoint Tm), @archimedes_axiom Tm -> line_extension f P Q -> forall A, Col (f P) (f Q) A -> exists B, Col P Q B /\ f B = A.
imports: GeoCoq.Tarski_dev.Definitions