proposition: Lemma lta_out_lta : forall A B C D E F A' C' D' F', Out B A A' -> Out B C C' -> Out E D D' -> Out E F F' -> LtA A B C D E F -> LtA A' B C' D' E F'.
proof: Proof. intros. unfold LtA in *. spliter. split. apply(lea_out_lea A B C D E F A' C' D' F');auto. intro. apply H4. apply (l11_10 A' B C' D' E F'); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_order