proposition: Lemma sams_suma__out546 : forall A B C D E F, SumA A B C D E F A B C -> SAMS A B C D E F -> Out E D F.
proof: Proof. intros A B C D E F HSuma HIsi. apply sams_suma__out213 with A B C. apply suma_sym; trivial. apply sams_sym; trivial. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles