proposition: Lemma trisuma__bet : forall A B C D E F, TriSumA A B C D E F -> Bet D E F.
proof: Proof. apply alternate_interior__triangle. unfold alternate_interior_angles_postulate. apply l12_21_a. Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Tarski_dev.Annexes.half_angles GeoCoq.Tarski_dev.Ch12_parallel_inter_dec