proposition: Lemma non_paralleles_trans : forall A B C D E F : PO, A <> B :>PO -> C <> D :>PO -> E <> F :>PO -> paralleles (droite A B) (droite C D) -> ~ paralleles (droite A B) (droite E F) -> ~ paralleles (droite C D) (droite E F).
proof: Proof. intros; red in |- *; intros. apply H3. apply paralleles_trans with (4 := H2); auto. Qed.