proposition: Theorem position_relative_droites_espace : forall A B C D : PO, A <> B :>PO -> C <> D :>PO -> ~ coplanaires A B C D \/ concours (droite A B) (droite C D) \/ paralleles (droite A B) (droite C D).
proof: Proof. intros A B C D H10 H; try assumption. elim (classic (paralleles (droite A B) (droite C D))); intros. right; right; try assumption. elim droites_non_paralleles with (A := A) (B := B) (C := C) (D := D); auto with geo; intros. Qed.