%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : GEO196+3 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n032.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Sat Jul 16 06:30:57 EDT 2022 % Result : Theorem 5.04s 5.24s % Output : Proof 5.93s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.10 % Problem : GEO196+3 : TPTP v8.1.0. Released v4.0.0. % 0.00/0.10 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.10/0.29 % Computer : n032.cluster.edu % 0.10/0.29 % Model : x86_64 x86_64 % 0.10/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.29 % Memory : 8042.1875MB % 0.10/0.29 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.29 % CPULimit : 300 % 0.10/0.29 % WCLimit : 600 % 0.10/0.29 % DateTime : Sat Jun 18 10:02:47 EDT 2022 % 0.10/0.30 % CPUTime : % 5.04/5.24 % SZS status Theorem % 5.04/5.24 (* PROOF-FOUND *) % 5.04/5.24 (* BEGIN-PROOF *) % 5.04/5.24 % SZS output start Proof % 5.04/5.24 1. (apart_point_and_line (intersection_point T_0 T_1) T_2) (-. (apart_point_and_line (intersection_point T_0 T_1) T_2)) ### Axiom % 5.04/5.24 2. (distinct_lines T_2 T_1) (-. (distinct_lines T_2 T_1)) ### Axiom % 5.04/5.24 3. (convergent_lines T_2 T_3) (-. (convergent_lines T_2 T_3)) ### Axiom % 5.04/5.24 4. (apart_point_and_line (intersection_point T_2 T_3) T_2) (-. (apart_point_and_line (intersection_point T_2 T_3) T_2)) ### Axiom % 5.04/5.24 5. ((convergent_lines T_2 T_3) => (-. (apart_point_and_line (intersection_point T_2 T_3) T_2))) (apart_point_and_line (intersection_point T_2 T_3) T_2) (convergent_lines T_2 T_3) ### Imply 3 4 % 5.04/5.24 6. (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (convergent_lines T_2 T_3) (apart_point_and_line (intersection_point T_2 T_3) T_2) ### All 5 % 5.04/5.24 7. (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (apart_point_and_line (intersection_point T_2 T_3) T_1) ### Axiom % 5.04/5.24 8. (-. (convergent_lines T_2 T_1)) (convergent_lines T_2 T_1) ### Axiom % 5.04/5.24 9. ((distinct_lines T_2 T_1) => ((apart_point_and_line (intersection_point T_2 T_3) T_2) \/ ((apart_point_and_line (intersection_point T_2 T_3) T_1) \/ (convergent_lines T_2 T_1)))) (-. (convergent_lines T_2 T_1)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (distinct_lines T_2 T_1) ### DisjTree 2 6 7 8 % 5.04/5.24 10. (All Z, ((distinct_lines T_2 Z) => ((apart_point_and_line (intersection_point T_2 T_3) T_2) \/ ((apart_point_and_line (intersection_point T_2 T_3) Z) \/ (convergent_lines T_2 Z))))) (distinct_lines T_2 T_1) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (convergent_lines T_2 T_1)) ### All 9 % 5.04/5.24 11. (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (apart_point_and_line (intersection_point T_0 T_1) T_1) ### Axiom % 5.04/5.24 12. ((apart_point_and_line (intersection_point T_0 T_1) T_2) => ((distinct_lines T_2 T_1) \/ (apart_point_and_line (intersection_point T_0 T_1) T_1))) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (-. (convergent_lines T_2 T_1)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (All Z, ((distinct_lines T_2 Z) => ((apart_point_and_line (intersection_point T_2 T_3) T_2) \/ ((apart_point_and_line (intersection_point T_2 T_3) Z) \/ (convergent_lines T_2 Z))))) (apart_point_and_line (intersection_point T_0 T_1) T_2) ### DisjTree 1 10 11 % 5.04/5.24 13. (All Z, ((apart_point_and_line (intersection_point T_0 T_1) T_2) => ((distinct_lines T_2 Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z)))) (apart_point_and_line (intersection_point T_0 T_1) T_2) (All Z, ((distinct_lines T_2 Z) => ((apart_point_and_line (intersection_point T_2 T_3) T_2) \/ ((apart_point_and_line (intersection_point T_2 T_3) Z) \/ (convergent_lines T_2 Z))))) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (convergent_lines T_2 T_1)) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) ### All 12 % 5.04/5.24 14. (All Y, (All Z, ((apart_point_and_line (intersection_point T_0 T_1) Y) => ((distinct_lines Y Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z))))) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (-. (convergent_lines T_2 T_1)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (All Z, ((distinct_lines T_2 Z) => ((apart_point_and_line (intersection_point T_2 T_3) T_2) \/ ((apart_point_and_line (intersection_point T_2 T_3) Z) \/ (convergent_lines T_2 Z))))) (apart_point_and_line (intersection_point T_0 T_1) T_2) ### All 13 % 5.04/5.24 15. (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (apart_point_and_line (intersection_point T_0 T_1) T_2) (All Z, ((distinct_lines T_2 Z) => ((apart_point_and_line (intersection_point T_2 T_3) T_2) \/ ((apart_point_and_line (intersection_point T_2 T_3) Z) \/ (convergent_lines T_2 Z))))) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (convergent_lines T_2 T_1)) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) ### All 14 % 5.04/5.24 16. (convergent_lines T_0 T_1) (-. (convergent_lines T_0 T_1)) ### Axiom % 5.04/5.24 17. (distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_3)) (-. (distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_3))) ### Axiom % 5.04/5.24 18. (distinct_lines T_1 T_0) (-. (distinct_lines T_1 T_0)) ### Axiom % 5.04/5.24 19. (convergent_lines T_0 T_1) (-. (convergent_lines T_0 T_1)) ### Axiom % 5.04/5.24 20. (apart_point_and_line (intersection_point T_0 T_1) T_1) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) ### Axiom % 5.04/5.24 21. ((convergent_lines T_0 T_1) => (-. (apart_point_and_line (intersection_point T_0 T_1) T_1))) (apart_point_and_line (intersection_point T_0 T_1) T_1) (convergent_lines T_0 T_1) ### Imply 19 20 % 5.04/5.24 22. (All Y, ((convergent_lines T_0 Y) => (-. (apart_point_and_line (intersection_point T_0 Y) Y)))) (convergent_lines T_0 T_1) (apart_point_and_line (intersection_point T_0 T_1) T_1) ### All 21 % 5.04/5.24 23. (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (apart_point_and_line (intersection_point T_0 T_1) T_1) (convergent_lines T_0 T_1) ### All 22 % 5.04/5.24 24. (-. (apart_point_and_line (intersection_point T_0 T_1) T_0)) (apart_point_and_line (intersection_point T_0 T_1) T_0) ### Axiom % 5.04/5.24 25. (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (apart_point_and_line (intersection_point T_2 T_3) T_1) ### Axiom % 5.04/5.24 26. (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (apart_point_and_line (intersection_point T_2 T_3) T_0) ### Axiom % 5.04/5.24 27. (((distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_3)) /\ (distinct_lines T_1 T_0)) => ((apart_point_and_line (intersection_point T_0 T_1) T_1) \/ ((apart_point_and_line (intersection_point T_0 T_1) T_0) \/ ((apart_point_and_line (intersection_point T_2 T_3) T_1) \/ (apart_point_and_line (intersection_point T_2 T_3) T_0))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (apart_point_and_line (intersection_point T_0 T_1) T_0)) (convergent_lines T_0 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (distinct_lines T_1 T_0) (distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_3)) ### DisjTree 17 18 23 24 25 26 % 5.04/5.24 28. (All V, (((distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_3)) /\ (distinct_lines T_1 V)) => ((apart_point_and_line (intersection_point T_0 T_1) T_1) \/ ((apart_point_and_line (intersection_point T_0 T_1) V) \/ ((apart_point_and_line (intersection_point T_2 T_3) T_1) \/ (apart_point_and_line (intersection_point T_2 T_3) V)))))) (distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_3)) (distinct_lines T_1 T_0) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_0 T_1) (-. (apart_point_and_line (intersection_point T_0 T_1) T_0)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) ### All 27 % 5.04/5.24 29. (-. (distinct_lines T_0 T_0)) (distinct_lines T_0 T_0) ### Axiom % 5.04/5.24 30. (convergent_lines T_0 T_1) (-. (convergent_lines T_0 T_1)) ### Axiom % 5.04/5.24 31. (apart_point_and_line (intersection_point T_0 T_1) T_0) (-. (apart_point_and_line (intersection_point T_0 T_1) T_0)) ### Axiom % 5.13/5.34 32. ((convergent_lines T_0 T_1) => (-. (apart_point_and_line (intersection_point T_0 T_1) T_0))) (apart_point_and_line (intersection_point T_0 T_1) T_0) (convergent_lines T_0 T_1) ### Imply 30 31 % 5.13/5.34 33. (All Y, ((convergent_lines T_0 Y) => (-. (apart_point_and_line (intersection_point T_0 Y) T_0)))) (convergent_lines T_0 T_1) (apart_point_and_line (intersection_point T_0 T_1) T_0) ### All 32 % 5.13/5.34 34. ((apart_point_and_line (intersection_point T_0 T_1) T_0) => ((distinct_lines T_0 T_0) \/ (apart_point_and_line (intersection_point T_0 T_1) T_0))) (All Y, ((convergent_lines T_0 Y) => (-. (apart_point_and_line (intersection_point T_0 Y) T_0)))) (-. (distinct_lines T_0 T_0)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_0 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (distinct_lines T_1 T_0) (distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_3)) (All V, (((distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_3)) /\ (distinct_lines T_1 V)) => ((apart_point_and_line (intersection_point T_0 T_1) T_1) \/ ((apart_point_and_line (intersection_point T_0 T_1) V) \/ ((apart_point_and_line (intersection_point T_2 T_3) T_1) \/ (apart_point_and_line (intersection_point T_2 T_3) V)))))) ### DisjTree 28 29 33 % 5.13/5.34 35. (All Z, ((apart_point_and_line (intersection_point T_0 T_1) T_0) => ((distinct_lines T_0 Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z)))) (All V, (((distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_3)) /\ (distinct_lines T_1 V)) => ((apart_point_and_line (intersection_point T_0 T_1) T_1) \/ ((apart_point_and_line (intersection_point T_0 T_1) V) \/ ((apart_point_and_line (intersection_point T_2 T_3) T_1) \/ (apart_point_and_line (intersection_point T_2 T_3) V)))))) (distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_3)) (distinct_lines T_1 T_0) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_0 T_1) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (-. (distinct_lines T_0 T_0)) (All Y, ((convergent_lines T_0 Y) => (-. (apart_point_and_line (intersection_point T_0 Y) T_0)))) ### All 34 % 5.13/5.34 36. (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (-. (distinct_lines T_0 T_0)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_0 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (distinct_lines T_1 T_0) (distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_3)) (All V, (((distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_3)) /\ (distinct_lines T_1 V)) => ((apart_point_and_line (intersection_point T_0 T_1) T_1) \/ ((apart_point_and_line (intersection_point T_0 T_1) V) \/ ((apart_point_and_line (intersection_point T_2 T_3) T_1) \/ (apart_point_and_line (intersection_point T_2 T_3) V)))))) (All Z, ((apart_point_and_line (intersection_point T_0 T_1) T_0) => ((distinct_lines T_0 Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z)))) ### All 35 % 5.13/5.34 37. (All U, (All V, (((distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_3)) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_1) U) \/ ((apart_point_and_line (intersection_point T_0 T_1) V) \/ ((apart_point_and_line (intersection_point T_2 T_3) U) \/ (apart_point_and_line (intersection_point T_2 T_3) V))))))) (All Z, ((apart_point_and_line (intersection_point T_0 T_1) T_0) => ((distinct_lines T_0 Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z)))) (distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_3)) (distinct_lines T_1 T_0) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_0 T_1) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (-. (distinct_lines T_0 T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) ### All 36 % 5.13/5.34 38. (All Y, (All Z, ((apart_point_and_line (intersection_point T_0 T_1) Y) => ((distinct_lines Y Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z))))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (-. (distinct_lines T_0 T_0)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_0 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (distinct_lines T_1 T_0) (distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_3)) (All U, (All V, (((distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_3)) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_1) U) \/ ((apart_point_and_line (intersection_point T_0 T_1) V) \/ ((apart_point_and_line (intersection_point T_2 T_3) U) \/ (apart_point_and_line (intersection_point T_2 T_3) V))))))) ### All 37 % 5.13/5.34 39. (All X, (-. (distinct_lines X X))) (All U, (All V, (((distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_3)) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_1) U) \/ ((apart_point_and_line (intersection_point T_0 T_1) V) \/ ((apart_point_and_line (intersection_point T_2 T_3) U) \/ (apart_point_and_line (intersection_point T_2 T_3) V))))))) (distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_3)) (distinct_lines T_1 T_0) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_0 T_1) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All Y, (All Z, ((apart_point_and_line (intersection_point T_0 T_1) Y) => ((distinct_lines Y Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z))))) ### All 38 % 5.13/5.34 40. (-. (convergent_lines T_0 T_0)) (convergent_lines T_0 T_0) ### Axiom % 5.13/5.34 41. ((convergent_lines T_0 T_1) => ((distinct_lines T_1 T_0) \/ (convergent_lines T_0 T_0))) (-. (convergent_lines T_0 T_0)) (All Y, (All Z, ((apart_point_and_line (intersection_point T_0 T_1) Y) => ((distinct_lines Y Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z))))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_3)) (All U, (All V, (((distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_3)) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_1) U) \/ ((apart_point_and_line (intersection_point T_0 T_1) V) \/ ((apart_point_and_line (intersection_point T_2 T_3) U) \/ (apart_point_and_line (intersection_point T_2 T_3) V))))))) (All X, (-. (distinct_lines X X))) (convergent_lines T_0 T_1) ### DisjTree 16 39 40 % 5.13/5.34 42. (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (convergent_lines T_0 T_1) (All X, (-. (distinct_lines X X))) (All U, (All V, (((distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_3)) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_1) U) \/ ((apart_point_and_line (intersection_point T_0 T_1) V) \/ ((apart_point_and_line (intersection_point T_2 T_3) U) \/ (apart_point_and_line (intersection_point T_2 T_3) V))))))) (distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_3)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All Y, (All Z, ((apart_point_and_line (intersection_point T_0 T_1) Y) => ((distinct_lines Y Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z))))) (-. (convergent_lines T_0 T_0)) ### All 41 % 5.34/5.60 43. (All X, (-. (convergent_lines X X))) (All Y, (All Z, ((apart_point_and_line (intersection_point T_0 T_1) Y) => ((distinct_lines Y Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z))))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_3)) (All U, (All V, (((distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_3)) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_1) U) \/ ((apart_point_and_line (intersection_point T_0 T_1) V) \/ ((apart_point_and_line (intersection_point T_2 T_3) U) \/ (apart_point_and_line (intersection_point T_2 T_3) V))))))) (All X, (-. (distinct_lines X X))) (convergent_lines T_0 T_1) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) ### All 42 % 5.34/5.60 44. (All Y, (All U, (All V, (((distinct_points (intersection_point T_0 T_1) Y) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_1) U) \/ ((apart_point_and_line (intersection_point T_0 T_1) V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V)))))))) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (convergent_lines T_0 T_1) (All X, (-. (distinct_lines X X))) (distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_3)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All Y, (All Z, ((apart_point_and_line (intersection_point T_0 T_1) Y) => ((distinct_lines Y Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z))))) (All X, (-. (convergent_lines X X))) ### All 43 % 5.34/5.60 45. (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (-. (convergent_lines X X))) (All Y, (All Z, ((apart_point_and_line (intersection_point T_0 T_1) Y) => ((distinct_lines Y Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z))))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_3)) (All X, (-. (distinct_lines X X))) (convergent_lines T_0 T_1) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) ### All 44 % 5.34/5.60 46. (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (convergent_lines T_0 T_1) (All X, (-. (distinct_lines X X))) (distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_3)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (convergent_lines X X))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) ### All 45 % 5.34/5.60 47. (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (apart_point_and_line (intersection_point T_2 T_3) T_1) ### Axiom % 5.34/5.60 48. ((apart_point_and_line (intersection_point T_0 T_1) T_1) => ((distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_3)) \/ (apart_point_and_line (intersection_point T_2 T_3) T_1))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (-. (convergent_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (All X, (-. (distinct_lines X X))) (convergent_lines T_0 T_1) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (-. (convergent_lines T_2 T_1)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (All Z, ((distinct_lines T_2 Z) => ((apart_point_and_line (intersection_point T_2 T_3) T_2) \/ ((apart_point_and_line (intersection_point T_2 T_3) Z) \/ (convergent_lines T_2 Z))))) (apart_point_and_line (intersection_point T_0 T_1) T_2) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) ### DisjTree 15 46 47 % 5.34/5.60 49. (All Z, ((apart_point_and_line (intersection_point T_0 T_1) T_1) => ((distinct_points (intersection_point T_0 T_1) Z) \/ (apart_point_and_line Z T_1)))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (apart_point_and_line (intersection_point T_0 T_1) T_2) (All Z, ((distinct_lines T_2 Z) => ((apart_point_and_line (intersection_point T_2 T_3) T_2) \/ ((apart_point_and_line (intersection_point T_2 T_3) Z) \/ (convergent_lines T_2 Z))))) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (convergent_lines T_2 T_1)) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (convergent_lines T_0 T_1) (All X, (-. (distinct_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (convergent_lines X X))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) ### All 48 % 5.34/5.60 50. (All Y, (All Z, ((distinct_lines Y Z) => ((apart_point_and_line (intersection_point T_2 T_3) Y) \/ ((apart_point_and_line (intersection_point T_2 T_3) Z) \/ (convergent_lines Y Z)))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (-. (convergent_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (All X, (-. (distinct_lines X X))) (convergent_lines T_0 T_1) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (-. (convergent_lines T_2 T_1)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (apart_point_and_line (intersection_point T_0 T_1) T_2) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All Z, ((apart_point_and_line (intersection_point T_0 T_1) T_1) => ((distinct_points (intersection_point T_0 T_1) Z) \/ (apart_point_and_line Z T_1)))) ### All 49 % 5.45/5.63 51. (All X, (All Y, (All Z, ((distinct_lines Y Z) => ((apart_point_and_line X Y) \/ ((apart_point_and_line X Z) \/ (convergent_lines Y Z))))))) (All Z, ((apart_point_and_line (intersection_point T_0 T_1) T_1) => ((distinct_points (intersection_point T_0 T_1) Z) \/ (apart_point_and_line Z T_1)))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (apart_point_and_line (intersection_point T_0 T_1) T_2) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (convergent_lines T_2 T_1)) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (convergent_lines T_0 T_1) (All X, (-. (distinct_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (convergent_lines X X))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) ### All 50 % 5.45/5.63 52. (All Y, (All Z, ((apart_point_and_line (intersection_point T_0 T_1) Y) => ((distinct_points (intersection_point T_0 T_1) Z) \/ (apart_point_and_line Z Y))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (-. (convergent_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (All X, (-. (distinct_lines X X))) (convergent_lines T_0 T_1) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (-. (convergent_lines T_2 T_1)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (apart_point_and_line (intersection_point T_0 T_1) T_2) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((distinct_lines Y Z) => ((apart_point_and_line X Y) \/ ((apart_point_and_line X Z) \/ (convergent_lines Y Z))))))) ### All 51 % 5.45/5.63 53. (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((distinct_lines Y Z) => ((apart_point_and_line X Y) \/ ((apart_point_and_line X Z) \/ (convergent_lines Y Z))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (apart_point_and_line (intersection_point T_0 T_1) T_2) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (convergent_lines T_2 T_1)) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (convergent_lines T_0 T_1) (All X, (-. (distinct_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (convergent_lines X X))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) ### All 52 % 5.45/5.63 54. (All Y, (All Z, ((convergent_lines T_0 Y) => ((distinct_lines Y Z) \/ (convergent_lines T_0 Z))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (-. (convergent_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (All X, (-. (distinct_lines X X))) (convergent_lines T_0 T_1) (-. (convergent_lines T_2 T_1)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (apart_point_and_line (intersection_point T_0 T_1) T_2) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((distinct_lines Y Z) => ((apart_point_and_line X Y) \/ ((apart_point_and_line X Z) \/ (convergent_lines Y Z))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) ### All 53 % 5.45/5.63 55. (All X, (All Y, (All Z, ((convergent_lines X Y) => ((distinct_lines Y Z) \/ (convergent_lines X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((distinct_lines Y Z) => ((apart_point_and_line X Y) \/ ((apart_point_and_line X Z) \/ (convergent_lines Y Z))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (apart_point_and_line (intersection_point T_0 T_1) T_2) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (convergent_lines T_2 T_1)) (convergent_lines T_0 T_1) (All X, (-. (distinct_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (convergent_lines X X))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) ### All 54 % 5.45/5.63 56. (apart_point_and_line (intersection_point T_0 T_1) T_2) (-. (apart_point_and_line (intersection_point T_0 T_1) T_2)) ### Axiom % 5.45/5.63 57. (apart_point_and_line (intersection_point T_0 T_1) T_2) (-. (apart_point_and_line (intersection_point T_0 T_1) T_2)) ### Axiom % 5.45/5.63 58. (convergent_lines T_0 T_1) (-. (convergent_lines T_0 T_1)) ### Axiom % 5.45/5.63 59. (distinct_lines T_1 T_0) (-. (distinct_lines T_1 T_0)) ### Axiom % 5.45/5.63 60. (-. (distinct_lines T_1 T_1)) (distinct_lines T_1 T_1) ### Axiom % 5.45/5.63 61. (distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) (-. (distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1))) ### Axiom % 5.45/5.65 62. (distinct_lines T_0 T_1) (-. (distinct_lines T_0 T_1)) ### Axiom % 5.45/5.65 63. (-. (apart_point_and_line (intersection_point T_0 T_1) T_0)) (apart_point_and_line (intersection_point T_0 T_1) T_0) ### Axiom % 5.45/5.65 64. (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (apart_point_and_line (intersection_point T_0 T_1) T_1) ### Axiom % 5.45/5.65 65. (apart_point_and_line (intersection_point T_2 T_1) T_0) (-. (apart_point_and_line (intersection_point T_2 T_1) T_0)) ### Axiom % 5.45/5.65 66. (distinct_points (intersection_point T_2 T_1) (intersection_point T_2 T_3)) (-. (distinct_points (intersection_point T_2 T_1) (intersection_point T_2 T_3))) ### Axiom % 5.45/5.65 67. (distinct_lines T_2 T_1) (-. (distinct_lines T_2 T_1)) ### Axiom % 5.45/5.65 68. (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (apart_point_and_line (intersection_point T_2 T_1) T_2) ### Axiom % 5.45/5.65 69. (-. (apart_point_and_line (intersection_point T_2 T_1) T_1)) (apart_point_and_line (intersection_point T_2 T_1) T_1) ### Axiom % 5.45/5.65 70. (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (apart_point_and_line (intersection_point T_2 T_3) T_1) ### Axiom % 5.45/5.65 71. (((distinct_points (intersection_point T_2 T_1) (intersection_point T_2 T_3)) /\ (distinct_lines T_2 T_1)) => ((apart_point_and_line (intersection_point T_2 T_1) T_2) \/ ((apart_point_and_line (intersection_point T_2 T_1) T_1) \/ ((apart_point_and_line (intersection_point T_2 T_3) T_2) \/ (apart_point_and_line (intersection_point T_2 T_3) T_1))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (-. (apart_point_and_line (intersection_point T_2 T_1) T_1)) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (distinct_lines T_2 T_1) (distinct_points (intersection_point T_2 T_1) (intersection_point T_2 T_3)) ### DisjTree 66 67 68 69 6 70 % 5.45/5.65 72. (All V, (((distinct_points (intersection_point T_2 T_1) (intersection_point T_2 T_3)) /\ (distinct_lines T_2 V)) => ((apart_point_and_line (intersection_point T_2 T_1) T_2) \/ ((apart_point_and_line (intersection_point T_2 T_1) V) \/ ((apart_point_and_line (intersection_point T_2 T_3) T_2) \/ (apart_point_and_line (intersection_point T_2 T_3) V)))))) (distinct_points (intersection_point T_2 T_1) (intersection_point T_2 T_3)) (distinct_lines T_2 T_1) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (-. (apart_point_and_line (intersection_point T_2 T_1) T_1)) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) ### All 71 % 5.45/5.65 73. (All U, (All V, (((distinct_points (intersection_point T_2 T_1) (intersection_point T_2 T_3)) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_2 T_1) U) \/ ((apart_point_and_line (intersection_point T_2 T_1) V) \/ ((apart_point_and_line (intersection_point T_2 T_3) U) \/ (apart_point_and_line (intersection_point T_2 T_3) V))))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (-. (apart_point_and_line (intersection_point T_2 T_1) T_1)) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (distinct_lines T_2 T_1) (distinct_points (intersection_point T_2 T_1) (intersection_point T_2 T_3)) ### All 72 % 5.45/5.65 74. (All Y, (All U, (All V, (((distinct_points (intersection_point T_2 T_1) Y) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_2 T_1) U) \/ ((apart_point_and_line (intersection_point T_2 T_1) V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V)))))))) (distinct_points (intersection_point T_2 T_1) (intersection_point T_2 T_3)) (distinct_lines T_2 T_1) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (-. (apart_point_and_line (intersection_point T_2 T_1) T_1)) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) ### All 73 % 5.45/5.65 75. (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (-. (apart_point_and_line (intersection_point T_2 T_1) T_1)) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (distinct_lines T_2 T_1) (distinct_points (intersection_point T_2 T_1) (intersection_point T_2 T_3)) ### All 74 % 5.45/5.65 76. (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (apart_point_and_line (intersection_point T_2 T_3) T_0) ### Axiom % 5.45/5.65 77. ((apart_point_and_line (intersection_point T_2 T_1) T_0) => ((distinct_points (intersection_point T_2 T_1) (intersection_point T_2 T_3)) \/ (apart_point_and_line (intersection_point T_2 T_3) T_0))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (distinct_lines T_2 T_1) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (-. (apart_point_and_line (intersection_point T_2 T_1) T_1)) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (apart_point_and_line (intersection_point T_2 T_1) T_0) ### DisjTree 65 75 76 % 5.45/5.65 78. (All Z, ((apart_point_and_line (intersection_point T_2 T_1) T_0) => ((distinct_points (intersection_point T_2 T_1) Z) \/ (apart_point_and_line Z T_0)))) (apart_point_and_line (intersection_point T_2 T_1) T_0) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (-. (apart_point_and_line (intersection_point T_2 T_1) T_1)) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (distinct_lines T_2 T_1) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) ### All 77 % 5.45/5.65 79. (All Y, (All Z, ((apart_point_and_line (intersection_point T_2 T_1) Y) => ((distinct_points (intersection_point T_2 T_1) Z) \/ (apart_point_and_line Z Y))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (distinct_lines T_2 T_1) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (-. (apart_point_and_line (intersection_point T_2 T_1) T_1)) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (apart_point_and_line (intersection_point T_2 T_1) T_0) ### All 78 % 5.45/5.65 80. (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (apart_point_and_line (intersection_point T_2 T_1) T_0) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (-. (apart_point_and_line (intersection_point T_2 T_1) T_1)) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (distinct_lines T_2 T_1) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) ### All 79 % 5.45/5.68 81. (-. (distinct_lines T_1 T_1)) (distinct_lines T_1 T_1) ### Axiom % 5.45/5.68 82. (convergent_lines T_2 T_1) (-. (convergent_lines T_2 T_1)) ### Axiom % 5.45/5.68 83. (apart_point_and_line (intersection_point T_2 T_1) T_1) (-. (apart_point_and_line (intersection_point T_2 T_1) T_1)) ### Axiom % 5.45/5.68 84. ((convergent_lines T_2 T_1) => (-. (apart_point_and_line (intersection_point T_2 T_1) T_1))) (apart_point_and_line (intersection_point T_2 T_1) T_1) (convergent_lines T_2 T_1) ### Imply 82 83 % 5.45/5.68 85. (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) Y)))) (convergent_lines T_2 T_1) (apart_point_and_line (intersection_point T_2 T_1) T_1) ### All 84 % 5.45/5.68 86. (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (apart_point_and_line (intersection_point T_2 T_1) T_1) (convergent_lines T_2 T_1) ### All 85 % 5.45/5.68 87. ((apart_point_and_line (intersection_point T_2 T_1) T_1) => ((distinct_lines T_1 T_1) \/ (apart_point_and_line (intersection_point T_2 T_1) T_1))) (convergent_lines T_2 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (distinct_lines T_1 T_1)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (distinct_lines T_2 T_1) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (apart_point_and_line (intersection_point T_2 T_1) T_0) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) ### DisjTree 80 81 86 % 5.45/5.68 88. (All Z, ((apart_point_and_line (intersection_point T_2 T_1) T_1) => ((distinct_lines T_1 Z) \/ (apart_point_and_line (intersection_point T_2 T_1) Z)))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (apart_point_and_line (intersection_point T_2 T_1) T_0) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (distinct_lines T_2 T_1) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (-. (distinct_lines T_1 T_1)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_2 T_1) ### All 87 % 5.45/5.68 89. (All Y, (All Z, ((apart_point_and_line (intersection_point T_2 T_1) Y) => ((distinct_lines Y Z) \/ (apart_point_and_line (intersection_point T_2 T_1) Z))))) (convergent_lines T_2 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (distinct_lines T_1 T_1)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (distinct_lines T_2 T_1) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (apart_point_and_line (intersection_point T_2 T_1) T_0) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) ### All 88 % 5.45/5.68 90. (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (apart_point_and_line (intersection_point T_2 T_1) T_0) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (distinct_lines T_2 T_1) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (-. (distinct_lines T_1 T_1)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_2 T_1) ### All 89 % 5.45/5.68 91. (((distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) /\ (distinct_lines T_0 T_1)) => ((apart_point_and_line (intersection_point T_0 T_1) T_0) \/ ((apart_point_and_line (intersection_point T_0 T_1) T_1) \/ ((apart_point_and_line (intersection_point T_2 T_1) T_0) \/ (apart_point_and_line (intersection_point T_2 T_1) T_1))))) (convergent_lines T_2 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (distinct_lines T_1 T_1)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (distinct_lines T_2 T_1) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (-. (apart_point_and_line (intersection_point T_0 T_1) T_0)) (distinct_lines T_0 T_1) (distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) ### DisjTree 61 62 63 64 90 86 % 5.45/5.68 92. (All V, (((distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) /\ (distinct_lines T_0 V)) => ((apart_point_and_line (intersection_point T_0 T_1) T_0) \/ ((apart_point_and_line (intersection_point T_0 T_1) V) \/ ((apart_point_and_line (intersection_point T_2 T_1) T_0) \/ (apart_point_and_line (intersection_point T_2 T_1) V)))))) (distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) (distinct_lines T_0 T_1) (-. (apart_point_and_line (intersection_point T_0 T_1) T_0)) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (distinct_lines T_2 T_1) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (-. (distinct_lines T_1 T_1)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_2 T_1) ### All 91 % 5.45/5.70 93. (All U, (All V, (((distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_1) U) \/ ((apart_point_and_line (intersection_point T_0 T_1) V) \/ ((apart_point_and_line (intersection_point T_2 T_1) U) \/ (apart_point_and_line (intersection_point T_2 T_1) V))))))) (convergent_lines T_2 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (distinct_lines T_1 T_1)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (distinct_lines T_2 T_1) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (-. (apart_point_and_line (intersection_point T_0 T_1) T_0)) (distinct_lines T_0 T_1) (distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) ### All 92 % 5.45/5.70 94. ((distinct_lines T_1 T_0) => ((distinct_lines T_1 T_1) \/ (distinct_lines T_0 T_1))) (distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) (-. (apart_point_and_line (intersection_point T_0 T_1) T_0)) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (distinct_lines T_2 T_1) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_2 T_1) (All U, (All V, (((distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_1) U) \/ ((apart_point_and_line (intersection_point T_0 T_1) V) \/ ((apart_point_and_line (intersection_point T_2 T_1) U) \/ (apart_point_and_line (intersection_point T_2 T_1) V))))))) (-. (distinct_lines T_1 T_1)) (distinct_lines T_1 T_0) ### DisjTree 59 60 93 % 5.45/5.70 95. (All Z, ((distinct_lines T_1 T_0) => ((distinct_lines T_1 Z) \/ (distinct_lines T_0 Z)))) (distinct_lines T_1 T_0) (-. (distinct_lines T_1 T_1)) (All U, (All V, (((distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_1) U) \/ ((apart_point_and_line (intersection_point T_0 T_1) V) \/ ((apart_point_and_line (intersection_point T_2 T_1) U) \/ (apart_point_and_line (intersection_point T_2 T_1) V))))))) (convergent_lines T_2 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (distinct_lines T_2 T_1) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (-. (apart_point_and_line (intersection_point T_0 T_1) T_0)) (distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) ### All 94 % 5.45/5.70 96. (All Y, (All Z, ((distinct_lines T_1 Y) => ((distinct_lines T_1 Z) \/ (distinct_lines Y Z))))) (distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) (-. (apart_point_and_line (intersection_point T_0 T_1) T_0)) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (distinct_lines T_2 T_1) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_2 T_1) (All U, (All V, (((distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_1) U) \/ ((apart_point_and_line (intersection_point T_0 T_1) V) \/ ((apart_point_and_line (intersection_point T_2 T_1) U) \/ (apart_point_and_line (intersection_point T_2 T_1) V))))))) (-. (distinct_lines T_1 T_1)) (distinct_lines T_1 T_0) ### All 95 % 5.45/5.70 97. (-. (convergent_lines T_0 T_0)) (convergent_lines T_0 T_0) ### Axiom % 5.45/5.70 98. ((convergent_lines T_0 T_1) => ((distinct_lines T_1 T_0) \/ (convergent_lines T_0 T_0))) (-. (convergent_lines T_0 T_0)) (-. (distinct_lines T_1 T_1)) (All U, (All V, (((distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_1) U) \/ ((apart_point_and_line (intersection_point T_0 T_1) V) \/ ((apart_point_and_line (intersection_point T_2 T_1) U) \/ (apart_point_and_line (intersection_point T_2 T_1) V))))))) (convergent_lines T_2 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (distinct_lines T_2 T_1) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (-. (apart_point_and_line (intersection_point T_0 T_1) T_0)) (distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) (All Y, (All Z, ((distinct_lines T_1 Y) => ((distinct_lines T_1 Z) \/ (distinct_lines Y Z))))) (convergent_lines T_0 T_1) ### DisjTree 58 96 97 % 5.54/5.73 99. (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (convergent_lines T_0 T_1) (All Y, (All Z, ((distinct_lines T_1 Y) => ((distinct_lines T_1 Z) \/ (distinct_lines Y Z))))) (distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) (-. (apart_point_and_line (intersection_point T_0 T_1) T_0)) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (distinct_lines T_2 T_1) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_2 T_1) (All U, (All V, (((distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_1) U) \/ ((apart_point_and_line (intersection_point T_0 T_1) V) \/ ((apart_point_and_line (intersection_point T_2 T_1) U) \/ (apart_point_and_line (intersection_point T_2 T_1) V))))))) (-. (distinct_lines T_1 T_1)) (-. (convergent_lines T_0 T_0)) ### All 98 % 5.54/5.73 100. (All X, (-. (convergent_lines X X))) (-. (distinct_lines T_1 T_1)) (All U, (All V, (((distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_1) U) \/ ((apart_point_and_line (intersection_point T_0 T_1) V) \/ ((apart_point_and_line (intersection_point T_2 T_1) U) \/ (apart_point_and_line (intersection_point T_2 T_1) V))))))) (convergent_lines T_2 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (distinct_lines T_2 T_1) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (-. (apart_point_and_line (intersection_point T_0 T_1) T_0)) (distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) (All Y, (All Z, ((distinct_lines T_1 Y) => ((distinct_lines T_1 Z) \/ (distinct_lines Y Z))))) (convergent_lines T_0 T_1) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) ### All 99 % 5.54/5.73 101. (distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) (-. (distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1))) ### Axiom % 5.54/5.73 102. (distinct_lines T_0 T_1) (-. (distinct_lines T_0 T_1)) ### Axiom % 5.54/5.73 103. (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (apart_point_and_line (intersection_point T_0 T_1) T_1) ### Axiom % 5.54/5.73 104. (-. (apart_point_and_line (intersection_point T_2 T_1) T_1)) (apart_point_and_line (intersection_point T_2 T_1) T_1) ### Axiom % 5.54/5.73 105. (((distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) /\ (distinct_lines T_0 T_1)) => ((apart_point_and_line (intersection_point T_0 T_1) T_0) \/ ((apart_point_and_line (intersection_point T_0 T_1) T_1) \/ ((apart_point_and_line (intersection_point T_2 T_1) T_0) \/ (apart_point_and_line (intersection_point T_2 T_1) T_1))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (distinct_lines T_2 T_1) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (-. (apart_point_and_line (intersection_point T_2 T_1) T_1)) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All Z, ((apart_point_and_line (intersection_point T_2 T_1) T_0) => ((distinct_points (intersection_point T_2 T_1) Z) \/ (apart_point_and_line Z T_0)))) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (convergent_lines T_0 T_1) (All Y, ((convergent_lines T_0 Y) => (-. (apart_point_and_line (intersection_point T_0 Y) T_0)))) (distinct_lines T_0 T_1) (distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) ### DisjTree 101 102 33 103 78 104 % 5.54/5.73 106. (All V, (((distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) /\ (distinct_lines T_0 V)) => ((apart_point_and_line (intersection_point T_0 T_1) T_0) \/ ((apart_point_and_line (intersection_point T_0 T_1) V) \/ ((apart_point_and_line (intersection_point T_2 T_1) T_0) \/ (apart_point_and_line (intersection_point T_2 T_1) V)))))) (distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) (distinct_lines T_0 T_1) (All Y, ((convergent_lines T_0 Y) => (-. (apart_point_and_line (intersection_point T_0 Y) T_0)))) (convergent_lines T_0 T_1) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (All Z, ((apart_point_and_line (intersection_point T_2 T_1) T_0) => ((distinct_points (intersection_point T_2 T_1) Z) \/ (apart_point_and_line Z T_0)))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (-. (apart_point_and_line (intersection_point T_2 T_1) T_1)) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (distinct_lines T_2 T_1) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) ### All 105 % 5.54/5.73 107. (All U, (All V, (((distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_1) U) \/ ((apart_point_and_line (intersection_point T_0 T_1) V) \/ ((apart_point_and_line (intersection_point T_2 T_1) U) \/ (apart_point_and_line (intersection_point T_2 T_1) V))))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (distinct_lines T_2 T_1) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (-. (apart_point_and_line (intersection_point T_2 T_1) T_1)) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All Z, ((apart_point_and_line (intersection_point T_2 T_1) T_0) => ((distinct_points (intersection_point T_2 T_1) Z) \/ (apart_point_and_line Z T_0)))) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (convergent_lines T_0 T_1) (All Y, ((convergent_lines T_0 Y) => (-. (apart_point_and_line (intersection_point T_0 Y) T_0)))) (distinct_lines T_0 T_1) (distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) ### All 106 % 5.54/5.77 108. (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (apart_point_and_line (intersection_point T_0 T_1) T_1) ### Axiom % 5.54/5.77 109. ((apart_point_and_line (intersection_point T_0 T_1) T_0) => ((distinct_lines T_0 T_1) \/ (apart_point_and_line (intersection_point T_0 T_1) T_1))) (All Y, ((convergent_lines T_0 Y) => (-. (apart_point_and_line (intersection_point T_0 Y) T_0)))) (All Z, ((apart_point_and_line (intersection_point T_2 T_1) T_0) => ((distinct_points (intersection_point T_2 T_1) Z) \/ (apart_point_and_line Z T_0)))) (-. (apart_point_and_line (intersection_point T_2 T_1) T_1)) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (convergent_lines T_0 T_1) (All Y, (All Z, ((distinct_lines T_1 Y) => ((distinct_lines T_1 Z) \/ (distinct_lines Y Z))))) (distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (distinct_lines T_2 T_1) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_2 T_1) (All U, (All V, (((distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_1) U) \/ ((apart_point_and_line (intersection_point T_0 T_1) V) \/ ((apart_point_and_line (intersection_point T_2 T_1) U) \/ (apart_point_and_line (intersection_point T_2 T_1) V))))))) (-. (distinct_lines T_1 T_1)) (All X, (-. (convergent_lines X X))) ### DisjTree 100 107 108 % 5.54/5.77 110. (All Z, ((apart_point_and_line (intersection_point T_0 T_1) T_0) => ((distinct_lines T_0 Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z)))) (All X, (-. (convergent_lines X X))) (-. (distinct_lines T_1 T_1)) (All U, (All V, (((distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_1) U) \/ ((apart_point_and_line (intersection_point T_0 T_1) V) \/ ((apart_point_and_line (intersection_point T_2 T_1) U) \/ (apart_point_and_line (intersection_point T_2 T_1) V))))))) (convergent_lines T_2 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (distinct_lines T_2 T_1) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) (All Y, (All Z, ((distinct_lines T_1 Y) => ((distinct_lines T_1 Z) \/ (distinct_lines Y Z))))) (convergent_lines T_0 T_1) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (-. (apart_point_and_line (intersection_point T_2 T_1) T_1)) (All Z, ((apart_point_and_line (intersection_point T_2 T_1) T_0) => ((distinct_points (intersection_point T_2 T_1) Z) \/ (apart_point_and_line Z T_0)))) (All Y, ((convergent_lines T_0 Y) => (-. (apart_point_and_line (intersection_point T_0 Y) T_0)))) ### All 109 % 5.54/5.77 111. (All Y, (All Z, ((apart_point_and_line (intersection_point T_0 T_1) Y) => ((distinct_lines Y Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z))))) (All Y, ((convergent_lines T_0 Y) => (-. (apart_point_and_line (intersection_point T_0 Y) T_0)))) (All Z, ((apart_point_and_line (intersection_point T_2 T_1) T_0) => ((distinct_points (intersection_point T_2 T_1) Z) \/ (apart_point_and_line Z T_0)))) (-. (apart_point_and_line (intersection_point T_2 T_1) T_1)) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (convergent_lines T_0 T_1) (All Y, (All Z, ((distinct_lines T_1 Y) => ((distinct_lines T_1 Z) \/ (distinct_lines Y Z))))) (distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (distinct_lines T_2 T_1) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_2 T_1) (All U, (All V, (((distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_1) U) \/ ((apart_point_and_line (intersection_point T_0 T_1) V) \/ ((apart_point_and_line (intersection_point T_2 T_1) U) \/ (apart_point_and_line (intersection_point T_2 T_1) V))))))) (-. (distinct_lines T_1 T_1)) (All X, (-. (convergent_lines X X))) ### All 110 % 5.54/5.77 112. (All Y, (All Z, ((apart_point_and_line (intersection_point T_2 T_1) Y) => ((distinct_points (intersection_point T_2 T_1) Z) \/ (apart_point_and_line Z Y))))) (All X, (-. (convergent_lines X X))) (-. (distinct_lines T_1 T_1)) (All U, (All V, (((distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_1) U) \/ ((apart_point_and_line (intersection_point T_0 T_1) V) \/ ((apart_point_and_line (intersection_point T_2 T_1) U) \/ (apart_point_and_line (intersection_point T_2 T_1) V))))))) (convergent_lines T_2 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (distinct_lines T_2 T_1) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) (All Y, (All Z, ((distinct_lines T_1 Y) => ((distinct_lines T_1 Z) \/ (distinct_lines Y Z))))) (convergent_lines T_0 T_1) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (-. (apart_point_and_line (intersection_point T_2 T_1) T_1)) (All Y, ((convergent_lines T_0 Y) => (-. (apart_point_and_line (intersection_point T_0 Y) T_0)))) (All Y, (All Z, ((apart_point_and_line (intersection_point T_0 T_1) Y) => ((distinct_lines Y Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z))))) ### All 111 % 5.54/5.78 113. (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All Y, (All Z, ((apart_point_and_line (intersection_point T_0 T_1) Y) => ((distinct_lines Y Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z))))) (-. (apart_point_and_line (intersection_point T_2 T_1) T_1)) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (convergent_lines T_0 T_1) (All Y, (All Z, ((distinct_lines T_1 Y) => ((distinct_lines T_1 Z) \/ (distinct_lines Y Z))))) (distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (distinct_lines T_2 T_1) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_2 T_1) (All U, (All V, (((distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_1) U) \/ ((apart_point_and_line (intersection_point T_0 T_1) V) \/ ((apart_point_and_line (intersection_point T_2 T_1) U) \/ (apart_point_and_line (intersection_point T_2 T_1) V))))))) (-. (distinct_lines T_1 T_1)) (All X, (-. (convergent_lines X X))) (All Y, (All Z, ((apart_point_and_line (intersection_point T_2 T_1) Y) => ((distinct_points (intersection_point T_2 T_1) Z) \/ (apart_point_and_line Z Y))))) ### All 112 % 5.54/5.78 114. (-. (distinct_lines T_1 T_1)) (distinct_lines T_1 T_1) ### Axiom % 5.54/5.78 115. ((apart_point_and_line (intersection_point T_2 T_1) T_1) => ((distinct_lines T_1 T_1) \/ (apart_point_and_line (intersection_point T_2 T_1) T_1))) (convergent_lines T_2 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (distinct_lines T_1 T_1)) (distinct_points (intersection_point T_2 T_1) (intersection_point T_2 T_3)) (distinct_lines T_2 T_1) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) ### DisjTree 75 114 86 % 5.54/5.78 116. (All Z, ((apart_point_and_line (intersection_point T_2 T_1) T_1) => ((distinct_lines T_1 Z) \/ (apart_point_and_line (intersection_point T_2 T_1) Z)))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (distinct_lines T_2 T_1) (distinct_points (intersection_point T_2 T_1) (intersection_point T_2 T_3)) (-. (distinct_lines T_1 T_1)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_2 T_1) ### All 115 % 5.54/5.78 117. (All Y, (All Z, ((apart_point_and_line (intersection_point T_2 T_1) Y) => ((distinct_lines Y Z) \/ (apart_point_and_line (intersection_point T_2 T_1) Z))))) (convergent_lines T_2 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (distinct_lines T_1 T_1)) (distinct_points (intersection_point T_2 T_1) (intersection_point T_2 T_3)) (distinct_lines T_2 T_1) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) ### All 116 % 5.54/5.78 118. (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (distinct_lines T_2 T_1) (distinct_points (intersection_point T_2 T_1) (intersection_point T_2 T_3)) (-. (distinct_lines T_1 T_1)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_2 T_1) ### All 117 % 5.54/5.78 119. (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (apart_point_and_line (intersection_point T_2 T_3) T_1) ### Axiom % 5.54/5.78 120. ((apart_point_and_line (intersection_point T_2 T_1) T_1) => ((distinct_points (intersection_point T_2 T_1) (intersection_point T_2 T_3)) \/ (apart_point_and_line (intersection_point T_2 T_3) T_1))) (All Y, (All Z, ((apart_point_and_line (intersection_point T_2 T_1) Y) => ((distinct_points (intersection_point T_2 T_1) Z) \/ (apart_point_and_line Z Y))))) (All X, (-. (convergent_lines X X))) (-. (distinct_lines T_1 T_1)) (All U, (All V, (((distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_1) U) \/ ((apart_point_and_line (intersection_point T_0 T_1) V) \/ ((apart_point_and_line (intersection_point T_2 T_1) U) \/ (apart_point_and_line (intersection_point T_2 T_1) V))))))) (convergent_lines T_2 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (distinct_lines T_2 T_1) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) (All Y, (All Z, ((distinct_lines T_1 Y) => ((distinct_lines T_1 Z) \/ (distinct_lines Y Z))))) (convergent_lines T_0 T_1) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (All Y, (All Z, ((apart_point_and_line (intersection_point T_0 T_1) Y) => ((distinct_lines Y Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z))))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) ### DisjTree 113 118 119 % 5.63/5.81 121. (All Z, ((apart_point_and_line (intersection_point T_2 T_1) T_1) => ((distinct_points (intersection_point T_2 T_1) Z) \/ (apart_point_and_line Z T_1)))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All Y, (All Z, ((apart_point_and_line (intersection_point T_0 T_1) Y) => ((distinct_lines Y Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z))))) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (convergent_lines T_0 T_1) (All Y, (All Z, ((distinct_lines T_1 Y) => ((distinct_lines T_1 Z) \/ (distinct_lines Y Z))))) (distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (distinct_lines T_2 T_1) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_2 T_1) (All U, (All V, (((distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_1) U) \/ ((apart_point_and_line (intersection_point T_0 T_1) V) \/ ((apart_point_and_line (intersection_point T_2 T_1) U) \/ (apart_point_and_line (intersection_point T_2 T_1) V))))))) (-. (distinct_lines T_1 T_1)) (All X, (-. (convergent_lines X X))) (All Y, (All Z, ((apart_point_and_line (intersection_point T_2 T_1) Y) => ((distinct_points (intersection_point T_2 T_1) Z) \/ (apart_point_and_line Z Y))))) ### All 120 % 5.63/5.81 122. (All Y, (All Z, ((apart_point_and_line (intersection_point T_2 T_1) Y) => ((distinct_points (intersection_point T_2 T_1) Z) \/ (apart_point_and_line Z Y))))) (All X, (-. (convergent_lines X X))) (-. (distinct_lines T_1 T_1)) (All U, (All V, (((distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_1) U) \/ ((apart_point_and_line (intersection_point T_0 T_1) V) \/ ((apart_point_and_line (intersection_point T_2 T_1) U) \/ (apart_point_and_line (intersection_point T_2 T_1) V))))))) (convergent_lines T_2 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (distinct_lines T_2 T_1) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) (All Y, (All Z, ((distinct_lines T_1 Y) => ((distinct_lines T_1 Z) \/ (distinct_lines Y Z))))) (convergent_lines T_0 T_1) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (All Y, (All Z, ((apart_point_and_line (intersection_point T_0 T_1) Y) => ((distinct_lines Y Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z))))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) ### All 121 % 5.63/5.81 123. (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All Y, (All Z, ((apart_point_and_line (intersection_point T_0 T_1) Y) => ((distinct_lines Y Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z))))) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (convergent_lines T_0 T_1) (All Y, (All Z, ((distinct_lines T_1 Y) => ((distinct_lines T_1 Z) \/ (distinct_lines Y Z))))) (distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (distinct_lines T_2 T_1) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_2 T_1) (All U, (All V, (((distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_1) U) \/ ((apart_point_and_line (intersection_point T_0 T_1) V) \/ ((apart_point_and_line (intersection_point T_2 T_1) U) \/ (apart_point_and_line (intersection_point T_2 T_1) V))))))) (-. (distinct_lines T_1 T_1)) (All X, (-. (convergent_lines X X))) ### All 122 % 5.63/5.81 124. (All Y, (All U, (All V, (((distinct_points (intersection_point T_0 T_1) Y) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_1) U) \/ ((apart_point_and_line (intersection_point T_0 T_1) V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V)))))))) (All X, (-. (convergent_lines X X))) (-. (distinct_lines T_1 T_1)) (convergent_lines T_2 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (distinct_lines T_2 T_1) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) (All Y, (All Z, ((distinct_lines T_1 Y) => ((distinct_lines T_1 Z) \/ (distinct_lines Y Z))))) (convergent_lines T_0 T_1) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (All Y, (All Z, ((apart_point_and_line (intersection_point T_0 T_1) Y) => ((distinct_lines Y Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z))))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) ### All 123 % 5.63/5.83 125. (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All Y, (All Z, ((apart_point_and_line (intersection_point T_0 T_1) Y) => ((distinct_lines Y Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z))))) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (convergent_lines T_0 T_1) (All Y, (All Z, ((distinct_lines T_1 Y) => ((distinct_lines T_1 Z) \/ (distinct_lines Y Z))))) (distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (distinct_lines T_2 T_1) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_2 T_1) (-. (distinct_lines T_1 T_1)) (All X, (-. (convergent_lines X X))) ### All 124 % 5.63/5.83 126. (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (apart_point_and_line (intersection_point T_2 T_1) T_2) ### Axiom % 5.63/5.83 127. ((apart_point_and_line (intersection_point T_0 T_1) T_2) => ((distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_1)) \/ (apart_point_and_line (intersection_point T_2 T_1) T_2))) (All X, (-. (convergent_lines X X))) (-. (distinct_lines T_1 T_1)) (convergent_lines T_2 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (distinct_lines T_2 T_1) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (All Y, (All Z, ((distinct_lines T_1 Y) => ((distinct_lines T_1 Z) \/ (distinct_lines Y Z))))) (convergent_lines T_0 T_1) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (All Y, (All Z, ((apart_point_and_line (intersection_point T_0 T_1) Y) => ((distinct_lines Y Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z))))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (apart_point_and_line (intersection_point T_0 T_1) T_2) ### DisjTree 57 125 126 % 5.63/5.83 128. (All Z, ((apart_point_and_line (intersection_point T_0 T_1) T_2) => ((distinct_points (intersection_point T_0 T_1) Z) \/ (apart_point_and_line Z T_2)))) (apart_point_and_line (intersection_point T_0 T_1) T_2) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All Y, (All Z, ((apart_point_and_line (intersection_point T_0 T_1) Y) => ((distinct_lines Y Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z))))) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (convergent_lines T_0 T_1) (All Y, (All Z, ((distinct_lines T_1 Y) => ((distinct_lines T_1 Z) \/ (distinct_lines Y Z))))) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (distinct_lines T_2 T_1) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_2 T_1) (-. (distinct_lines T_1 T_1)) (All X, (-. (convergent_lines X X))) ### All 127 % 5.63/5.83 129. (All Y, (All Z, ((apart_point_and_line (intersection_point T_0 T_1) Y) => ((distinct_points (intersection_point T_0 T_1) Z) \/ (apart_point_and_line Z Y))))) (All X, (-. (convergent_lines X X))) (-. (distinct_lines T_1 T_1)) (convergent_lines T_2 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (distinct_lines T_2 T_1) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (All Y, (All Z, ((distinct_lines T_1 Y) => ((distinct_lines T_1 Z) \/ (distinct_lines Y Z))))) (convergent_lines T_0 T_1) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (All Y, (All Z, ((apart_point_and_line (intersection_point T_0 T_1) Y) => ((distinct_lines Y Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z))))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (apart_point_and_line (intersection_point T_0 T_1) T_2) ### All 128 % 5.63/5.83 130. (apart_point_and_line (intersection_point T_0 T_1) T_2) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All Y, (All Z, ((apart_point_and_line (intersection_point T_0 T_1) Y) => ((distinct_lines Y Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z))))) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (convergent_lines T_0 T_1) (All Y, (All Z, ((distinct_lines T_1 Y) => ((distinct_lines T_1 Z) \/ (distinct_lines Y Z))))) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (distinct_lines T_2 T_1) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_2 T_1) (-. (distinct_lines T_1 T_1)) (All X, (-. (convergent_lines X X))) ### All 129 % 5.63/5.84 131. (-. (distinct_lines T_1 T_1)) (distinct_lines T_1 T_1) ### Axiom % 5.63/5.84 132. ((apart_point_and_line (intersection_point T_0 T_1) T_1) => ((distinct_lines T_1 T_1) \/ (apart_point_and_line (intersection_point T_0 T_1) T_1))) (All X, (-. (convergent_lines X X))) (-. (distinct_lines T_1 T_1)) (convergent_lines T_2 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (distinct_lines T_2 T_1) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All Y, (All Z, ((distinct_lines T_1 Y) => ((distinct_lines T_1 Z) \/ (distinct_lines Y Z))))) (convergent_lines T_0 T_1) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (All Y, (All Z, ((apart_point_and_line (intersection_point T_0 T_1) Y) => ((distinct_lines Y Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z))))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (apart_point_and_line (intersection_point T_0 T_1) T_2) ### DisjTree 130 131 23 % 5.63/5.84 133. (All Z, ((apart_point_and_line (intersection_point T_0 T_1) T_1) => ((distinct_lines T_1 Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z)))) (apart_point_and_line (intersection_point T_0 T_1) T_2) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All Y, (All Z, ((apart_point_and_line (intersection_point T_0 T_1) Y) => ((distinct_lines Y Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z))))) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (convergent_lines T_0 T_1) (All Y, (All Z, ((distinct_lines T_1 Y) => ((distinct_lines T_1 Z) \/ (distinct_lines Y Z))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (distinct_lines T_2 T_1) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_2 T_1) (-. (distinct_lines T_1 T_1)) (All X, (-. (convergent_lines X X))) ### All 132 % 5.63/5.84 134. ((apart_point_and_line (intersection_point T_0 T_1) T_2) => ((distinct_lines T_2 T_1) \/ (apart_point_and_line (intersection_point T_0 T_1) T_1))) (All X, (-. (convergent_lines X X))) (-. (distinct_lines T_1 T_1)) (convergent_lines T_2 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All Y, (All Z, ((distinct_lines T_1 Y) => ((distinct_lines T_1 Z) \/ (distinct_lines Y Z))))) (convergent_lines T_0 T_1) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (All Y, (All Z, ((apart_point_and_line (intersection_point T_0 T_1) Y) => ((distinct_lines Y Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z))))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All Z, ((apart_point_and_line (intersection_point T_0 T_1) T_1) => ((distinct_lines T_1 Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z)))) (apart_point_and_line (intersection_point T_0 T_1) T_2) ### DisjTree 56 133 23 % 5.63/5.84 135. (All Z, ((apart_point_and_line (intersection_point T_0 T_1) T_2) => ((distinct_lines T_2 Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z)))) (apart_point_and_line (intersection_point T_0 T_1) T_2) (All Z, ((apart_point_and_line (intersection_point T_0 T_1) T_1) => ((distinct_lines T_1 Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z)))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All Y, (All Z, ((apart_point_and_line (intersection_point T_0 T_1) Y) => ((distinct_lines Y Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z))))) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (convergent_lines T_0 T_1) (All Y, (All Z, ((distinct_lines T_1 Y) => ((distinct_lines T_1 Z) \/ (distinct_lines Y Z))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_2 T_1) (-. (distinct_lines T_1 T_1)) (All X, (-. (convergent_lines X X))) ### All 134 % 5.63/5.84 136. (All X, (-. (convergent_lines X X))) (-. (distinct_lines T_1 T_1)) (convergent_lines T_2 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All Y, (All Z, ((distinct_lines T_1 Y) => ((distinct_lines T_1 Z) \/ (distinct_lines Y Z))))) (convergent_lines T_0 T_1) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (All Y, (All Z, ((apart_point_and_line (intersection_point T_0 T_1) Y) => ((distinct_lines Y Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z))))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (apart_point_and_line (intersection_point T_0 T_1) T_2) (All Z, ((apart_point_and_line (intersection_point T_0 T_1) T_2) => ((distinct_lines T_2 Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z)))) ### All 135 % 5.63/5.87 137. (apart_point_and_line (intersection_point T_0 T_1) T_2) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All Y, (All Z, ((apart_point_and_line (intersection_point T_0 T_1) Y) => ((distinct_lines Y Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z))))) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (convergent_lines T_0 T_1) (All Y, (All Z, ((distinct_lines T_1 Y) => ((distinct_lines T_1 Z) \/ (distinct_lines Y Z))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_2 T_1) (-. (distinct_lines T_1 T_1)) (All X, (-. (convergent_lines X X))) ### All 136 % 5.63/5.87 138. (All X, (-. (convergent_lines X X))) (-. (distinct_lines T_1 T_1)) (convergent_lines T_2 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All Y, (All Z, ((distinct_lines T_1 Y) => ((distinct_lines T_1 Z) \/ (distinct_lines Y Z))))) (convergent_lines T_0 T_1) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (apart_point_and_line (intersection_point T_0 T_1) T_2) ### All 137 % 5.63/5.87 139. (All X, (All Y, (All Z, ((distinct_lines X Y) => ((distinct_lines X Z) \/ (distinct_lines Y Z)))))) (apart_point_and_line (intersection_point T_0 T_1) T_2) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (convergent_lines T_0 T_1) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_2 T_1) (-. (distinct_lines T_1 T_1)) (All X, (-. (convergent_lines X X))) ### All 138 % 5.63/5.87 140. (-. (convergent_lines T_1 T_1)) (convergent_lines T_1 T_1) ### Axiom % 5.63/5.87 141. ((convergent_lines T_2 T_1) => ((convergent_lines T_2 T_1) \/ (convergent_lines T_1 T_1))) (-. (convergent_lines T_1 T_1)) (-. (distinct_lines T_1 T_1)) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (All X, (All Y, (All Z, ((distinct_lines X Y) => ((distinct_lines X Z) \/ (distinct_lines Y Z)))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (-. (convergent_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (All X, (-. (distinct_lines X X))) (convergent_lines T_0 T_1) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (apart_point_and_line (intersection_point T_0 T_1) T_2) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((distinct_lines Y Z) => ((apart_point_and_line X Y) \/ ((apart_point_and_line X Z) \/ (convergent_lines Y Z))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) ### DisjTree 53 139 140 % 5.63/5.87 142. (All Z, ((convergent_lines T_2 T_1) => ((convergent_lines T_2 Z) \/ (convergent_lines T_1 Z)))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((distinct_lines Y Z) => ((apart_point_and_line X Y) \/ ((apart_point_and_line X Z) \/ (convergent_lines Y Z))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (apart_point_and_line (intersection_point T_0 T_1) T_2) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (convergent_lines T_0 T_1) (All X, (-. (distinct_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (convergent_lines X X))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((distinct_lines X Y) => ((distinct_lines X Z) \/ (distinct_lines Y Z)))))) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (-. (distinct_lines T_1 T_1)) (-. (convergent_lines T_1 T_1)) ### All 141 % 5.63/5.87 143. (-. (convergent_lines T_1 T_1)) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (All X, (All Y, (All Z, ((distinct_lines X Y) => ((distinct_lines X Z) \/ (distinct_lines Y Z)))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (-. (convergent_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (All X, (-. (distinct_lines X X))) (convergent_lines T_0 T_1) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (apart_point_and_line (intersection_point T_0 T_1) T_2) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((distinct_lines Y Z) => ((apart_point_and_line X Y) \/ ((apart_point_and_line X Z) \/ (convergent_lines Y Z))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All Z, ((convergent_lines T_2 T_1) => ((convergent_lines T_2 Z) \/ (convergent_lines T_1 Z)))) ### All 142 % 5.63/5.87 144. (All Y, (All Z, ((convergent_lines T_2 Y) => ((convergent_lines T_2 Z) \/ (convergent_lines Y Z))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((distinct_lines Y Z) => ((apart_point_and_line X Y) \/ ((apart_point_and_line X Z) \/ (convergent_lines Y Z))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (apart_point_and_line (intersection_point T_0 T_1) T_2) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (convergent_lines T_0 T_1) (All X, (-. (distinct_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (convergent_lines X X))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((distinct_lines X Y) => ((distinct_lines X Z) \/ (distinct_lines Y Z)))))) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (-. (convergent_lines T_1 T_1)) ### All 143 % 5.63/5.87 145. (All Y, (All Z, ((convergent_lines T_0 Y) => ((distinct_lines Y Z) \/ (convergent_lines T_0 Z))))) (-. (convergent_lines T_1 T_1)) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (All X, (All Y, (All Z, ((distinct_lines X Y) => ((distinct_lines X Z) \/ (distinct_lines Y Z)))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (-. (convergent_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (All X, (-. (distinct_lines X X))) (convergent_lines T_0 T_1) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (apart_point_and_line (intersection_point T_0 T_1) T_2) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((distinct_lines Y Z) => ((apart_point_and_line X Y) \/ ((apart_point_and_line X Z) \/ (convergent_lines Y Z))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All Y, (All Z, ((convergent_lines T_2 Y) => ((convergent_lines T_2 Z) \/ (convergent_lines Y Z))))) ### All 144 % 5.63/5.87 146. (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((distinct_lines Y Z) => ((apart_point_and_line X Y) \/ ((apart_point_and_line X Z) \/ (convergent_lines Y Z))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (apart_point_and_line (intersection_point T_0 T_1) T_2) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_0 T_1) (All X, (-. (distinct_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (convergent_lines X X))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((distinct_lines X Y) => ((distinct_lines X Z) \/ (distinct_lines Y Z)))))) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (-. (convergent_lines T_1 T_1)) (All Y, (All Z, ((convergent_lines T_0 Y) => ((distinct_lines Y Z) \/ (convergent_lines T_0 Z))))) ### All 145 % 5.63/5.87 147. (All X, (All Y, (All Z, ((convergent_lines X Y) => ((distinct_lines Y Z) \/ (convergent_lines X Z)))))) (-. (convergent_lines T_1 T_1)) (-. (apart_point_and_line (intersection_point T_2 T_1) T_2)) (All X, (All Y, (All Z, ((distinct_lines X Y) => ((distinct_lines X Z) \/ (distinct_lines Y Z)))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (-. (convergent_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (All X, (-. (distinct_lines X X))) (convergent_lines T_0 T_1) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (apart_point_and_line (intersection_point T_0 T_1) T_2) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((distinct_lines Y Z) => ((apart_point_and_line X Y) \/ ((apart_point_and_line X Z) \/ (convergent_lines Y Z))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) ### All 146 % 5.63/5.88 148. ((convergent_lines T_2 T_1) => (-. (apart_point_and_line (intersection_point T_2 T_1) T_2))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (All X, (All Y, (All Z, ((distinct_lines X Y) => ((distinct_lines X Z) \/ (distinct_lines Y Z)))))) (-. (convergent_lines T_1 T_1)) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (-. (convergent_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (All X, (-. (distinct_lines X X))) (convergent_lines T_0 T_1) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (apart_point_and_line (intersection_point T_0 T_1) T_2) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((distinct_lines Y Z) => ((apart_point_and_line X Y) \/ ((apart_point_and_line X Z) \/ (convergent_lines Y Z))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((distinct_lines Y Z) \/ (convergent_lines X Z)))))) ### Imply 55 147 % 5.63/5.88 149. (All X, (All Y, (All Z, ((convergent_lines X Y) => ((distinct_lines Y Z) \/ (convergent_lines X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((distinct_lines Y Z) => ((apart_point_and_line X Y) \/ ((apart_point_and_line X Z) \/ (convergent_lines Y Z))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (apart_point_and_line (intersection_point T_0 T_1) T_2) (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) T_2)))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_0 T_1) (All X, (-. (distinct_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (convergent_lines X X))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (-. (convergent_lines T_1 T_1)) (All X, (All Y, (All Z, ((distinct_lines X Y) => ((distinct_lines X Z) \/ (distinct_lines Y Z)))))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) ### All 148 % 5.63/5.88 150. (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (All X, (All Y, (All Z, ((distinct_lines X Y) => ((distinct_lines X Z) \/ (distinct_lines Y Z)))))) (-. (convergent_lines T_1 T_1)) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (-. (convergent_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (All X, (-. (distinct_lines X X))) (convergent_lines T_0 T_1) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (apart_point_and_line (intersection_point T_0 T_1) T_2) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((distinct_lines Y Z) => ((apart_point_and_line X Y) \/ ((apart_point_and_line X Z) \/ (convergent_lines Y Z))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((distinct_lines Y Z) \/ (convergent_lines X Z)))))) ### All 149 % 5.63/5.88 151. (All X, (All Y, (All Z, ((convergent_lines X Y) => ((distinct_lines Y Z) \/ (convergent_lines X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((distinct_lines Y Z) => ((apart_point_and_line X Y) \/ ((apart_point_and_line X Z) \/ (convergent_lines Y Z))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (apart_point_and_line (intersection_point T_0 T_1) T_2) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_0 T_1) (All X, (-. (distinct_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (convergent_lines X X))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((distinct_lines X Y) => ((distinct_lines X Z) \/ (distinct_lines Y Z)))))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) ### All 150 % 5.63/5.88 152. (-. (-. (apart_point_and_line (intersection_point T_0 T_1) T_2))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (All X, (All Y, (All Z, ((distinct_lines X Y) => ((distinct_lines X Z) \/ (distinct_lines Y Z)))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (-. (convergent_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (All X, (-. (distinct_lines X X))) (convergent_lines T_0 T_1) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((distinct_lines Y Z) => ((apart_point_and_line X Y) \/ ((apart_point_and_line X Z) \/ (convergent_lines Y Z))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((distinct_lines Y Z) \/ (convergent_lines X Z)))))) ### NotNot 151 % 5.63/5.88 153. (-. (incident_point_and_line (intersection_point T_0 T_1) T_2)) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((distinct_lines Y Z) \/ (convergent_lines X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((distinct_lines Y Z) => ((apart_point_and_line X Y) \/ ((apart_point_and_line X Z) \/ (convergent_lines Y Z))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_0 T_1) (All X, (-. (distinct_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (convergent_lines X X))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((distinct_lines X Y) => ((distinct_lines X Z) \/ (distinct_lines Y Z)))))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) ### Definition-Pseudo(incident_point_and_line) 152 % 5.72/5.91 154. (apart_point_and_line (intersection_point T_0 T_1) T_3) (-. (apart_point_and_line (intersection_point T_0 T_1) T_3)) ### Axiom % 5.72/5.91 155. (distinct_lines T_3 T_1) (-. (distinct_lines T_3 T_1)) ### Axiom % 5.72/5.91 156. (-. (convergent_lines T_3 T_1)) (convergent_lines T_3 T_1) ### Axiom % 5.72/5.91 157. ((distinct_lines T_3 T_1) => (convergent_lines T_3 T_1)) (-. (convergent_lines T_3 T_1)) (distinct_lines T_3 T_1) ### Imply 155 156 % 5.72/5.91 158. (All Y, ((distinct_lines T_3 Y) => (convergent_lines T_3 Y))) (distinct_lines T_3 T_1) (-. (convergent_lines T_3 T_1)) ### All 157 % 5.72/5.91 159. (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (-. (convergent_lines T_3 T_1)) (distinct_lines T_3 T_1) ### All 158 % 5.72/5.91 160. (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (apart_point_and_line (intersection_point T_0 T_1) T_1) ### Axiom % 5.72/5.91 161. ((apart_point_and_line (intersection_point T_0 T_1) T_3) => ((distinct_lines T_3 T_1) \/ (apart_point_and_line (intersection_point T_0 T_1) T_1))) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (-. (convergent_lines T_3 T_1)) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (apart_point_and_line (intersection_point T_0 T_1) T_3) ### DisjTree 154 159 160 % 5.72/5.91 162. (All Z, ((apart_point_and_line (intersection_point T_0 T_1) T_3) => ((distinct_lines T_3 Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z)))) (apart_point_and_line (intersection_point T_0 T_1) T_3) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (-. (convergent_lines T_3 T_1)) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) ### All 161 % 5.72/5.91 163. (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (apart_point_and_line (intersection_point T_2 T_3) T_1) ### Axiom % 5.72/5.91 164. ((apart_point_and_line (intersection_point T_0 T_1) T_1) => ((distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_3)) \/ (apart_point_and_line (intersection_point T_2 T_3) T_1))) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (convergent_lines T_0 T_1) (All X, (-. (distinct_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All Y, (All Z, ((apart_point_and_line (intersection_point T_0 T_1) Y) => ((distinct_lines Y Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z))))) (All X, (-. (convergent_lines X X))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (-. (convergent_lines T_3 T_1)) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (apart_point_and_line (intersection_point T_0 T_1) T_3) (All Z, ((apart_point_and_line (intersection_point T_0 T_1) T_3) => ((distinct_lines T_3 Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z)))) ### DisjTree 162 45 163 % 5.72/5.91 165. (All Z, ((apart_point_and_line (intersection_point T_0 T_1) T_1) => ((distinct_points (intersection_point T_0 T_1) Z) \/ (apart_point_and_line Z T_1)))) (All Z, ((apart_point_and_line (intersection_point T_0 T_1) T_3) => ((distinct_lines T_3 Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z)))) (apart_point_and_line (intersection_point T_0 T_1) T_3) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (-. (convergent_lines T_3 T_1)) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (-. (convergent_lines X X))) (All Y, (All Z, ((apart_point_and_line (intersection_point T_0 T_1) Y) => ((distinct_lines Y Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z))))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (All X, (-. (distinct_lines X X))) (convergent_lines T_0 T_1) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) ### All 164 % 5.72/5.91 166. (All Y, (All Z, ((apart_point_and_line (intersection_point T_0 T_1) Y) => ((distinct_points (intersection_point T_0 T_1) Z) \/ (apart_point_and_line Z Y))))) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (convergent_lines T_0 T_1) (All X, (-. (distinct_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All Y, (All Z, ((apart_point_and_line (intersection_point T_0 T_1) Y) => ((distinct_lines Y Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z))))) (All X, (-. (convergent_lines X X))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (-. (convergent_lines T_3 T_1)) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (apart_point_and_line (intersection_point T_0 T_1) T_3) (All Z, ((apart_point_and_line (intersection_point T_0 T_1) T_3) => ((distinct_lines T_3 Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z)))) ### All 165 % 5.72/5.91 167. (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All Z, ((apart_point_and_line (intersection_point T_0 T_1) T_3) => ((distinct_lines T_3 Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z)))) (apart_point_and_line (intersection_point T_0 T_1) T_3) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (-. (convergent_lines T_3 T_1)) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (-. (convergent_lines X X))) (All Y, (All Z, ((apart_point_and_line (intersection_point T_0 T_1) Y) => ((distinct_lines Y Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z))))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (All X, (-. (distinct_lines X X))) (convergent_lines T_0 T_1) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) ### All 166 % 5.72/5.93 168. (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (convergent_lines T_0 T_1) (All X, (-. (distinct_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All Y, (All Z, ((apart_point_and_line (intersection_point T_0 T_1) Y) => ((distinct_lines Y Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z))))) (All X, (-. (convergent_lines X X))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (-. (convergent_lines T_3 T_1)) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (apart_point_and_line (intersection_point T_0 T_1) T_3) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) ### All 167 % 5.72/5.93 169. (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (apart_point_and_line (intersection_point T_0 T_1) T_3) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (-. (convergent_lines T_3 T_1)) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (-. (convergent_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (All X, (-. (distinct_lines X X))) (convergent_lines T_0 T_1) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) ### All 168 % 5.72/5.93 170. (All Y, (All Z, ((convergent_lines T_0 Y) => ((distinct_lines Y Z) \/ (convergent_lines T_0 Z))))) (convergent_lines T_0 T_1) (All X, (-. (distinct_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (convergent_lines X X))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (-. (convergent_lines T_3 T_1)) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (apart_point_and_line (intersection_point T_0 T_1) T_3) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) ### All 169 % 5.72/5.93 171. (All X, (All Y, (All Z, ((convergent_lines X Y) => ((distinct_lines Y Z) \/ (convergent_lines X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (apart_point_and_line (intersection_point T_0 T_1) T_3) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (-. (convergent_lines T_3 T_1)) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (-. (convergent_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (All X, (-. (distinct_lines X X))) (convergent_lines T_0 T_1) ### All 170 % 5.72/5.93 172. (-. (distinct_lines T_1 T_1)) (distinct_lines T_1 T_1) ### Axiom % 5.72/5.93 173. (apart_point_and_line (intersection_point T_0 T_1) T_3) (-. (apart_point_and_line (intersection_point T_0 T_1) T_3)) ### Axiom % 5.72/5.93 174. (convergent_lines T_0 T_1) (-. (convergent_lines T_0 T_1)) ### Axiom % 5.72/5.93 175. (distinct_points (intersection_point T_0 T_1) (intersection_point T_3 T_1)) (-. (distinct_points (intersection_point T_0 T_1) (intersection_point T_3 T_1))) ### Axiom % 5.72/5.93 176. (distinct_lines T_1 T_0) (-. (distinct_lines T_1 T_0)) ### Axiom % 5.72/5.93 177. (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (apart_point_and_line (intersection_point T_0 T_1) T_1) ### Axiom % 5.72/5.93 178. (convergent_lines T_3 T_1) (-. (convergent_lines T_3 T_1)) ### Axiom % 5.72/5.93 179. (apart_point_and_line (intersection_point T_3 T_1) T_1) (-. (apart_point_and_line (intersection_point T_3 T_1) T_1)) ### Axiom % 5.72/5.93 180. ((convergent_lines T_3 T_1) => (-. (apart_point_and_line (intersection_point T_3 T_1) T_1))) (apart_point_and_line (intersection_point T_3 T_1) T_1) (convergent_lines T_3 T_1) ### Imply 178 179 % 5.72/5.93 181. (All Y, ((convergent_lines T_3 Y) => (-. (apart_point_and_line (intersection_point T_3 Y) Y)))) (convergent_lines T_3 T_1) (apart_point_and_line (intersection_point T_3 T_1) T_1) ### All 180 % 5.72/5.93 182. (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (apart_point_and_line (intersection_point T_3 T_1) T_1) (convergent_lines T_3 T_1) ### All 181 % 5.72/5.93 183. (apart_point_and_line (intersection_point T_3 T_1) T_0) (-. (apart_point_and_line (intersection_point T_3 T_1) T_0)) ### Axiom % 5.72/5.93 184. (distinct_points (intersection_point T_3 T_1) (intersection_point T_2 T_3)) (-. (distinct_points (intersection_point T_3 T_1) (intersection_point T_2 T_3))) ### Axiom % 5.72/5.93 185. (distinct_lines T_1 T_3) (-. (distinct_lines T_1 T_3)) ### Axiom % 5.72/5.93 186. (-. (apart_point_and_line (intersection_point T_3 T_1) T_1)) (apart_point_and_line (intersection_point T_3 T_1) T_1) ### Axiom % 5.72/5.93 187. (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (apart_point_and_line (intersection_point T_3 T_1) T_3) ### Axiom % 5.72/5.93 188. (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (apart_point_and_line (intersection_point T_2 T_3) T_1) ### Axiom % 5.72/5.93 189. (convergent_lines T_2 T_3) (-. (convergent_lines T_2 T_3)) ### Axiom % 5.72/5.93 190. (apart_point_and_line (intersection_point T_2 T_3) T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_3)) ### Axiom % 5.72/5.93 191. ((convergent_lines T_2 T_3) => (-. (apart_point_and_line (intersection_point T_2 T_3) T_3))) (apart_point_and_line (intersection_point T_2 T_3) T_3) (convergent_lines T_2 T_3) ### Imply 189 190 % 5.72/5.93 192. (All Y, ((convergent_lines T_2 Y) => (-. (apart_point_and_line (intersection_point T_2 Y) Y)))) (convergent_lines T_2 T_3) (apart_point_and_line (intersection_point T_2 T_3) T_3) ### All 191 % 5.72/5.93 193. (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (apart_point_and_line (intersection_point T_2 T_3) T_3) (convergent_lines T_2 T_3) ### All 192 % 5.72/5.93 194. (((distinct_points (intersection_point T_3 T_1) (intersection_point T_2 T_3)) /\ (distinct_lines T_1 T_3)) => ((apart_point_and_line (intersection_point T_3 T_1) T_1) \/ ((apart_point_and_line (intersection_point T_3 T_1) T_3) \/ ((apart_point_and_line (intersection_point T_2 T_3) T_1) \/ (apart_point_and_line (intersection_point T_2 T_3) T_3))))) (convergent_lines T_2 T_3) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (-. (apart_point_and_line (intersection_point T_3 T_1) T_1)) (distinct_lines T_1 T_3) (distinct_points (intersection_point T_3 T_1) (intersection_point T_2 T_3)) ### DisjTree 184 185 186 187 188 193 % 5.72/5.96 195. (All V, (((distinct_points (intersection_point T_3 T_1) (intersection_point T_2 T_3)) /\ (distinct_lines T_1 V)) => ((apart_point_and_line (intersection_point T_3 T_1) T_1) \/ ((apart_point_and_line (intersection_point T_3 T_1) V) \/ ((apart_point_and_line (intersection_point T_2 T_3) T_1) \/ (apart_point_and_line (intersection_point T_2 T_3) V)))))) (distinct_points (intersection_point T_3 T_1) (intersection_point T_2 T_3)) (distinct_lines T_1 T_3) (-. (apart_point_and_line (intersection_point T_3 T_1) T_1)) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_2 T_3) ### All 194 % 5.72/5.96 196. (All U, (All V, (((distinct_points (intersection_point T_3 T_1) (intersection_point T_2 T_3)) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_3 T_1) U) \/ ((apart_point_and_line (intersection_point T_3 T_1) V) \/ ((apart_point_and_line (intersection_point T_2 T_3) U) \/ (apart_point_and_line (intersection_point T_2 T_3) V))))))) (convergent_lines T_2 T_3) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (-. (apart_point_and_line (intersection_point T_3 T_1) T_1)) (distinct_lines T_1 T_3) (distinct_points (intersection_point T_3 T_1) (intersection_point T_2 T_3)) ### All 195 % 5.72/5.96 197. (All Y, (All U, (All V, (((distinct_points (intersection_point T_3 T_1) Y) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_3 T_1) U) \/ ((apart_point_and_line (intersection_point T_3 T_1) V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V)))))))) (distinct_points (intersection_point T_3 T_1) (intersection_point T_2 T_3)) (distinct_lines T_1 T_3) (-. (apart_point_and_line (intersection_point T_3 T_1) T_1)) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_2 T_3) ### All 196 % 5.72/5.96 198. (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (convergent_lines T_2 T_3) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (-. (apart_point_and_line (intersection_point T_3 T_1) T_1)) (distinct_lines T_1 T_3) (distinct_points (intersection_point T_3 T_1) (intersection_point T_2 T_3)) ### All 197 % 5.72/5.96 199. (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (apart_point_and_line (intersection_point T_2 T_3) T_0) ### Axiom % 5.72/5.96 200. ((apart_point_and_line (intersection_point T_3 T_1) T_0) => ((distinct_points (intersection_point T_3 T_1) (intersection_point T_2 T_3)) \/ (apart_point_and_line (intersection_point T_2 T_3) T_0))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (distinct_lines T_1 T_3) (-. (apart_point_and_line (intersection_point T_3 T_1) T_1)) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_2 T_3) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (apart_point_and_line (intersection_point T_3 T_1) T_0) ### DisjTree 183 198 199 % 5.72/5.96 201. (All Z, ((apart_point_and_line (intersection_point T_3 T_1) T_0) => ((distinct_points (intersection_point T_3 T_1) Z) \/ (apart_point_and_line Z T_0)))) (apart_point_and_line (intersection_point T_3 T_1) T_0) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (convergent_lines T_2 T_3) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (-. (apart_point_and_line (intersection_point T_3 T_1) T_1)) (distinct_lines T_1 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) ### All 200 % 5.72/5.96 202. (distinct_lines T_1 T_1) (-. (distinct_lines T_1 T_1)) ### Axiom % 5.72/5.96 203. (All X, (-. (distinct_lines X X))) (distinct_lines T_1 T_1) ### All 202 % 5.72/5.96 204. ((apart_point_and_line (intersection_point T_3 T_1) T_1) => ((distinct_lines T_1 T_1) \/ (apart_point_and_line (intersection_point T_3 T_1) T_1))) (convergent_lines T_3 T_1) (All X, (-. (distinct_lines X X))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (distinct_lines T_1 T_3) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_2 T_3) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (apart_point_and_line (intersection_point T_3 T_1) T_0) (All Z, ((apart_point_and_line (intersection_point T_3 T_1) T_0) => ((distinct_points (intersection_point T_3 T_1) Z) \/ (apart_point_and_line Z T_0)))) ### DisjTree 201 203 182 % 5.72/5.96 205. (All Z, ((apart_point_and_line (intersection_point T_3 T_1) T_1) => ((distinct_lines T_1 Z) \/ (apart_point_and_line (intersection_point T_3 T_1) Z)))) (All Z, ((apart_point_and_line (intersection_point T_3 T_1) T_0) => ((distinct_points (intersection_point T_3 T_1) Z) \/ (apart_point_and_line Z T_0)))) (apart_point_and_line (intersection_point T_3 T_1) T_0) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (convergent_lines T_2 T_3) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (distinct_lines T_1 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (-. (distinct_lines X X))) (convergent_lines T_3 T_1) ### All 204 % 5.72/5.96 206. (All Y, (All Z, ((apart_point_and_line (intersection_point T_3 T_1) Y) => ((distinct_lines Y Z) \/ (apart_point_and_line (intersection_point T_3 T_1) Z))))) (convergent_lines T_3 T_1) (All X, (-. (distinct_lines X X))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (distinct_lines T_1 T_3) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_2 T_3) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (apart_point_and_line (intersection_point T_3 T_1) T_0) (All Z, ((apart_point_and_line (intersection_point T_3 T_1) T_0) => ((distinct_points (intersection_point T_3 T_1) Z) \/ (apart_point_and_line Z T_0)))) ### All 205 % 5.72/5.97 207. (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All Z, ((apart_point_and_line (intersection_point T_3 T_1) T_0) => ((distinct_points (intersection_point T_3 T_1) Z) \/ (apart_point_and_line Z T_0)))) (apart_point_and_line (intersection_point T_3 T_1) T_0) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (convergent_lines T_2 T_3) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (distinct_lines T_1 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (-. (distinct_lines X X))) (convergent_lines T_3 T_1) ### All 206 % 5.72/5.97 208. (All Y, (All Z, ((apart_point_and_line (intersection_point T_3 T_1) Y) => ((distinct_points (intersection_point T_3 T_1) Z) \/ (apart_point_and_line Z Y))))) (convergent_lines T_3 T_1) (All X, (-. (distinct_lines X X))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (distinct_lines T_1 T_3) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_2 T_3) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (apart_point_and_line (intersection_point T_3 T_1) T_0) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) ### All 207 % 5.72/5.97 209. (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (apart_point_and_line (intersection_point T_3 T_1) T_0) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (convergent_lines T_2 T_3) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (distinct_lines T_1 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (-. (distinct_lines X X))) (convergent_lines T_3 T_1) ### All 208 % 5.72/5.97 210. (((distinct_points (intersection_point T_0 T_1) (intersection_point T_3 T_1)) /\ (distinct_lines T_1 T_0)) => ((apart_point_and_line (intersection_point T_0 T_1) T_1) \/ ((apart_point_and_line (intersection_point T_0 T_1) T_0) \/ ((apart_point_and_line (intersection_point T_3 T_1) T_1) \/ (apart_point_and_line (intersection_point T_3 T_1) T_0))))) (All X, (-. (distinct_lines X X))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (distinct_lines T_1 T_3) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (convergent_lines T_3 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_0 T_1) (All Y, ((convergent_lines T_0 Y) => (-. (apart_point_and_line (intersection_point T_0 Y) T_0)))) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (distinct_lines T_1 T_0) (distinct_points (intersection_point T_0 T_1) (intersection_point T_3 T_1)) ### DisjTree 175 176 177 33 182 209 % 5.72/5.97 211. (All V, (((distinct_points (intersection_point T_0 T_1) (intersection_point T_3 T_1)) /\ (distinct_lines T_1 V)) => ((apart_point_and_line (intersection_point T_0 T_1) T_1) \/ ((apart_point_and_line (intersection_point T_0 T_1) V) \/ ((apart_point_and_line (intersection_point T_3 T_1) T_1) \/ (apart_point_and_line (intersection_point T_3 T_1) V)))))) (distinct_points (intersection_point T_0 T_1) (intersection_point T_3 T_1)) (distinct_lines T_1 T_0) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (All Y, ((convergent_lines T_0 Y) => (-. (apart_point_and_line (intersection_point T_0 Y) T_0)))) (convergent_lines T_0 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_3 T_1) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (distinct_lines T_1 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (-. (distinct_lines X X))) ### All 210 % 5.72/5.97 212. (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (distinct_lines X X))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (distinct_lines T_1 T_3) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (convergent_lines T_3 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_0 T_1) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (distinct_lines T_1 T_0) (distinct_points (intersection_point T_0 T_1) (intersection_point T_3 T_1)) (All V, (((distinct_points (intersection_point T_0 T_1) (intersection_point T_3 T_1)) /\ (distinct_lines T_1 V)) => ((apart_point_and_line (intersection_point T_0 T_1) T_1) \/ ((apart_point_and_line (intersection_point T_0 T_1) V) \/ ((apart_point_and_line (intersection_point T_3 T_1) T_1) \/ (apart_point_and_line (intersection_point T_3 T_1) V)))))) ### All 211 % 5.72/5.97 213. (All U, (All V, (((distinct_points (intersection_point T_0 T_1) (intersection_point T_3 T_1)) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_1) U) \/ ((apart_point_and_line (intersection_point T_0 T_1) V) \/ ((apart_point_and_line (intersection_point T_3 T_1) U) \/ (apart_point_and_line (intersection_point T_3 T_1) V))))))) (distinct_points (intersection_point T_0 T_1) (intersection_point T_3 T_1)) (distinct_lines T_1 T_0) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (convergent_lines T_0 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_3 T_1) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (distinct_lines T_1 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (-. (distinct_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) ### All 212 % 5.84/6.01 214. (-. (convergent_lines T_0 T_0)) (convergent_lines T_0 T_0) ### Axiom % 5.84/6.01 215. ((convergent_lines T_0 T_1) => ((distinct_lines T_1 T_0) \/ (convergent_lines T_0 T_0))) (-. (convergent_lines T_0 T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (distinct_lines X X))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (distinct_lines T_1 T_3) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (convergent_lines T_3 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (distinct_points (intersection_point T_0 T_1) (intersection_point T_3 T_1)) (All U, (All V, (((distinct_points (intersection_point T_0 T_1) (intersection_point T_3 T_1)) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_1) U) \/ ((apart_point_and_line (intersection_point T_0 T_1) V) \/ ((apart_point_and_line (intersection_point T_3 T_1) U) \/ (apart_point_and_line (intersection_point T_3 T_1) V))))))) (convergent_lines T_0 T_1) ### DisjTree 174 213 214 % 5.84/6.01 216. (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (convergent_lines T_0 T_1) (All U, (All V, (((distinct_points (intersection_point T_0 T_1) (intersection_point T_3 T_1)) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_1) U) \/ ((apart_point_and_line (intersection_point T_0 T_1) V) \/ ((apart_point_and_line (intersection_point T_3 T_1) U) \/ (apart_point_and_line (intersection_point T_3 T_1) V))))))) (distinct_points (intersection_point T_0 T_1) (intersection_point T_3 T_1)) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_3 T_1) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (distinct_lines T_1 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (-. (distinct_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (-. (convergent_lines T_0 T_0)) ### All 215 % 5.84/6.01 217. (All X, (-. (convergent_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (distinct_lines X X))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (distinct_lines T_1 T_3) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (convergent_lines T_3 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (distinct_points (intersection_point T_0 T_1) (intersection_point T_3 T_1)) (All U, (All V, (((distinct_points (intersection_point T_0 T_1) (intersection_point T_3 T_1)) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_1) U) \/ ((apart_point_and_line (intersection_point T_0 T_1) V) \/ ((apart_point_and_line (intersection_point T_3 T_1) U) \/ (apart_point_and_line (intersection_point T_3 T_1) V))))))) (convergent_lines T_0 T_1) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) ### All 216 % 5.84/6.01 218. (All Y, (All U, (All V, (((distinct_points (intersection_point T_0 T_1) Y) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_1) U) \/ ((apart_point_and_line (intersection_point T_0 T_1) V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V)))))))) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (convergent_lines T_0 T_1) (distinct_points (intersection_point T_0 T_1) (intersection_point T_3 T_1)) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_3 T_1) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (distinct_lines T_1 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (-. (distinct_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (convergent_lines X X))) ### All 217 % 5.84/6.01 219. ((apart_point_and_line (intersection_point T_0 T_1) T_1) => ((distinct_lines T_1 T_1) \/ (apart_point_and_line (intersection_point T_0 T_1) T_1))) (All X, (-. (convergent_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (distinct_lines X X))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (distinct_lines T_1 T_3) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (convergent_lines T_3 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (distinct_points (intersection_point T_0 T_1) (intersection_point T_3 T_1)) (convergent_lines T_0 T_1) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (All Y, (All U, (All V, (((distinct_points (intersection_point T_0 T_1) Y) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_1) U) \/ ((apart_point_and_line (intersection_point T_0 T_1) V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V)))))))) ### DisjTree 218 203 23 % 5.84/6.02 220. (All Z, ((apart_point_and_line (intersection_point T_0 T_1) T_1) => ((distinct_lines T_1 Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z)))) (All Y, (All U, (All V, (((distinct_points (intersection_point T_0 T_1) Y) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_1) U) \/ ((apart_point_and_line (intersection_point T_0 T_1) V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V)))))))) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (convergent_lines T_0 T_1) (distinct_points (intersection_point T_0 T_1) (intersection_point T_3 T_1)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_3 T_1) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (distinct_lines T_1 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (-. (distinct_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (convergent_lines X X))) ### All 219 % 5.84/6.02 221. (All X, (-. (convergent_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (distinct_lines X X))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (distinct_lines T_1 T_3) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (convergent_lines T_3 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (distinct_points (intersection_point T_0 T_1) (intersection_point T_3 T_1)) (convergent_lines T_0 T_1) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (All Z, ((apart_point_and_line (intersection_point T_0 T_1) T_1) => ((distinct_lines T_1 Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z)))) ### All 220 % 5.84/6.02 222. (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (apart_point_and_line (intersection_point T_3 T_1) T_3) ### Axiom % 5.84/6.02 223. ((apart_point_and_line (intersection_point T_0 T_1) T_3) => ((distinct_points (intersection_point T_0 T_1) (intersection_point T_3 T_1)) \/ (apart_point_and_line (intersection_point T_3 T_1) T_3))) (All Z, ((apart_point_and_line (intersection_point T_0 T_1) T_1) => ((distinct_lines T_1 Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z)))) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (convergent_lines T_0 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_3 T_1) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (distinct_lines T_1 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (-. (distinct_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (convergent_lines X X))) (apart_point_and_line (intersection_point T_0 T_1) T_3) ### DisjTree 173 221 222 % 5.84/6.02 224. (All Z, ((apart_point_and_line (intersection_point T_0 T_1) T_3) => ((distinct_points (intersection_point T_0 T_1) Z) \/ (apart_point_and_line Z T_3)))) (apart_point_and_line (intersection_point T_0 T_1) T_3) (All X, (-. (convergent_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (distinct_lines X X))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (distinct_lines T_1 T_3) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (convergent_lines T_3 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_0 T_1) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (All Z, ((apart_point_and_line (intersection_point T_0 T_1) T_1) => ((distinct_lines T_1 Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z)))) ### All 223 % 5.84/6.02 225. (All Y, (All Z, ((apart_point_and_line (intersection_point T_0 T_1) Y) => ((distinct_points (intersection_point T_0 T_1) Z) \/ (apart_point_and_line Z Y))))) (All Z, ((apart_point_and_line (intersection_point T_0 T_1) T_1) => ((distinct_lines T_1 Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z)))) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (convergent_lines T_0 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_3 T_1) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (distinct_lines T_1 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (-. (distinct_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (convergent_lines X X))) (apart_point_and_line (intersection_point T_0 T_1) T_3) ### All 224 % 5.84/6.04 226. (apart_point_and_line (intersection_point T_0 T_1) T_3) (All X, (-. (convergent_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (distinct_lines X X))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (distinct_lines T_1 T_3) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (convergent_lines T_3 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_0 T_1) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (All Z, ((apart_point_and_line (intersection_point T_0 T_1) T_1) => ((distinct_lines T_1 Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z)))) ### All 225 % 5.84/6.04 227. (All Y, (All Z, ((apart_point_and_line (intersection_point T_0 T_1) Y) => ((distinct_lines Y Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z))))) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (convergent_lines T_0 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_3 T_1) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (distinct_lines T_1 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (-. (distinct_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (convergent_lines X X))) (apart_point_and_line (intersection_point T_0 T_1) T_3) ### All 226 % 5.84/6.04 228. (apart_point_and_line (intersection_point T_0 T_1) T_3) (All X, (-. (convergent_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (distinct_lines X X))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (distinct_lines T_1 T_3) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (convergent_lines T_3 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_0 T_1) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) ### All 227 % 5.84/6.04 229. ((convergent_lines T_3 T_1) => ((distinct_lines T_1 T_1) \/ (convergent_lines T_3 T_1))) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (convergent_lines T_0 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (distinct_lines T_1 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (-. (distinct_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (convergent_lines X X))) (-. (distinct_lines T_1 T_1)) (apart_point_and_line (intersection_point T_0 T_1) T_3) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) ((apart_point_and_line (intersection_point T_0 T_1) T_3) => ((distinct_lines T_3 T_1) \/ (apart_point_and_line (intersection_point T_0 T_1) T_1))) ### DisjTree 161 172 228 % 5.84/6.04 230. (All Z, ((convergent_lines T_3 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_3 Z)))) ((apart_point_and_line (intersection_point T_0 T_1) T_3) => ((distinct_lines T_3 T_1) \/ (apart_point_and_line (intersection_point T_0 T_1) T_1))) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (apart_point_and_line (intersection_point T_0 T_1) T_3) (-. (distinct_lines T_1 T_1)) (All X, (-. (convergent_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (distinct_lines X X))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (distinct_lines T_1 T_3) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_0 T_1) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) ### All 229 % 5.84/6.04 231. (-. (convergent_lines T_3 T_3)) (convergent_lines T_3 T_3) ### Axiom % 5.84/6.04 232. ((convergent_lines T_3 T_1) => ((distinct_lines T_1 T_3) \/ (convergent_lines T_3 T_3))) (-. (convergent_lines T_3 T_3)) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (convergent_lines T_0 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (-. (distinct_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (convergent_lines X X))) (-. (distinct_lines T_1 T_1)) (All Z, ((convergent_lines T_3 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_3 Z)))) (apart_point_and_line (intersection_point T_0 T_1) T_3) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) ((apart_point_and_line (intersection_point T_0 T_1) T_3) => ((distinct_lines T_3 T_1) \/ (apart_point_and_line (intersection_point T_0 T_1) T_1))) ### DisjTree 161 230 231 % 5.84/6.07 233. ((apart_point_and_line (intersection_point T_0 T_1) T_3) => ((distinct_lines T_3 T_1) \/ (apart_point_and_line (intersection_point T_0 T_1) T_1))) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (apart_point_and_line (intersection_point T_0 T_1) T_3) (All Z, ((convergent_lines T_3 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_3 Z)))) (-. (distinct_lines T_1 T_1)) (All X, (-. (convergent_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (distinct_lines X X))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_0 T_1) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (-. (convergent_lines T_3 T_3)) ### All 232 % 5.84/6.07 234. (All Y, (All Z, ((convergent_lines T_3 Y) => ((distinct_lines Y Z) \/ (convergent_lines T_3 Z))))) (-. (convergent_lines T_3 T_3)) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (convergent_lines T_0 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (-. (distinct_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (convergent_lines X X))) (-. (distinct_lines T_1 T_1)) (apart_point_and_line (intersection_point T_0 T_1) T_3) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) ((apart_point_and_line (intersection_point T_0 T_1) T_3) => ((distinct_lines T_3 T_1) \/ (apart_point_and_line (intersection_point T_0 T_1) T_1))) ### All 233 % 5.84/6.07 235. ((apart_point_and_line (intersection_point T_0 T_1) T_3) => ((distinct_lines T_3 T_1) \/ (apart_point_and_line (intersection_point T_0 T_1) T_1))) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (apart_point_and_line (intersection_point T_0 T_1) T_3) (All X, (-. (convergent_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (distinct_lines X X))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_0 T_1) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (-. (convergent_lines T_3 T_3)) (All Y, (All Z, ((convergent_lines T_3 Y) => ((distinct_lines Y Z) \/ (convergent_lines T_3 Z))))) ### All 234 % 5.84/6.07 236. (All Z, ((apart_point_and_line (intersection_point T_0 T_1) T_3) => ((distinct_lines T_3 Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z)))) (All Y, (All Z, ((convergent_lines T_3 Y) => ((distinct_lines Y Z) \/ (convergent_lines T_3 Z))))) (-. (convergent_lines T_3 T_3)) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (convergent_lines T_0 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (-. (distinct_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (convergent_lines X X))) (apart_point_and_line (intersection_point T_0 T_1) T_3) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) ### All 235 % 5.84/6.07 237. (All X, (All Y, (All Z, ((convergent_lines X Y) => ((distinct_lines Y Z) \/ (convergent_lines X Z)))))) (-. (apart_point_and_line (intersection_point T_0 T_1) T_1)) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (apart_point_and_line (intersection_point T_0 T_1) T_3) (All X, (-. (convergent_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (distinct_lines X X))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_0 T_1) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (-. (convergent_lines T_3 T_3)) (All Z, ((apart_point_and_line (intersection_point T_0 T_1) T_3) => ((distinct_lines T_3 Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z)))) ### All 236 % 5.84/6.08 238. (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (apart_point_and_line (intersection_point T_2 T_3) T_1) ### Axiom % 5.84/6.08 239. ((apart_point_and_line (intersection_point T_0 T_1) T_1) => ((distinct_points (intersection_point T_0 T_1) (intersection_point T_2 T_3)) \/ (apart_point_and_line (intersection_point T_2 T_3) T_1))) (All Y, (All Z, ((apart_point_and_line (intersection_point T_0 T_1) Y) => ((distinct_lines Y Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z))))) (All Z, ((apart_point_and_line (intersection_point T_0 T_1) T_3) => ((distinct_lines T_3 Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z)))) (-. (convergent_lines T_3 T_3)) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (convergent_lines T_0 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (-. (distinct_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (convergent_lines X X))) (apart_point_and_line (intersection_point T_0 T_1) T_3) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((distinct_lines Y Z) \/ (convergent_lines X Z)))))) ### DisjTree 237 45 238 % 5.84/6.08 240. (All Z, ((apart_point_and_line (intersection_point T_0 T_1) T_1) => ((distinct_points (intersection_point T_0 T_1) Z) \/ (apart_point_and_line Z T_1)))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((distinct_lines Y Z) \/ (convergent_lines X Z)))))) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (apart_point_and_line (intersection_point T_0 T_1) T_3) (All X, (-. (convergent_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (distinct_lines X X))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_0 T_1) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (-. (convergent_lines T_3 T_3)) (All Z, ((apart_point_and_line (intersection_point T_0 T_1) T_3) => ((distinct_lines T_3 Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z)))) (All Y, (All Z, ((apart_point_and_line (intersection_point T_0 T_1) Y) => ((distinct_lines Y Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z))))) ### All 239 % 5.84/6.08 241. (All Y, (All Z, ((apart_point_and_line (intersection_point T_0 T_1) Y) => ((distinct_points (intersection_point T_0 T_1) Z) \/ (apart_point_and_line Z Y))))) (All Y, (All Z, ((apart_point_and_line (intersection_point T_0 T_1) Y) => ((distinct_lines Y Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z))))) (All Z, ((apart_point_and_line (intersection_point T_0 T_1) T_3) => ((distinct_lines T_3 Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z)))) (-. (convergent_lines T_3 T_3)) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (convergent_lines T_0 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (-. (distinct_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (convergent_lines X X))) (apart_point_and_line (intersection_point T_0 T_1) T_3) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((distinct_lines Y Z) \/ (convergent_lines X Z)))))) ### All 240 % 5.84/6.08 242. (All X, (All Y, (All Z, ((convergent_lines X Y) => ((distinct_lines Y Z) \/ (convergent_lines X Z)))))) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (apart_point_and_line (intersection_point T_0 T_1) T_3) (All X, (-. (convergent_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (distinct_lines X X))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_0 T_1) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (-. (convergent_lines T_3 T_3)) (All Z, ((apart_point_and_line (intersection_point T_0 T_1) T_3) => ((distinct_lines T_3 Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z)))) (All Y, (All Z, ((apart_point_and_line (intersection_point T_0 T_1) Y) => ((distinct_lines Y Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z))))) ### All 241 % 5.84/6.08 243. (All Y, (All Z, ((apart_point_and_line (intersection_point T_0 T_1) Y) => ((distinct_lines Y Z) \/ (apart_point_and_line (intersection_point T_0 T_1) Z))))) (-. (convergent_lines T_3 T_3)) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (convergent_lines T_0 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (-. (distinct_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (convergent_lines X X))) (apart_point_and_line (intersection_point T_0 T_1) T_3) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((distinct_lines Y Z) \/ (convergent_lines X Z)))))) ### All 242 % 5.84/6.08 244. (All X, (All Y, (All Z, ((convergent_lines X Y) => ((distinct_lines Y Z) \/ (convergent_lines X Z)))))) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (apart_point_and_line (intersection_point T_0 T_1) T_3) (All X, (-. (convergent_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (distinct_lines X X))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_0 T_1) (All Z, ((convergent_lines T_0 T_1) => ((distinct_lines T_1 Z) \/ (convergent_lines T_0 Z)))) (-. (convergent_lines T_3 T_3)) ### All 243 % 5.84/6.08 245. (All Y, (All Z, ((convergent_lines T_0 Y) => ((distinct_lines Y Z) \/ (convergent_lines T_0 Z))))) (-. (convergent_lines T_3 T_3)) (convergent_lines T_0 T_1) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (convergent_lines T_2 T_3) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (-. (distinct_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (convergent_lines X X))) (apart_point_and_line (intersection_point T_0 T_1) T_3) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((distinct_lines Y Z) \/ (convergent_lines X Z)))))) ### All 244 % 5.84/6.08 246. (All X, (All Y, (All Z, ((convergent_lines X Y) => ((distinct_lines Y Z) \/ (convergent_lines X Z)))))) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (apart_point_and_line (intersection_point T_0 T_1) T_3) (All X, (-. (convergent_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (distinct_lines X X))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (-. (apart_point_and_line (intersection_point T_3 T_1) T_3)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (convergent_lines T_0 T_1) (-. (convergent_lines T_3 T_3)) ### All 245 % 5.84/6.08 247. ((convergent_lines T_3 T_1) => (-. (apart_point_and_line (intersection_point T_3 T_1) T_3))) (-. (convergent_lines T_3 T_3)) (convergent_lines T_2 T_3) (convergent_lines T_0 T_1) (All X, (-. (distinct_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (convergent_lines X X))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (apart_point_and_line (intersection_point T_0 T_1) T_3) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((distinct_lines Y Z) \/ (convergent_lines X Z)))))) ### Imply 171 246 % 5.84/6.08 248. (All Y, ((convergent_lines T_3 Y) => (-. (apart_point_and_line (intersection_point T_3 Y) T_3)))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((distinct_lines Y Z) \/ (convergent_lines X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (apart_point_and_line (intersection_point T_0 T_1) T_3) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (-. (convergent_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (All X, (-. (distinct_lines X X))) (convergent_lines T_0 T_1) (convergent_lines T_2 T_3) (-. (convergent_lines T_3 T_3)) ### All 247 % 5.84/6.08 249. (-. (convergent_lines T_3 T_3)) (convergent_lines T_2 T_3) (convergent_lines T_0 T_1) (All X, (-. (distinct_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (convergent_lines X X))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (apart_point_and_line (intersection_point T_0 T_1) T_3) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((distinct_lines Y Z) \/ (convergent_lines X Z)))))) ### All 248 % 5.93/6.11 250. (All X, (All Y, (All Z, ((convergent_lines X Y) => ((distinct_lines Y Z) \/ (convergent_lines X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (apart_point_and_line (intersection_point T_0 T_1) T_3) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (-. (convergent_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (All X, (-. (distinct_lines X X))) (convergent_lines T_0 T_1) (convergent_lines T_2 T_3) ### All 249 % 5.93/6.11 251. (-. (-. (apart_point_and_line (intersection_point T_0 T_1) T_3))) (convergent_lines T_2 T_3) (convergent_lines T_0 T_1) (All X, (-. (distinct_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (convergent_lines X X))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((distinct_lines Y Z) \/ (convergent_lines X Z)))))) ### NotNot 250 % 5.93/6.11 252. (-. (incident_point_and_line (intersection_point T_0 T_1) T_3)) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((distinct_lines Y Z) \/ (convergent_lines X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (-. (convergent_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (All X, (-. (distinct_lines X X))) (convergent_lines T_0 T_1) (convergent_lines T_2 T_3) ### Definition-Pseudo(incident_point_and_line) 251 % 5.93/6.11 253. (-. ((incident_point_and_line (intersection_point T_0 T_1) T_2) /\ (incident_point_and_line (intersection_point T_0 T_1) T_3))) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (All X, (All Y, (All Z, ((distinct_lines X Y) => ((distinct_lines X Z) \/ (distinct_lines Y Z)))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (-. (convergent_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (All X, (-. (distinct_lines X X))) (convergent_lines T_0 T_1) (-. (apart_point_and_line (intersection_point T_2 T_3) T_1)) (convergent_lines T_2 T_3) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((distinct_lines Y Z) => ((apart_point_and_line X Y) \/ ((apart_point_and_line X Z) \/ (convergent_lines Y Z))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((distinct_lines Y Z) \/ (convergent_lines X Z)))))) ### NotAnd 153 252 % 5.93/6.11 254. (incident_point_and_line (intersection_point T_2 T_3) T_1) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((distinct_lines Y Z) \/ (convergent_lines X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((distinct_lines Y Z) => ((apart_point_and_line X Y) \/ ((apart_point_and_line X Z) \/ (convergent_lines Y Z))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (convergent_lines T_2 T_3) (convergent_lines T_0 T_1) (All X, (-. (distinct_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (-. (apart_point_and_line (intersection_point T_2 T_3) T_0)) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (convergent_lines X X))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((distinct_lines X Y) => ((distinct_lines X Z) \/ (distinct_lines Y Z)))))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (-. ((incident_point_and_line (intersection_point T_0 T_1) T_2) /\ (incident_point_and_line (intersection_point T_0 T_1) T_3))) ### Definition-Pseudo(incident_point_and_line) 253 % 5.93/6.11 255. (incident_point_and_line (intersection_point T_2 T_3) T_0) (-. ((incident_point_and_line (intersection_point T_0 T_1) T_2) /\ (incident_point_and_line (intersection_point T_0 T_1) T_3))) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (All X, (All Y, (All Z, ((distinct_lines X Y) => ((distinct_lines X Z) \/ (distinct_lines Y Z)))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (-. (convergent_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (All X, (-. (distinct_lines X X))) (convergent_lines T_0 T_1) (convergent_lines T_2 T_3) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((distinct_lines Y Z) => ((apart_point_and_line X Y) \/ ((apart_point_and_line X Z) \/ (convergent_lines Y Z))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((distinct_lines Y Z) \/ (convergent_lines X Z)))))) (incident_point_and_line (intersection_point T_2 T_3) T_1) ### Definition-Pseudo(incident_point_and_line) 254 % 5.93/6.11 256. (-. (((convergent_lines T_2 T_3) /\ ((convergent_lines T_0 T_1) /\ ((incident_point_and_line (intersection_point T_2 T_3) T_0) /\ (incident_point_and_line (intersection_point T_2 T_3) T_1)))) => ((incident_point_and_line (intersection_point T_0 T_1) T_2) /\ (incident_point_and_line (intersection_point T_0 T_1) T_3)))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((distinct_lines Y Z) \/ (convergent_lines X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((distinct_lines Y Z) => ((apart_point_and_line X Y) \/ ((apart_point_and_line X Z) \/ (convergent_lines Y Z))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (-. (distinct_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (convergent_lines X X))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((distinct_lines X Y) => ((distinct_lines X Z) \/ (distinct_lines Y Z)))))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) ### ConjTree 255 % 5.93/6.11 257. (-. (All V, (((convergent_lines T_2 T_3) /\ ((convergent_lines T_0 V) /\ ((incident_point_and_line (intersection_point T_2 T_3) T_0) /\ (incident_point_and_line (intersection_point T_2 T_3) V)))) => ((incident_point_and_line (intersection_point T_0 V) T_2) /\ (incident_point_and_line (intersection_point T_0 V) T_3))))) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (All X, (All Y, (All Z, ((distinct_lines X Y) => ((distinct_lines X Z) \/ (distinct_lines Y Z)))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (-. (convergent_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (All X, (-. (distinct_lines X X))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((distinct_lines Y Z) => ((apart_point_and_line X Y) \/ ((apart_point_and_line X Z) \/ (convergent_lines Y Z))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((distinct_lines Y Z) \/ (convergent_lines X Z)))))) ### NotAllEx 256 % 5.93/6.11 258. (-. (All U, (All V, (((convergent_lines T_2 T_3) /\ ((convergent_lines U V) /\ ((incident_point_and_line (intersection_point T_2 T_3) U) /\ (incident_point_and_line (intersection_point T_2 T_3) V)))) => ((incident_point_and_line (intersection_point U V) T_2) /\ (incident_point_and_line (intersection_point U V) T_3)))))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((distinct_lines Y Z) \/ (convergent_lines X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((distinct_lines Y Z) => ((apart_point_and_line X Y) \/ ((apart_point_and_line X Z) \/ (convergent_lines Y Z))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (-. (distinct_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (convergent_lines X X))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((distinct_lines X Y) => ((distinct_lines X Z) \/ (distinct_lines Y Z)))))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) ### NotAllEx 257 % 5.93/6.11 259. (-. (All Y, (All U, (All V, (((convergent_lines T_2 Y) /\ ((convergent_lines U V) /\ ((incident_point_and_line (intersection_point T_2 Y) U) /\ (incident_point_and_line (intersection_point T_2 Y) V)))) => ((incident_point_and_line (intersection_point U V) T_2) /\ (incident_point_and_line (intersection_point U V) Y))))))) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (All X, (All Y, (All Z, ((distinct_lines X Y) => ((distinct_lines X Z) \/ (distinct_lines Y Z)))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (-. (convergent_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (All X, (-. (distinct_lines X X))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (All Y, (All Z, ((distinct_lines Y Z) => ((apart_point_and_line X Y) \/ ((apart_point_and_line X Z) \/ (convergent_lines Y Z))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((distinct_lines Y Z) \/ (convergent_lines X Z)))))) ### NotAllEx 258 % 5.93/6.11 260. (-. (All X, (All Y, (All U, (All V, (((convergent_lines X Y) /\ ((convergent_lines U V) /\ ((incident_point_and_line (intersection_point X Y) U) /\ (incident_point_and_line (intersection_point X Y) V)))) => ((incident_point_and_line (intersection_point U V) X) /\ (incident_point_and_line (intersection_point U V) Y)))))))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((distinct_lines Y Z) \/ (convergent_lines X Z)))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_points X Z) \/ (apart_point_and_line Z Y)))))) (All X, (All Y, (All Z, ((distinct_lines Y Z) => ((apart_point_and_line X Y) \/ ((apart_point_and_line X Z) \/ (convergent_lines Y Z))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All X, (-. (distinct_lines X X))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) Y))))) (All X, (All Y, ((convergent_lines X Y) => (-. (apart_point_and_line (intersection_point X Y) X))))) (All X, (-. (convergent_lines X X))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((distinct_lines X Y) => ((distinct_lines X Z) \/ (distinct_lines Y Z)))))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) ### NotAllEx 259 % 5.93/6.11 % SZS output end Proof % 5.93/6.11 (* END-PROOF *) %------------------------------------------------------------------------------