proposition: Lemma bet_out__suppa : forall A B C D E F, A <> B -> B <> C -> Bet A B C -> Out E D F -> SuppA A B C D E F.
proof: Proof. intros. split; auto. exists C. split; auto. apply l11_21_b; trivial. apply out_trivial; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2