proposition: Lemma l11_31_1 : forall A B C D E F, Out B A C -> D <> E -> F <> E -> LeA A B C D E F.
proof: Proof. intros. unfold LeA. exists D. split. apply inangle1123; assumption. apply l11_21_b. assumption. apply out_trivial. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2