%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SEU386+1 : TPTP v8.1.0. Released v3.3.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 : Tue Jul 19 14:50:45 EDT 2022 % Result : Theorem 5.02s 5.25s % Output : Proof 5.46s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.09 % Problem : SEU386+1 : TPTP v8.1.0. Released v3.3.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 : Sun Jun 19 08:48:17 EDT 2022 % 0.14/0.29 % CPUTime : % 5.02/5.25 % SZS status Theorem % 5.02/5.25 (* PROOF-FOUND *) % 5.02/5.25 (* BEGIN-PROOF *) % 5.02/5.25 % SZS output start Proof % 5.02/5.25 1. (-. (empty_carrier T_0)) (empty_carrier T_0) ### Axiom % 5.02/5.25 2. (topological_space T_0) (-. (topological_space T_0)) ### Axiom % 5.02/5.25 3. (top_str T_0) (-. (top_str T_0)) ### Axiom % 5.02/5.25 4. (-. (empty_carrier T_1)) (empty_carrier T_1) ### Axiom % 5.02/5.25 5. (net_str T_1 T_0) (-. (net_str T_1 T_0)) ### Axiom % 5.02/5.25 6. (element T_2 (the_carrier T_0)) (-. (element T_2 (the_carrier T_0))) ### Axiom % 5.02/5.25 7. (-. (empty_carrier T_0)) (empty_carrier T_0) ### Axiom % 5.02/5.25 8. (top_str T_0) (-. (top_str T_0)) ### Axiom % 5.02/5.25 9. (-. (one_sorted_str T_0)) (one_sorted_str T_0) ### Axiom % 5.02/5.25 10. ((top_str T_0) => (one_sorted_str T_0)) (-. (one_sorted_str T_0)) (top_str T_0) ### Imply 8 9 % 5.02/5.25 11. (All A, ((top_str A) => (one_sorted_str A))) (top_str T_0) (-. (one_sorted_str T_0)) ### All 10 % 5.02/5.25 12. (-. (empty_carrier T_1)) (empty_carrier T_1) ### Axiom % 5.02/5.25 13. (transitive_relstr T_1) (-. (transitive_relstr T_1)) ### Axiom % 5.02/5.25 14. (directed_relstr T_1) (-. (directed_relstr T_1)) ### Axiom % 5.02/5.25 15. (net_str T_1 T_0) (-. (net_str T_1 T_0)) ### Axiom % 5.02/5.25 16. (-. (empty_carrier T_0)) (empty_carrier T_0) ### Axiom % 5.02/5.25 17. (topological_space T_0) (-. (topological_space T_0)) ### Axiom % 5.02/5.25 18. (top_str T_0) (-. (top_str T_0)) ### Axiom % 5.02/5.25 19. (-. (empty_carrier T_1)) (empty_carrier T_1) ### Axiom % 5.02/5.25 20. (transitive_relstr T_1) (-. (transitive_relstr T_1)) ### Axiom % 5.02/5.25 21. (directed_relstr T_1) (-. (directed_relstr T_1)) ### Axiom % 5.02/5.25 22. (net_str T_1 T_0) (-. (net_str T_1 T_0)) ### Axiom % 5.02/5.25 23. (-. (empty_carrier T_0)) (empty_carrier T_0) ### Axiom % 5.02/5.25 24. (topological_space T_0) (-. (topological_space T_0)) ### Axiom % 5.02/5.25 25. (top_str T_0) (-. (top_str T_0)) ### Axiom % 5.02/5.25 26. (-. (empty_carrier T_1)) (empty_carrier T_1) ### Axiom % 5.02/5.25 27. (transitive_relstr T_1) (-. (transitive_relstr T_1)) ### Axiom % 5.02/5.25 28. (directed_relstr T_1) (-. (directed_relstr T_1)) ### Axiom % 5.02/5.25 29. (net_str T_1 T_0) (-. (net_str T_1 T_0)) ### Axiom % 5.02/5.25 30. (-. (element (lim_points_of_net T_0 T_1) (powerset (the_carrier T_0)))) (element (lim_points_of_net T_0 T_1) (powerset (the_carrier T_0))) ### Axiom % 5.02/5.25 31. (((-. (empty_carrier T_0)) /\ ((topological_space T_0) /\ ((top_str T_0) /\ ((-. (empty_carrier T_1)) /\ ((transitive_relstr T_1) /\ ((directed_relstr T_1) /\ (net_str T_1 T_0))))))) => (element (lim_points_of_net T_0 T_1) (powerset (the_carrier T_0)))) (-. (element (lim_points_of_net T_0 T_1) (powerset (the_carrier T_0)))) (net_str T_1 T_0) (directed_relstr T_1) (transitive_relstr T_1) (-. (empty_carrier T_1)) (top_str T_0) (topological_space T_0) (-. (empty_carrier T_0)) ### DisjTree 23 24 25 26 27 28 29 30 % 5.02/5.25 32. (All B, (((-. (empty_carrier T_0)) /\ ((topological_space T_0) /\ ((top_str T_0) /\ ((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B T_0))))))) => (element (lim_points_of_net T_0 B) (powerset (the_carrier T_0))))) (-. (empty_carrier T_0)) (topological_space T_0) (top_str T_0) (-. (empty_carrier T_1)) (transitive_relstr T_1) (directed_relstr T_1) (net_str T_1 T_0) (-. (element (lim_points_of_net T_0 T_1) (powerset (the_carrier T_0)))) ### All 31 % 5.02/5.25 33. (All A, (All B, (((-. (empty_carrier A)) /\ ((topological_space A) /\ ((top_str A) /\ ((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A))))))) => (element (lim_points_of_net A B) (powerset (the_carrier A)))))) (-. (element (lim_points_of_net T_0 T_1) (powerset (the_carrier T_0)))) (net_str T_1 T_0) (directed_relstr T_1) (transitive_relstr T_1) (-. (empty_carrier T_1)) (top_str T_0) (topological_space T_0) (-. (empty_carrier T_0)) ### All 32 % 5.02/5.25 34. ((lim_points_of_net T_0 T_1) != (lim_points_of_net T_0 T_1)) ### Refl(=) % 5.02/5.25 35. (element T_2 (the_carrier T_0)) (-. (element T_2 (the_carrier T_0))) ### Axiom % 5.02/5.25 36. (in T_2 (lim_points_of_net T_0 T_1)) (-. (in T_2 (lim_points_of_net T_0 T_1))) ### Axiom % 5.02/5.25 37. (point_neighbourhood T_3 T_0 T_2) (-. (point_neighbourhood T_3 T_0 T_2)) ### Axiom % 5.02/5.25 38. (-. (is_eventually_in T_0 T_1 T_3)) (is_eventually_in T_0 T_1 T_3) ### Axiom % 5.02/5.25 39. ((point_neighbourhood T_3 T_0 T_2) => (is_eventually_in T_0 T_1 T_3)) (-. (is_eventually_in T_0 T_1 T_3)) (point_neighbourhood T_3 T_0 T_2) ### Imply 37 38 % 5.02/5.25 40. (All E, ((point_neighbourhood E T_0 T_2) => (is_eventually_in T_0 T_1 E))) (point_neighbourhood T_3 T_0 T_2) (-. (is_eventually_in T_0 T_1 T_3)) ### All 39 % 5.02/5.25 41. ((in T_2 (lim_points_of_net T_0 T_1)) <=> (All E, ((point_neighbourhood E T_0 T_2) => (is_eventually_in T_0 T_1 E)))) (-. (is_eventually_in T_0 T_1 T_3)) (point_neighbourhood T_3 T_0 T_2) (in T_2 (lim_points_of_net T_0 T_1)) ### Equiv 36 40 % 5.02/5.25 42. ((element T_2 (the_carrier T_0)) => ((in T_2 (lim_points_of_net T_0 T_1)) <=> (All E, ((point_neighbourhood E T_0 T_2) => (is_eventually_in T_0 T_1 E))))) (in T_2 (lim_points_of_net T_0 T_1)) (point_neighbourhood T_3 T_0 T_2) (-. (is_eventually_in T_0 T_1 T_3)) (element T_2 (the_carrier T_0)) ### Imply 35 41 % 5.02/5.25 43. (All D, ((element D (the_carrier T_0)) => ((in D (lim_points_of_net T_0 T_1)) <=> (All E, ((point_neighbourhood E T_0 D) => (is_eventually_in T_0 T_1 E)))))) (element T_2 (the_carrier T_0)) (-. (is_eventually_in T_0 T_1 T_3)) (point_neighbourhood T_3 T_0 T_2) (in T_2 (lim_points_of_net T_0 T_1)) ### All 42 % 5.02/5.25 44. (((lim_points_of_net T_0 T_1) = (lim_points_of_net T_0 T_1)) <=> (All D, ((element D (the_carrier T_0)) => ((in D (lim_points_of_net T_0 T_1)) <=> (All E, ((point_neighbourhood E T_0 D) => (is_eventually_in T_0 T_1 E))))))) (in T_2 (lim_points_of_net T_0 T_1)) (point_neighbourhood T_3 T_0 T_2) (-. (is_eventually_in T_0 T_1 T_3)) (element T_2 (the_carrier T_0)) ### Equiv 34 43 % 5.02/5.25 45. ((element (lim_points_of_net T_0 T_1) (powerset (the_carrier T_0))) => (((lim_points_of_net T_0 T_1) = (lim_points_of_net T_0 T_1)) <=> (All D, ((element D (the_carrier T_0)) => ((in D (lim_points_of_net T_0 T_1)) <=> (All E, ((point_neighbourhood E T_0 D) => (is_eventually_in T_0 T_1 E)))))))) (element T_2 (the_carrier T_0)) (-. (is_eventually_in T_0 T_1 T_3)) (point_neighbourhood T_3 T_0 T_2) (in T_2 (lim_points_of_net T_0 T_1)) (-. (empty_carrier T_0)) (topological_space T_0) (top_str T_0) (-. (empty_carrier T_1)) (transitive_relstr T_1) (directed_relstr T_1) (net_str T_1 T_0) (All A, (All B, (((-. (empty_carrier A)) /\ ((topological_space A) /\ ((top_str A) /\ ((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A))))))) => (element (lim_points_of_net A B) (powerset (the_carrier A)))))) ### Imply 33 44 % 5.02/5.25 46. (All C, ((element C (powerset (the_carrier T_0))) => ((C = (lim_points_of_net T_0 T_1)) <=> (All D, ((element D (the_carrier T_0)) => ((in D C) <=> (All E, ((point_neighbourhood E T_0 D) => (is_eventually_in T_0 T_1 E))))))))) (All A, (All B, (((-. (empty_carrier A)) /\ ((topological_space A) /\ ((top_str A) /\ ((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A))))))) => (element (lim_points_of_net A B) (powerset (the_carrier A)))))) (net_str T_1 T_0) (directed_relstr T_1) (transitive_relstr T_1) (-. (empty_carrier T_1)) (top_str T_0) (topological_space T_0) (-. (empty_carrier T_0)) (in T_2 (lim_points_of_net T_0 T_1)) (point_neighbourhood T_3 T_0 T_2) (-. (is_eventually_in T_0 T_1 T_3)) (element T_2 (the_carrier T_0)) ### All 45 % 5.02/5.25 47. (((-. (empty_carrier T_1)) /\ ((transitive_relstr T_1) /\ ((directed_relstr T_1) /\ (net_str T_1 T_0)))) => (All C, ((element C (powerset (the_carrier T_0))) => ((C = (lim_points_of_net T_0 T_1)) <=> (All D, ((element D (the_carrier T_0)) => ((in D C) <=> (All E, ((point_neighbourhood E T_0 D) => (is_eventually_in T_0 T_1 E)))))))))) (element T_2 (the_carrier T_0)) (-. (is_eventually_in T_0 T_1 T_3)) (point_neighbourhood T_3 T_0 T_2) (in T_2 (lim_points_of_net T_0 T_1)) (-. (empty_carrier T_0)) (topological_space T_0) (top_str T_0) (All A, (All B, (((-. (empty_carrier A)) /\ ((topological_space A) /\ ((top_str A) /\ ((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A))))))) => (element (lim_points_of_net A B) (powerset (the_carrier A)))))) (net_str T_1 T_0) (directed_relstr T_1) (transitive_relstr T_1) (-. (empty_carrier T_1)) ### DisjTree 19 20 21 22 46 % 5.02/5.25 48. (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B T_0)))) => (All C, ((element C (powerset (the_carrier T_0))) => ((C = (lim_points_of_net T_0 B)) <=> (All D, ((element D (the_carrier T_0)) => ((in D C) <=> (All E, ((point_neighbourhood E T_0 D) => (is_eventually_in T_0 B E))))))))))) (-. (empty_carrier T_1)) (transitive_relstr T_1) (directed_relstr T_1) (net_str T_1 T_0) (All A, (All B, (((-. (empty_carrier A)) /\ ((topological_space A) /\ ((top_str A) /\ ((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A))))))) => (element (lim_points_of_net A B) (powerset (the_carrier A)))))) (top_str T_0) (topological_space T_0) (-. (empty_carrier T_0)) (in T_2 (lim_points_of_net T_0 T_1)) (point_neighbourhood T_3 T_0 T_2) (-. (is_eventually_in T_0 T_1 T_3)) (element T_2 (the_carrier T_0)) ### All 47 % 5.46/5.65 49. (((-. (empty_carrier T_0)) /\ ((topological_space T_0) /\ (top_str T_0))) => (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B T_0)))) => (All C, ((element C (powerset (the_carrier T_0))) => ((C = (lim_points_of_net T_0 B)) <=> (All D, ((element D (the_carrier T_0)) => ((in D C) <=> (All E, ((point_neighbourhood E T_0 D) => (is_eventually_in T_0 B E)))))))))))) (element T_2 (the_carrier T_0)) (-. (is_eventually_in T_0 T_1 T_3)) (point_neighbourhood T_3 T_0 T_2) (in T_2 (lim_points_of_net T_0 T_1)) (All A, (All B, (((-. (empty_carrier A)) /\ ((topological_space A) /\ ((top_str A) /\ ((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A))))))) => (element (lim_points_of_net A B) (powerset (the_carrier A)))))) (net_str T_1 T_0) (directed_relstr T_1) (transitive_relstr T_1) (-. (empty_carrier T_1)) (top_str T_0) (topological_space T_0) (-. (empty_carrier T_0)) ### DisjTree 16 17 18 48 % 5.46/5.65 50. (All A, (((-. (empty_carrier A)) /\ ((topological_space A) /\ (top_str A))) => (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A)))) => (All C, ((element C (powerset (the_carrier A))) => ((C = (lim_points_of_net A B)) <=> (All D, ((element D (the_carrier A)) => ((in D C) <=> (All E, ((point_neighbourhood E A D) => (is_eventually_in A B E))))))))))))) (-. (empty_carrier T_0)) (topological_space T_0) (top_str T_0) (-. (empty_carrier T_1)) (transitive_relstr T_1) (directed_relstr T_1) (net_str T_1 T_0) (All A, (All B, (((-. (empty_carrier A)) /\ ((topological_space A) /\ ((top_str A) /\ ((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A))))))) => (element (lim_points_of_net A B) (powerset (the_carrier A)))))) (in T_2 (lim_points_of_net T_0 T_1)) (point_neighbourhood T_3 T_0 T_2) (-. (is_eventually_in T_0 T_1 T_3)) (element T_2 (the_carrier T_0)) ### All 49 % 5.46/5.65 51. (-. (is_often_in T_0 T_1 T_3)) (is_often_in T_0 T_1 T_3) ### Axiom % 5.46/5.65 52. ((is_eventually_in T_0 T_1 T_3) => (is_often_in T_0 T_1 T_3)) (-. (is_often_in T_0 T_1 T_3)) (element T_2 (the_carrier T_0)) (point_neighbourhood T_3 T_0 T_2) (in T_2 (lim_points_of_net T_0 T_1)) (All A, (All B, (((-. (empty_carrier A)) /\ ((topological_space A) /\ ((top_str A) /\ ((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A))))))) => (element (lim_points_of_net A B) (powerset (the_carrier A)))))) (net_str T_1 T_0) (directed_relstr T_1) (transitive_relstr T_1) (-. (empty_carrier T_1)) (top_str T_0) (topological_space T_0) (-. (empty_carrier T_0)) (All A, (((-. (empty_carrier A)) /\ ((topological_space A) /\ (top_str A))) => (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A)))) => (All C, ((element C (powerset (the_carrier A))) => ((C = (lim_points_of_net A B)) <=> (All D, ((element D (the_carrier A)) => ((in D C) <=> (All E, ((point_neighbourhood E A D) => (is_eventually_in A B E))))))))))))) ### Imply 50 51 % 5.46/5.65 53. (All C, ((is_eventually_in T_0 T_1 C) => (is_often_in T_0 T_1 C))) (All A, (((-. (empty_carrier A)) /\ ((topological_space A) /\ (top_str A))) => (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A)))) => (All C, ((element C (powerset (the_carrier A))) => ((C = (lim_points_of_net A B)) <=> (All D, ((element D (the_carrier A)) => ((in D C) <=> (All E, ((point_neighbourhood E A D) => (is_eventually_in A B E))))))))))))) (-. (empty_carrier T_0)) (topological_space T_0) (top_str T_0) (-. (empty_carrier T_1)) (transitive_relstr T_1) (directed_relstr T_1) (net_str T_1 T_0) (All A, (All B, (((-. (empty_carrier A)) /\ ((topological_space A) /\ ((top_str A) /\ ((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A))))))) => (element (lim_points_of_net A B) (powerset (the_carrier A)))))) (in T_2 (lim_points_of_net T_0 T_1)) (point_neighbourhood T_3 T_0 T_2) (element T_2 (the_carrier T_0)) (-. (is_often_in T_0 T_1 T_3)) ### All 52 % 5.46/5.65 54. (((-. (empty_carrier T_1)) /\ ((transitive_relstr T_1) /\ ((directed_relstr T_1) /\ (net_str T_1 T_0)))) => (All C, ((is_eventually_in T_0 T_1 C) => (is_often_in T_0 T_1 C)))) (-. (is_often_in T_0 T_1 T_3)) (element T_2 (the_carrier T_0)) (point_neighbourhood T_3 T_0 T_2) (in T_2 (lim_points_of_net T_0 T_1)) (All A, (All B, (((-. (empty_carrier A)) /\ ((topological_space A) /\ ((top_str A) /\ ((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A))))))) => (element (lim_points_of_net A B) (powerset (the_carrier A)))))) (top_str T_0) (topological_space T_0) (-. (empty_carrier T_0)) (All A, (((-. (empty_carrier A)) /\ ((topological_space A) /\ (top_str A))) => (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A)))) => (All C, ((element C (powerset (the_carrier A))) => ((C = (lim_points_of_net A B)) <=> (All D, ((element D (the_carrier A)) => ((in D C) <=> (All E, ((point_neighbourhood E A D) => (is_eventually_in A B E))))))))))))) (net_str T_1 T_0) (directed_relstr T_1) (transitive_relstr T_1) (-. (empty_carrier T_1)) ### DisjTree 12 13 14 15 53 % 5.46/5.65 55. (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B T_0)))) => (All C, ((is_eventually_in T_0 B C) => (is_often_in T_0 B C))))) (-. (empty_carrier T_1)) (transitive_relstr T_1) (directed_relstr T_1) (net_str T_1 T_0) (All A, (((-. (empty_carrier A)) /\ ((topological_space A) /\ (top_str A))) => (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A)))) => (All C, ((element C (powerset (the_carrier A))) => ((C = (lim_points_of_net A B)) <=> (All D, ((element D (the_carrier A)) => ((in D C) <=> (All E, ((point_neighbourhood E A D) => (is_eventually_in A B E))))))))))))) (-. (empty_carrier T_0)) (topological_space T_0) (top_str T_0) (All A, (All B, (((-. (empty_carrier A)) /\ ((topological_space A) /\ ((top_str A) /\ ((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A))))))) => (element (lim_points_of_net A B) (powerset (the_carrier A)))))) (in T_2 (lim_points_of_net T_0 T_1)) (point_neighbourhood T_3 T_0 T_2) (element T_2 (the_carrier T_0)) (-. (is_often_in T_0 T_1 T_3)) ### All 54 % 5.46/5.65 56. (((-. (empty_carrier T_0)) /\ (one_sorted_str T_0)) => (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B T_0)))) => (All C, ((is_eventually_in T_0 B C) => (is_often_in T_0 B C)))))) (-. (is_often_in T_0 T_1 T_3)) (element T_2 (the_carrier T_0)) (point_neighbourhood T_3 T_0 T_2) (in T_2 (lim_points_of_net T_0 T_1)) (All A, (All B, (((-. (empty_carrier A)) /\ ((topological_space A) /\ ((top_str A) /\ ((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A))))))) => (element (lim_points_of_net A B) (powerset (the_carrier A)))))) (topological_space T_0) (All A, (((-. (empty_carrier A)) /\ ((topological_space A) /\ (top_str A))) => (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A)))) => (All C, ((element C (powerset (the_carrier A))) => ((C = (lim_points_of_net A B)) <=> (All D, ((element D (the_carrier A)) => ((in D C) <=> (All E, ((point_neighbourhood E A D) => (is_eventually_in A B E))))))))))))) (net_str T_1 T_0) (directed_relstr T_1) (transitive_relstr T_1) (-. (empty_carrier T_1)) (top_str T_0) (All A, ((top_str A) => (one_sorted_str A))) (-. (empty_carrier T_0)) ### DisjTree 7 11 55 % 5.46/5.69 57. (All A, (((-. (empty_carrier A)) /\ (one_sorted_str A)) => (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A)))) => (All C, ((is_eventually_in A B C) => (is_often_in A B C))))))) (-. (empty_carrier T_0)) (All A, ((top_str A) => (one_sorted_str A))) (top_str T_0) (-. (empty_carrier T_1)) (transitive_relstr T_1) (directed_relstr T_1) (net_str T_1 T_0) (All A, (((-. (empty_carrier A)) /\ ((topological_space A) /\ (top_str A))) => (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A)))) => (All C, ((element C (powerset (the_carrier A))) => ((C = (lim_points_of_net A B)) <=> (All D, ((element D (the_carrier A)) => ((in D C) <=> (All E, ((point_neighbourhood E A D) => (is_eventually_in A B E))))))))))))) (topological_space T_0) (All A, (All B, (((-. (empty_carrier A)) /\ ((topological_space A) /\ ((top_str A) /\ ((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A))))))) => (element (lim_points_of_net A B) (powerset (the_carrier A)))))) (in T_2 (lim_points_of_net T_0 T_1)) (point_neighbourhood T_3 T_0 T_2) (element T_2 (the_carrier T_0)) (-. (is_often_in T_0 T_1 T_3)) ### All 56 % 5.46/5.69 58. (-. ((point_neighbourhood T_3 T_0 T_2) => (is_often_in T_0 T_1 T_3))) (element T_2 (the_carrier T_0)) (in T_2 (lim_points_of_net T_0 T_1)) (All A, (All B, (((-. (empty_carrier A)) /\ ((topological_space A) /\ ((top_str A) /\ ((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A))))))) => (element (lim_points_of_net A B) (powerset (the_carrier A)))))) (topological_space T_0) (All A, (((-. (empty_carrier A)) /\ ((topological_space A) /\ (top_str A))) => (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A)))) => (All C, ((element C (powerset (the_carrier A))) => ((C = (lim_points_of_net A B)) <=> (All D, ((element D (the_carrier A)) => ((in D C) <=> (All E, ((point_neighbourhood E A D) => (is_eventually_in A B E))))))))))))) (net_str T_1 T_0) (directed_relstr T_1) (transitive_relstr T_1) (-. (empty_carrier T_1)) (top_str T_0) (All A, ((top_str A) => (one_sorted_str A))) (-. (empty_carrier T_0)) (All A, (((-. (empty_carrier A)) /\ (one_sorted_str A)) => (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A)))) => (All C, ((is_eventually_in A B C) => (is_often_in A B C))))))) ### NotImply 57 % 5.46/5.69 59. (-. (All D, ((point_neighbourhood D T_0 T_2) => (is_often_in T_0 T_1 D)))) (All A, (((-. (empty_carrier A)) /\ (one_sorted_str A)) => (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A)))) => (All C, ((is_eventually_in A B C) => (is_often_in A B C))))))) (-. (empty_carrier T_0)) (All A, ((top_str A) => (one_sorted_str A))) (top_str T_0) (-. (empty_carrier T_1)) (transitive_relstr T_1) (directed_relstr T_1) (net_str T_1 T_0) (All A, (((-. (empty_carrier A)) /\ ((topological_space A) /\ (top_str A))) => (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A)))) => (All C, ((element C (powerset (the_carrier A))) => ((C = (lim_points_of_net A B)) <=> (All D, ((element D (the_carrier A)) => ((in D C) <=> (All E, ((point_neighbourhood E A D) => (is_eventually_in A B E))))))))))))) (topological_space T_0) (All A, (All B, (((-. (empty_carrier A)) /\ ((topological_space A) /\ ((top_str A) /\ ((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A))))))) => (element (lim_points_of_net A B) (powerset (the_carrier A)))))) (in T_2 (lim_points_of_net T_0 T_1)) (element T_2 (the_carrier T_0)) ### NotAllEx 58 % 5.46/5.69 60. (-. (is_a_cluster_point_of_netstr T_0 T_1 T_2)) (is_a_cluster_point_of_netstr T_0 T_1 T_2) ### Axiom % 5.46/5.69 61. ((is_a_cluster_point_of_netstr T_0 T_1 T_2) <=> (All D, ((point_neighbourhood D T_0 T_2) => (is_often_in T_0 T_1 D)))) (-. (is_a_cluster_point_of_netstr T_0 T_1 T_2)) (element T_2 (the_carrier T_0)) (in T_2 (lim_points_of_net T_0 T_1)) (All A, (All B, (((-. (empty_carrier A)) /\ ((topological_space A) /\ ((top_str A) /\ ((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A))))))) => (element (lim_points_of_net A B) (powerset (the_carrier A)))))) (topological_space T_0) (All A, (((-. (empty_carrier A)) /\ ((topological_space A) /\ (top_str A))) => (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A)))) => (All C, ((element C (powerset (the_carrier A))) => ((C = (lim_points_of_net A B)) <=> (All D, ((element D (the_carrier A)) => ((in D C) <=> (All E, ((point_neighbourhood E A D) => (is_eventually_in A B E))))))))))))) (net_str T_1 T_0) (directed_relstr T_1) (transitive_relstr T_1) (-. (empty_carrier T_1)) (top_str T_0) (All A, ((top_str A) => (one_sorted_str A))) (-. (empty_carrier T_0)) (All A, (((-. (empty_carrier A)) /\ (one_sorted_str A)) => (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A)))) => (All C, ((is_eventually_in A B C) => (is_often_in A B C))))))) ### Equiv 59 60 % 5.46/5.69 62. ((element T_2 (the_carrier T_0)) => ((is_a_cluster_point_of_netstr T_0 T_1 T_2) <=> (All D, ((point_neighbourhood D T_0 T_2) => (is_often_in T_0 T_1 D))))) (All A, (((-. (empty_carrier A)) /\ (one_sorted_str A)) => (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A)))) => (All C, ((is_eventually_in A B C) => (is_often_in A B C))))))) (-. (empty_carrier T_0)) (All A, ((top_str A) => (one_sorted_str A))) (top_str T_0) (-. (empty_carrier T_1)) (transitive_relstr T_1) (directed_relstr T_1) (net_str T_1 T_0) (All A, (((-. (empty_carrier A)) /\ ((topological_space A) /\ (top_str A))) => (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A)))) => (All C, ((element C (powerset (the_carrier A))) => ((C = (lim_points_of_net A B)) <=> (All D, ((element D (the_carrier A)) => ((in D C) <=> (All E, ((point_neighbourhood E A D) => (is_eventually_in A B E))))))))))))) (topological_space T_0) (All A, (All B, (((-. (empty_carrier A)) /\ ((topological_space A) /\ ((top_str A) /\ ((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A))))))) => (element (lim_points_of_net A B) (powerset (the_carrier A)))))) (in T_2 (lim_points_of_net T_0 T_1)) (-. (is_a_cluster_point_of_netstr T_0 T_1 T_2)) (element T_2 (the_carrier T_0)) ### Imply 6 61 % 5.46/5.69 63. (All C, ((element C (the_carrier T_0)) => ((is_a_cluster_point_of_netstr T_0 T_1 C) <=> (All D, ((point_neighbourhood D T_0 C) => (is_often_in T_0 T_1 D)))))) (element T_2 (the_carrier T_0)) (-. (is_a_cluster_point_of_netstr T_0 T_1 T_2)) (in T_2 (lim_points_of_net T_0 T_1)) (All A, (All B, (((-. (empty_carrier A)) /\ ((topological_space A) /\ ((top_str A) /\ ((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A))))))) => (element (lim_points_of_net A B) (powerset (the_carrier A)))))) (topological_space T_0) (All A, (((-. (empty_carrier A)) /\ ((topological_space A) /\ (top_str A))) => (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A)))) => (All C, ((element C (powerset (the_carrier A))) => ((C = (lim_points_of_net A B)) <=> (All D, ((element D (the_carrier A)) => ((in D C) <=> (All E, ((point_neighbourhood E A D) => (is_eventually_in A B E))))))))))))) (net_str T_1 T_0) (directed_relstr T_1) (transitive_relstr T_1) (-. (empty_carrier T_1)) (top_str T_0) (All A, ((top_str A) => (one_sorted_str A))) (-. (empty_carrier T_0)) (All A, (((-. (empty_carrier A)) /\ (one_sorted_str A)) => (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A)))) => (All C, ((is_eventually_in A B C) => (is_often_in A B C))))))) ### All 62 % 5.46/5.69 64. (((-. (empty_carrier T_1)) /\ (net_str T_1 T_0)) => (All C, ((element C (the_carrier T_0)) => ((is_a_cluster_point_of_netstr T_0 T_1 C) <=> (All D, ((point_neighbourhood D T_0 C) => (is_often_in T_0 T_1 D))))))) (All A, (((-. (empty_carrier A)) /\ (one_sorted_str A)) => (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A)))) => (All C, ((is_eventually_in A B C) => (is_often_in A B C))))))) (-. (empty_carrier T_0)) (All A, ((top_str A) => (one_sorted_str A))) (top_str T_0) (transitive_relstr T_1) (directed_relstr T_1) (All A, (((-. (empty_carrier A)) /\ ((topological_space A) /\ (top_str A))) => (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A)))) => (All C, ((element C (powerset (the_carrier A))) => ((C = (lim_points_of_net A B)) <=> (All D, ((element D (the_carrier A)) => ((in D C) <=> (All E, ((point_neighbourhood E A D) => (is_eventually_in A B E))))))))))))) (topological_space T_0) (All A, (All B, (((-. (empty_carrier A)) /\ ((topological_space A) /\ ((top_str A) /\ ((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A))))))) => (element (lim_points_of_net A B) (powerset (the_carrier A)))))) (in T_2 (lim_points_of_net T_0 T_1)) (-. (is_a_cluster_point_of_netstr T_0 T_1 T_2)) (element T_2 (the_carrier T_0)) (net_str T_1 T_0) (-. (empty_carrier T_1)) ### DisjTree 4 5 63 % 5.46/5.69 65. (All B, (((-. (empty_carrier B)) /\ (net_str B T_0)) => (All C, ((element C (the_carrier T_0)) => ((is_a_cluster_point_of_netstr T_0 B C) <=> (All D, ((point_neighbourhood D T_0 C) => (is_often_in T_0 B D)))))))) (-. (empty_carrier T_1)) (net_str T_1 T_0) (element T_2 (the_carrier T_0)) (-. (is_a_cluster_point_of_netstr T_0 T_1 T_2)) (in T_2 (lim_points_of_net T_0 T_1)) (All A, (All B, (((-. (empty_carrier A)) /\ ((topological_space A) /\ ((top_str A) /\ ((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A))))))) => (element (lim_points_of_net A B) (powerset (the_carrier A)))))) (topological_space T_0) (All A, (((-. (empty_carrier A)) /\ ((topological_space A) /\ (top_str A))) => (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A)))) => (All C, ((element C (powerset (the_carrier A))) => ((C = (lim_points_of_net A B)) <=> (All D, ((element D (the_carrier A)) => ((in D C) <=> (All E, ((point_neighbourhood E A D) => (is_eventually_in A B E))))))))))))) (directed_relstr T_1) (transitive_relstr T_1) (top_str T_0) (All A, ((top_str A) => (one_sorted_str A))) (-. (empty_carrier T_0)) (All A, (((-. (empty_carrier A)) /\ (one_sorted_str A)) => (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A)))) => (All C, ((is_eventually_in A B C) => (is_often_in A B C))))))) ### All 64 % 5.46/5.69 66. (((-. (empty_carrier T_0)) /\ ((topological_space T_0) /\ (top_str T_0))) => (All B, (((-. (empty_carrier B)) /\ (net_str B T_0)) => (All C, ((element C (the_carrier T_0)) => ((is_a_cluster_point_of_netstr T_0 B C) <=> (All D, ((point_neighbourhood D T_0 C) => (is_often_in T_0 B D))))))))) (All A, (((-. (empty_carrier A)) /\ (one_sorted_str A)) => (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A)))) => (All C, ((is_eventually_in A B C) => (is_often_in A B C))))))) (All A, ((top_str A) => (one_sorted_str A))) (transitive_relstr T_1) (directed_relstr T_1) (All A, (((-. (empty_carrier A)) /\ ((topological_space A) /\ (top_str A))) => (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A)))) => (All C, ((element C (powerset (the_carrier A))) => ((C = (lim_points_of_net A B)) <=> (All D, ((element D (the_carrier A)) => ((in D C) <=> (All E, ((point_neighbourhood E A D) => (is_eventually_in A B E))))))))))))) (All A, (All B, (((-. (empty_carrier A)) /\ ((topological_space A) /\ ((top_str A) /\ ((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A))))))) => (element (lim_points_of_net A B) (powerset (the_carrier A)))))) (in T_2 (lim_points_of_net T_0 T_1)) (-. (is_a_cluster_point_of_netstr T_0 T_1 T_2)) (element T_2 (the_carrier T_0)) (net_str T_1 T_0) (-. (empty_carrier T_1)) (top_str T_0) (topological_space T_0) (-. (empty_carrier T_0)) ### DisjTree 1 2 3 65 % 5.46/5.69 67. (All A, (((-. (empty_carrier A)) /\ ((topological_space A) /\ (top_str A))) => (All B, (((-. (empty_carrier B)) /\ (net_str B A)) => (All C, ((element C (the_carrier A)) => ((is_a_cluster_point_of_netstr A B C) <=> (All D, ((point_neighbourhood D A C) => (is_often_in A B D)))))))))) (-. (empty_carrier T_0)) (topological_space T_0) (top_str T_0) (-. (empty_carrier T_1)) (net_str T_1 T_0) (element T_2 (the_carrier T_0)) (-. (is_a_cluster_point_of_netstr T_0 T_1 T_2)) (in T_2 (lim_points_of_net T_0 T_1)) (All A, (All B, (((-. (empty_carrier A)) /\ ((topological_space A) /\ ((top_str A) /\ ((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A))))))) => (element (lim_points_of_net A B) (powerset (the_carrier A)))))) (All A, (((-. (empty_carrier A)) /\ ((topological_space A) /\ (top_str A))) => (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A)))) => (All C, ((element C (powerset (the_carrier A))) => ((C = (lim_points_of_net A B)) <=> (All D, ((element D (the_carrier A)) => ((in D C) <=> (All E, ((point_neighbourhood E A D) => (is_eventually_in A B E))))))))))))) (directed_relstr T_1) (transitive_relstr T_1) (All A, ((top_str A) => (one_sorted_str A))) (All A, (((-. (empty_carrier A)) /\ (one_sorted_str A)) => (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A)))) => (All C, ((is_eventually_in A B C) => (is_often_in A B C))))))) ### All 66 % 5.46/5.69 68. (-. ((element T_2 (the_carrier T_0)) => ((in T_2 (lim_points_of_net T_0 T_1)) => (is_a_cluster_point_of_netstr T_0 T_1 T_2)))) (All A, (((-. (empty_carrier A)) /\ (one_sorted_str A)) => (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A)))) => (All C, ((is_eventually_in A B C) => (is_often_in A B C))))))) (All A, ((top_str A) => (one_sorted_str A))) (transitive_relstr T_1) (directed_relstr T_1) (All A, (((-. (empty_carrier A)) /\ ((topological_space A) /\ (top_str A))) => (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A)))) => (All C, ((element C (powerset (the_carrier A))) => ((C = (lim_points_of_net A B)) <=> (All D, ((element D (the_carrier A)) => ((in D C) <=> (All E, ((point_neighbourhood E A D) => (is_eventually_in A B E))))))))))))) (All A, (All B, (((-. (empty_carrier A)) /\ ((topological_space A) /\ ((top_str A) /\ ((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A))))))) => (element (lim_points_of_net A B) (powerset (the_carrier A)))))) (net_str T_1 T_0) (-. (empty_carrier T_1)) (top_str T_0) (topological_space T_0) (-. (empty_carrier T_0)) (All A, (((-. (empty_carrier A)) /\ ((topological_space A) /\ (top_str A))) => (All B, (((-. (empty_carrier B)) /\ (net_str B A)) => (All C, ((element C (the_carrier A)) => ((is_a_cluster_point_of_netstr A B C) <=> (All D, ((point_neighbourhood D A C) => (is_often_in A B D)))))))))) ### ConjTree 67 % 5.46/5.69 69. (-. (All C, ((element C (the_carrier T_0)) => ((in C (lim_points_of_net T_0 T_1)) => (is_a_cluster_point_of_netstr T_0 T_1 C))))) (All A, (((-. (empty_carrier A)) /\ ((topological_space A) /\ (top_str A))) => (All B, (((-. (empty_carrier B)) /\ (net_str B A)) => (All C, ((element C (the_carrier A)) => ((is_a_cluster_point_of_netstr A B C) <=> (All D, ((point_neighbourhood D A C) => (is_often_in A B D)))))))))) (-. (empty_carrier T_0)) (topological_space T_0) (top_str T_0) (-. (empty_carrier T_1)) (net_str T_1 T_0) (All A, (All B, (((-. (empty_carrier A)) /\ ((topological_space A) /\ ((top_str A) /\ ((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A))))))) => (element (lim_points_of_net A B) (powerset (the_carrier A)))))) (All A, (((-. (empty_carrier A)) /\ ((topological_space A) /\ (top_str A))) => (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A)))) => (All C, ((element C (powerset (the_carrier A))) => ((C = (lim_points_of_net A B)) <=> (All D, ((element D (the_carrier A)) => ((in D C) <=> (All E, ((point_neighbourhood E A D) => (is_eventually_in A B E))))))))))))) (directed_relstr T_1) (transitive_relstr T_1) (All A, ((top_str A) => (one_sorted_str A))) (All A, (((-. (empty_carrier A)) /\ (one_sorted_str A)) => (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A)))) => (All C, ((is_eventually_in A B C) => (is_often_in A B C))))))) ### NotAllEx 68 % 5.46/5.70 70. (-. (((-. (empty_carrier T_1)) /\ ((transitive_relstr T_1) /\ ((directed_relstr T_1) /\ (net_str T_1 T_0)))) => (All C, ((element C (the_carrier T_0)) => ((in C (lim_points_of_net T_0 T_1)) => (is_a_cluster_point_of_netstr T_0 T_1 C)))))) (All A, (((-. (empty_carrier A)) /\ (one_sorted_str A)) => (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A)))) => (All C, ((is_eventually_in A B C) => (is_often_in A B C))))))) (All A, ((top_str A) => (one_sorted_str A))) (All A, (((-. (empty_carrier A)) /\ ((topological_space A) /\ (top_str A))) => (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A)))) => (All C, ((element C (powerset (the_carrier A))) => ((C = (lim_points_of_net A B)) <=> (All D, ((element D (the_carrier A)) => ((in D C) <=> (All E, ((point_neighbourhood E A D) => (is_eventually_in A B E))))))))))))) (All A, (All B, (((-. (empty_carrier A)) /\ ((topological_space A) /\ ((top_str A) /\ ((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A))))))) => (element (lim_points_of_net A B) (powerset (the_carrier A)))))) (top_str T_0) (topological_space T_0) (-. (empty_carrier T_0)) (All A, (((-. (empty_carrier A)) /\ ((topological_space A) /\ (top_str A))) => (All B, (((-. (empty_carrier B)) /\ (net_str B A)) => (All C, ((element C (the_carrier A)) => ((is_a_cluster_point_of_netstr A B C) <=> (All D, ((point_neighbourhood D A C) => (is_often_in A B D)))))))))) ### ConjTree 69 % 5.46/5.70 71. (-. (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B T_0)))) => (All C, ((element C (the_carrier T_0)) => ((in C (lim_points_of_net T_0 B)) => (is_a_cluster_point_of_netstr T_0 B C))))))) (All A, (((-. (empty_carrier A)) /\ ((topological_space A) /\ (top_str A))) => (All B, (((-. (empty_carrier B)) /\ (net_str B A)) => (All C, ((element C (the_carrier A)) => ((is_a_cluster_point_of_netstr A B C) <=> (All D, ((point_neighbourhood D A C) => (is_often_in A B D)))))))))) (-. (empty_carrier T_0)) (topological_space T_0) (top_str T_0) (All A, (All B, (((-. (empty_carrier A)) /\ ((topological_space A) /\ ((top_str A) /\ ((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A))))))) => (element (lim_points_of_net A B) (powerset (the_carrier A)))))) (All A, (((-. (empty_carrier A)) /\ ((topological_space A) /\ (top_str A))) => (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A)))) => (All C, ((element C (powerset (the_carrier A))) => ((C = (lim_points_of_net A B)) <=> (All D, ((element D (the_carrier A)) => ((in D C) <=> (All E, ((point_neighbourhood E A D) => (is_eventually_in A B E))))))))))))) (All A, ((top_str A) => (one_sorted_str A))) (All A, (((-. (empty_carrier A)) /\ (one_sorted_str A)) => (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A)))) => (All C, ((is_eventually_in A B C) => (is_often_in A B C))))))) ### NotAllEx 70 % 5.46/5.70 72. (-. (((-. (empty_carrier T_0)) /\ ((topological_space T_0) /\ (top_str T_0))) => (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B T_0)))) => (All C, ((element C (the_carrier T_0)) => ((in C (lim_points_of_net T_0 B)) => (is_a_cluster_point_of_netstr T_0 B C)))))))) (All A, (((-. (empty_carrier A)) /\ (one_sorted_str A)) => (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A)))) => (All C, ((is_eventually_in A B C) => (is_often_in A B C))))))) (All A, ((top_str A) => (one_sorted_str A))) (All A, (((-. (empty_carrier A)) /\ ((topological_space A) /\ (top_str A))) => (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A)))) => (All C, ((element C (powerset (the_carrier A))) => ((C = (lim_points_of_net A B)) <=> (All D, ((element D (the_carrier A)) => ((in D C) <=> (All E, ((point_neighbourhood E A D) => (is_eventually_in A B E))))))))))))) (All A, (All B, (((-. (empty_carrier A)) /\ ((topological_space A) /\ ((top_str A) /\ ((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A))))))) => (element (lim_points_of_net A B) (powerset (the_carrier A)))))) (All A, (((-. (empty_carrier A)) /\ ((topological_space A) /\ (top_str A))) => (All B, (((-. (empty_carrier B)) /\ (net_str B A)) => (All C, ((element C (the_carrier A)) => ((is_a_cluster_point_of_netstr A B C) <=> (All D, ((point_neighbourhood D A C) => (is_often_in A B D)))))))))) ### ConjTree 71 % 5.46/5.70 73. (-. (All A, (((-. (empty_carrier A)) /\ ((topological_space A) /\ (top_str A))) => (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A)))) => (All C, ((element C (the_carrier A)) => ((in C (lim_points_of_net A B)) => (is_a_cluster_point_of_netstr A B C))))))))) (All A, (((-. (empty_carrier A)) /\ ((topological_space A) /\ (top_str A))) => (All B, (((-. (empty_carrier B)) /\ (net_str B A)) => (All C, ((element C (the_carrier A)) => ((is_a_cluster_point_of_netstr A B C) <=> (All D, ((point_neighbourhood D A C) => (is_often_in A B D)))))))))) (All A, (All B, (((-. (empty_carrier A)) /\ ((topological_space A) /\ ((top_str A) /\ ((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A))))))) => (element (lim_points_of_net A B) (powerset (the_carrier A)))))) (All A, (((-. (empty_carrier A)) /\ ((topological_space A) /\ (top_str A))) => (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A)))) => (All C, ((element C (powerset (the_carrier A))) => ((C = (lim_points_of_net A B)) <=> (All D, ((element D (the_carrier A)) => ((in D C) <=> (All E, ((point_neighbourhood E A D) => (is_eventually_in A B E))))))))))))) (All A, ((top_str A) => (one_sorted_str A))) (All A, (((-. (empty_carrier A)) /\ (one_sorted_str A)) => (All B, (((-. (empty_carrier B)) /\ ((transitive_relstr B) /\ ((directed_relstr B) /\ (net_str B A)))) => (All C, ((is_eventually_in A B C) => (is_often_in A B C))))))) ### NotAllEx 72 % 5.46/5.70 % SZS output end Proof % 5.46/5.70 (* END-PROOF *) %------------------------------------------------------------------------------