%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : GEO223+2 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n020.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 07:01:03 EDT 2022 % Result : Theorem 7.27s 7.43s % Output : Proof 7.27s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : GEO223+2 : TPTP v8.1.0. Released v3.3.0. % 0.12/0.13 % Command : run_zenon %s %d % 0.13/0.35 % Computer : n020.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 600 % 0.13/0.35 % DateTime : Sat Jun 18 06:31:34 EDT 2022 % 0.13/0.35 % CPUTime : % 7.27/7.43 (* PROOF-FOUND *) % 7.27/7.43 % SZS status Theorem % 7.27/7.43 (* BEGIN-PROOF *) % 7.27/7.43 % SZS output start Proof % 7.27/7.43 Theorem con : (forall A : zenon_U, (forall L : zenon_U, (~(distinct_lines (parallel_through_point L A) (orthogonal_through_point (orthogonal_through_point L A) A))))). % 7.27/7.43 Proof. % 7.27/7.43 assert (zenon_L1_ : forall (zenon_TL_w : zenon_U) (zenon_TA_x : zenon_U), (apart_point_and_line zenon_TA_x (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x)) -> False). % 7.27/7.43 do 2 intro. intros zenon_H15. % 7.27/7.43 generalize (ooc2 zenon_TA_x). zenon_intro zenon_H18. % 7.27/7.43 generalize (zenon_H18 (orthogonal_through_point zenon_TL_w zenon_TA_x)). zenon_intro zenon_H19. % 7.27/7.43 exact (zenon_H19 zenon_H15). % 7.27/7.43 (* end of lemma zenon_L1_ *) % 7.27/7.43 assert (zenon_L2_ : forall (zenon_TL_w : zenon_U) (zenon_TA_x : zenon_U), (forall Y : zenon_U, (~(apart_point_and_line zenon_TA_x (parallel_through_point Y zenon_TA_x)))) -> (apart_point_and_line zenon_TA_x (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x)) -> False). % 7.27/7.43 do 2 intro. intros zenon_H1a zenon_H1b. % 7.27/7.43 generalize (zenon_H1a (parallel_through_point zenon_TL_w zenon_TA_x)). zenon_intro zenon_H1c. % 7.27/7.43 exact (zenon_H1c zenon_H1b). % 7.27/7.43 (* end of lemma zenon_L2_ *) % 7.27/7.43 assert (zenon_L3_ : forall (zenon_TA_x : zenon_U) (zenon_TL_w : zenon_U), (forall Y : zenon_U, (forall Z : zenon_U, ((distinct_lines (parallel_through_point zenon_TL_w zenon_TA_x) Y)->((distinct_lines (parallel_through_point zenon_TL_w zenon_TA_x) Z)\/(distinct_lines Y Z))))) -> (~(distinct_lines (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) (parallel_through_point zenon_TL_w zenon_TA_x))) -> (~(distinct_lines (parallel_through_point zenon_TL_w zenon_TA_x) (parallel_through_point zenon_TL_w zenon_TA_x))) -> (distinct_lines (parallel_through_point zenon_TL_w zenon_TA_x) (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x)) -> False). % 7.27/7.43 do 2 intro. intros zenon_H1d zenon_H1e zenon_H1f zenon_H20. % 7.27/7.43 generalize (zenon_H1d (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x)). zenon_intro zenon_H21. % 7.27/7.43 generalize (zenon_H21 (parallel_through_point zenon_TL_w zenon_TA_x)). zenon_intro zenon_H22. % 7.27/7.43 apply (zenon_imply_s _ _ zenon_H22); [ zenon_intro zenon_H24 | zenon_intro zenon_H23 ]. % 7.27/7.43 exact (zenon_H24 zenon_H20). % 7.27/7.43 apply (zenon_or_s _ _ zenon_H23); [ zenon_intro zenon_H26 | zenon_intro zenon_H25 ]. % 7.27/7.43 exact (zenon_H1f zenon_H26). % 7.27/7.43 exact (zenon_H1e zenon_H25). % 7.27/7.43 (* end of lemma zenon_L3_ *) % 7.27/7.43 assert (zenon_L4_ : forall (zenon_TL_w : zenon_U) (zenon_TA_x : zenon_U), (forall L : zenon_U, (~(apart_point_and_line zenon_TA_x (orthogonal_through_point L zenon_TA_x)))) -> (apart_point_and_line zenon_TA_x (orthogonal_through_point zenon_TL_w zenon_TA_x)) -> False). % 7.27/7.43 do 2 intro. intros zenon_H18 zenon_H27. % 7.27/7.43 generalize (zenon_H18 zenon_TL_w). zenon_intro zenon_H28. % 7.27/7.43 exact (zenon_H28 zenon_H27). % 7.27/7.43 (* end of lemma zenon_L4_ *) % 7.27/7.43 assert (zenon_L5_ : forall (zenon_TA_x : zenon_U) (zenon_TL_w : zenon_U), (forall M : zenon_U, (forall N : zenon_U, ((distinct_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) M)->((apart_point_and_line zenon_TA_x (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x))\/((apart_point_and_line zenon_TA_x M)\/((unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) N)\/(unorthogonal_lines M N))))))) -> (~(unorthogonal_lines (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TL_w)) -> (~(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) zenon_TL_w)) -> (forall L : zenon_U, (~(apart_point_and_line zenon_TA_x (orthogonal_through_point L zenon_TA_x)))) -> (~(apart_point_and_line zenon_TA_x (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x))) -> (distinct_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) (orthogonal_through_point zenon_TL_w zenon_TA_x)) -> False). % 7.27/7.43 do 2 intro. intros zenon_H29 zenon_H2a zenon_H2b zenon_H18 zenon_H19 zenon_H2c. % 7.27/7.43 generalize (zenon_H29 (orthogonal_through_point zenon_TL_w zenon_TA_x)). zenon_intro zenon_H2d. % 7.27/7.43 generalize (zenon_H2d zenon_TL_w). zenon_intro zenon_H2e. % 7.27/7.43 apply (zenon_imply_s _ _ zenon_H2e); [ zenon_intro zenon_H30 | zenon_intro zenon_H2f ]. % 7.27/7.43 exact (zenon_H30 zenon_H2c). % 7.27/7.43 apply (zenon_or_s _ _ zenon_H2f); [ zenon_intro zenon_H15 | zenon_intro zenon_H31 ]. % 7.27/7.43 exact (zenon_H19 zenon_H15). % 7.27/7.43 apply (zenon_or_s _ _ zenon_H31); [ zenon_intro zenon_H27 | zenon_intro zenon_H32 ]. % 7.27/7.43 apply (zenon_L4_ zenon_TL_w zenon_TA_x); trivial. % 7.27/7.43 apply (zenon_or_s _ _ zenon_H32); [ zenon_intro zenon_H34 | zenon_intro zenon_H33 ]. % 7.27/7.43 exact (zenon_H2b zenon_H34). % 7.27/7.43 exact (zenon_H2a zenon_H33). % 7.27/7.43 (* end of lemma zenon_L5_ *) % 7.27/7.43 assert (zenon_L6_ : forall (zenon_TA_x : zenon_U) (zenon_TL_w : zenon_U), (forall Z : zenon_U, ((distinct_lines (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) Z)->((apart_point_and_line zenon_TA_x (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x))\/((apart_point_and_line zenon_TA_x Z)\/(convergent_lines (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) Z))))) -> (forall Z : zenon_U, ((distinct_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x))->((distinct_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) Z)\/(distinct_lines (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) Z)))) -> (distinct_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x)) -> (forall M : zenon_U, (forall N : zenon_U, ((distinct_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) M)->((apart_point_and_line zenon_TA_x (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x))\/((apart_point_and_line zenon_TA_x M)\/((unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) N)\/(unorthogonal_lines M N))))))) -> (~(unorthogonal_lines (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TL_w)) -> (~(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) zenon_TL_w)) -> (forall L : zenon_U, (~(apart_point_and_line zenon_TA_x (orthogonal_through_point L zenon_TA_x)))) -> (~(apart_point_and_line zenon_TA_x (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x))) -> (~(apart_point_and_line zenon_TA_x (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x))) -> (~(convergent_lines (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) (orthogonal_through_point zenon_TL_w zenon_TA_x))) -> False). % 7.27/7.43 do 2 intro. intros zenon_H35 zenon_H36 zenon_H37 zenon_H29 zenon_H2a zenon_H2b zenon_H18 zenon_H19 zenon_H1c zenon_H38. % 7.27/7.43 generalize (zenon_H35 (orthogonal_through_point zenon_TL_w zenon_TA_x)). zenon_intro zenon_H39. % 7.27/7.43 apply (zenon_imply_s _ _ zenon_H39); [ zenon_intro zenon_H3b | zenon_intro zenon_H3a ]. % 7.27/7.43 generalize (zenon_H36 (orthogonal_through_point zenon_TL_w zenon_TA_x)). zenon_intro zenon_H3c. % 7.27/7.43 apply (zenon_imply_s _ _ zenon_H3c); [ zenon_intro zenon_H3e | zenon_intro zenon_H3d ]. % 7.27/7.43 exact (zenon_H3e zenon_H37). % 7.27/7.43 apply (zenon_or_s _ _ zenon_H3d); [ zenon_intro zenon_H2c | zenon_intro zenon_H3f ]. % 7.27/7.43 apply (zenon_L5_ zenon_TA_x zenon_TL_w); trivial. % 7.27/7.43 exact (zenon_H3b zenon_H3f). % 7.27/7.43 apply (zenon_or_s _ _ zenon_H3a); [ zenon_intro zenon_H1b | zenon_intro zenon_H40 ]. % 7.27/7.43 exact (zenon_H1c zenon_H1b). % 7.27/7.43 apply (zenon_or_s _ _ zenon_H40); [ zenon_intro zenon_H27 | zenon_intro zenon_H41 ]. % 7.27/7.43 apply (zenon_L4_ zenon_TL_w zenon_TA_x); trivial. % 7.27/7.43 exact (zenon_H38 zenon_H41). % 7.27/7.43 (* end of lemma zenon_L6_ *) % 7.27/7.43 assert (zenon_L7_ : forall (zenon_TA_x : zenon_U) (zenon_TL_w : zenon_U), (forall N : zenon_U, ((distinct_lines (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x))->((apart_point_and_line zenon_TA_x (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x))\/((apart_point_and_line zenon_TA_x (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x))\/((unorthogonal_lines (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) N)\/(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) N)))))) -> (distinct_lines (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x)) -> (~(apart_point_and_line zenon_TA_x (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x))) -> (~(apart_point_and_line zenon_TA_x (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x))) -> (~(unorthogonal_lines (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) (orthogonal_through_point zenon_TL_w zenon_TA_x))) -> (~(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) (orthogonal_through_point zenon_TL_w zenon_TA_x))) -> False). % 7.27/7.43 do 2 intro. intros zenon_H42 zenon_H43 zenon_H1c zenon_H19 zenon_H44 zenon_H45. % 7.27/7.43 generalize (zenon_H42 (orthogonal_through_point zenon_TL_w zenon_TA_x)). zenon_intro zenon_H46. % 7.27/7.43 apply (zenon_imply_s _ _ zenon_H46); [ zenon_intro zenon_H48 | zenon_intro zenon_H47 ]. % 7.27/7.43 exact (zenon_H48 zenon_H43). % 7.27/7.43 apply (zenon_or_s _ _ zenon_H47); [ zenon_intro zenon_H1b | zenon_intro zenon_H49 ]. % 7.27/7.43 exact (zenon_H1c zenon_H1b). % 7.27/7.43 apply (zenon_or_s _ _ zenon_H49); [ zenon_intro zenon_H15 | zenon_intro zenon_H4a ]. % 7.27/7.43 exact (zenon_H19 zenon_H15). % 7.27/7.43 apply (zenon_or_s _ _ zenon_H4a); [ zenon_intro zenon_H4c | zenon_intro zenon_H4b ]. % 7.27/7.43 exact (zenon_H44 zenon_H4c). % 7.27/7.43 exact (zenon_H45 zenon_H4b). % 7.27/7.43 (* end of lemma zenon_L7_ *) % 7.27/7.43 assert (zenon_L8_ : forall (zenon_TA_x : zenon_U) (zenon_TL_w : zenon_U), ((convergent_lines (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TL_w)/\(unorthogonal_lines (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TL_w)) -> (~(unorthogonal_lines (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TL_w)) -> False). % 7.27/7.43 do 2 intro. intros zenon_H4d zenon_H2a. % 7.27/7.43 apply (zenon_and_s _ _ zenon_H4d). zenon_intro zenon_H4e. zenon_intro zenon_H33. % 7.27/7.43 exact (zenon_H2a zenon_H33). % 7.27/7.43 (* end of lemma zenon_L8_ *) % 7.27/7.43 assert (zenon_L9_ : forall (zenon_TA_x : zenon_U) (zenon_TL_w : zenon_U), (forall N : zenon_U, (((convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) (parallel_through_point zenon_TL_w zenon_TA_x))/\(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) (parallel_through_point zenon_TL_w zenon_TA_x)))->(((convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) N)/\(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) N))\/((convergent_lines (parallel_through_point zenon_TL_w zenon_TA_x) N)/\(unorthogonal_lines (parallel_through_point zenon_TL_w zenon_TA_x) N))))) -> (convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) (parallel_through_point zenon_TL_w zenon_TA_x)) -> (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) (parallel_through_point zenon_TL_w zenon_TA_x)) -> (~(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) (orthogonal_through_point zenon_TL_w zenon_TA_x))) -> (~(convergent_lines (parallel_through_point zenon_TL_w zenon_TA_x) (orthogonal_through_point zenon_TL_w zenon_TA_x))) -> False). % 7.27/7.43 do 2 intro. intros zenon_H4f zenon_H50 zenon_H51 zenon_H45 zenon_H52. % 7.27/7.43 generalize (zenon_H4f (orthogonal_through_point zenon_TL_w zenon_TA_x)). zenon_intro zenon_H53. % 7.27/7.43 apply (zenon_imply_s _ _ zenon_H53); [ zenon_intro zenon_H55 | zenon_intro zenon_H54 ]. % 7.27/7.43 apply (zenon_notand_s _ _ zenon_H55); [ zenon_intro zenon_H57 | zenon_intro zenon_H56 ]. % 7.27/7.43 exact (zenon_H57 zenon_H50). % 7.27/7.43 exact (zenon_H56 zenon_H51). % 7.27/7.43 apply (zenon_or_s _ _ zenon_H54); [ zenon_intro zenon_H59 | zenon_intro zenon_H58 ]. % 7.27/7.43 apply (zenon_and_s _ _ zenon_H59). zenon_intro zenon_H5a. zenon_intro zenon_H4b. % 7.27/7.43 exact (zenon_H45 zenon_H4b). % 7.27/7.43 apply (zenon_and_s _ _ zenon_H58). zenon_intro zenon_H5c. zenon_intro zenon_H5b. % 7.27/7.43 exact (zenon_H52 zenon_H5c). % 7.27/7.43 (* end of lemma zenon_L9_ *) % 7.27/7.43 assert (zenon_L10_ : forall (zenon_TA_x : zenon_U) (zenon_TL_w : zenon_U), ((convergent_lines zenon_TL_w (parallel_through_point zenon_TL_w zenon_TA_x))/\(unorthogonal_lines zenon_TL_w (parallel_through_point zenon_TL_w zenon_TA_x))) -> (~(convergent_lines zenon_TL_w (parallel_through_point zenon_TL_w zenon_TA_x))) -> False). % 7.27/7.43 do 2 intro. intros zenon_H5d zenon_H5e. % 7.27/7.43 apply (zenon_and_s _ _ zenon_H5d). zenon_intro zenon_H60. zenon_intro zenon_H5f. % 7.27/7.43 exact (zenon_H5e zenon_H60). % 7.27/7.43 (* end of lemma zenon_L10_ *) % 7.27/7.43 assert (zenon_L11_ : forall (zenon_TA_x : zenon_U) (zenon_TL_w : zenon_U), (forall N : zenon_U, (((convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) zenon_TL_w)/\(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) zenon_TL_w))->(((convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) N)/\(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) N))\/((convergent_lines zenon_TL_w N)/\(unorthogonal_lines zenon_TL_w N))))) -> (convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) zenon_TL_w) -> (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) zenon_TL_w) -> (~(convergent_lines (parallel_through_point zenon_TL_w zenon_TA_x) (orthogonal_through_point zenon_TL_w zenon_TA_x))) -> (~(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) (orthogonal_through_point zenon_TL_w zenon_TA_x))) -> (convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) (parallel_through_point zenon_TL_w zenon_TA_x)) -> (forall N : zenon_U, (((convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) (parallel_through_point zenon_TL_w zenon_TA_x))/\(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) (parallel_through_point zenon_TL_w zenon_TA_x)))->(((convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) N)/\(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) N))\/((convergent_lines (parallel_through_point zenon_TL_w zenon_TA_x) N)/\(unorthogonal_lines (parallel_through_point zenon_TL_w zenon_TA_x) N))))) -> (~(convergent_lines zenon_TL_w (parallel_through_point zenon_TL_w zenon_TA_x))) -> False). % 7.27/7.43 do 2 intro. intros zenon_H61 zenon_H62 zenon_H34 zenon_H52 zenon_H45 zenon_H50 zenon_H4f zenon_H5e. % 7.27/7.43 generalize (zenon_H61 (parallel_through_point zenon_TL_w zenon_TA_x)). zenon_intro zenon_H63. % 7.27/7.43 apply (zenon_imply_s _ _ zenon_H63); [ zenon_intro zenon_H65 | zenon_intro zenon_H64 ]. % 7.27/7.43 apply (zenon_notand_s _ _ zenon_H65); [ zenon_intro zenon_H66 | zenon_intro zenon_H2b ]. % 7.27/7.43 exact (zenon_H66 zenon_H62). % 7.27/7.43 exact (zenon_H2b zenon_H34). % 7.27/7.43 apply (zenon_or_s _ _ zenon_H64); [ zenon_intro zenon_H67 | zenon_intro zenon_H5d ]. % 7.27/7.43 apply (zenon_and_s _ _ zenon_H67). zenon_intro zenon_H50. zenon_intro zenon_H51. % 7.27/7.43 apply (zenon_L9_ zenon_TA_x zenon_TL_w); trivial. % 7.27/7.43 apply (zenon_L10_ zenon_TA_x zenon_TL_w); trivial. % 7.27/7.43 (* end of lemma zenon_L11_ *) % 7.27/7.43 assert (zenon_L12_ : forall (zenon_TA_x : zenon_U) (zenon_TL_w : zenon_U), (forall N : zenon_U, ((distinct_lines (parallel_through_point zenon_TL_w zenon_TA_x) (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x))->((apart_point_and_line zenon_TA_x (parallel_through_point zenon_TL_w zenon_TA_x))\/((apart_point_and_line zenon_TA_x (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x))\/((unorthogonal_lines (parallel_through_point zenon_TL_w zenon_TA_x) N)\/(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) N)))))) -> (distinct_lines (parallel_through_point zenon_TL_w zenon_TA_x) (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x)) -> (~(apart_point_and_line zenon_TA_x (parallel_through_point zenon_TL_w zenon_TA_x))) -> (~(apart_point_and_line zenon_TA_x (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x))) -> (~(unorthogonal_lines (parallel_through_point zenon_TL_w zenon_TA_x) (orthogonal_through_point zenon_TL_w zenon_TA_x))) -> (~(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) (orthogonal_through_point zenon_TL_w zenon_TA_x))) -> False). % 7.27/7.43 do 2 intro. intros zenon_H68 zenon_H69 zenon_H6a zenon_H19 zenon_H6b zenon_H45. % 7.27/7.43 generalize (zenon_H68 (orthogonal_through_point zenon_TL_w zenon_TA_x)). zenon_intro zenon_H6c. % 7.27/7.43 apply (zenon_imply_s _ _ zenon_H6c); [ zenon_intro zenon_H6e | zenon_intro zenon_H6d ]. % 7.27/7.43 exact (zenon_H6e zenon_H69). % 7.27/7.43 apply (zenon_or_s _ _ zenon_H6d); [ zenon_intro zenon_H70 | zenon_intro zenon_H6f ]. % 7.27/7.43 exact (zenon_H6a zenon_H70). % 7.27/7.43 apply (zenon_or_s _ _ zenon_H6f); [ zenon_intro zenon_H15 | zenon_intro zenon_H71 ]. % 7.27/7.43 exact (zenon_H19 zenon_H15). % 7.27/7.43 apply (zenon_or_s _ _ zenon_H71); [ zenon_intro zenon_H5b | zenon_intro zenon_H4b ]. % 7.27/7.43 exact (zenon_H6b zenon_H5b). % 7.27/7.43 exact (zenon_H45 zenon_H4b). % 7.27/7.43 (* end of lemma zenon_L12_ *) % 7.27/7.43 assert (zenon_L13_ : forall (zenon_TA_x : zenon_U) (zenon_TL_w : zenon_U), ((convergent_lines (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TL_w)/\(unorthogonal_lines (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TL_w)) -> (~(convergent_lines (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TL_w)) -> False). % 7.27/7.43 do 2 intro. intros zenon_H72 zenon_H73. % 7.27/7.43 apply (zenon_and_s _ _ zenon_H72). zenon_intro zenon_H75. zenon_intro zenon_H74. % 7.27/7.43 exact (zenon_H73 zenon_H75). % 7.27/7.43 (* end of lemma zenon_L13_ *) % 7.27/7.43 assert (zenon_L14_ : forall (zenon_TL_w : zenon_U) (zenon_TA_x : zenon_U), (forall L : zenon_U, (~(unorthogonal_lines (orthogonal_through_point L zenon_TA_x) L))) -> (forall N : zenon_U, (((convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) zenon_TL_w)/\(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) zenon_TL_w))->(((convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) N)/\(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) N))\/((convergent_lines zenon_TL_w N)/\(unorthogonal_lines zenon_TL_w N))))) -> (convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) zenon_TL_w) -> (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) zenon_TL_w) -> (convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) (parallel_through_point zenon_TL_w zenon_TA_x)) -> (forall N : zenon_U, (((convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) (parallel_through_point zenon_TL_w zenon_TA_x))/\(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) (parallel_through_point zenon_TL_w zenon_TA_x)))->(((convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) N)/\(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) N))\/((convergent_lines (parallel_through_point zenon_TL_w zenon_TA_x) N)/\(unorthogonal_lines (parallel_through_point zenon_TL_w zenon_TA_x) N))))) -> (~(convergent_lines zenon_TL_w (parallel_through_point zenon_TL_w zenon_TA_x))) -> (forall N : zenon_U, ((distinct_lines (parallel_through_point zenon_TL_w zenon_TA_x) (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x))->((apart_point_and_line zenon_TA_x (parallel_through_point zenon_TL_w zenon_TA_x))\/((apart_point_and_line zenon_TA_x (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x))\/((unorthogonal_lines (parallel_through_point zenon_TL_w zenon_TA_x) N)\/(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) N)))))) -> (distinct_lines (parallel_through_point zenon_TL_w zenon_TA_x) (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x)) -> (~(apart_point_and_line zenon_TA_x (parallel_through_point zenon_TL_w zenon_TA_x))) -> (~(apart_point_and_line zenon_TA_x (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x))) -> (~(convergent_lines (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TL_w)) -> (~(unorthogonal_lines (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TL_w)) -> (forall M : zenon_U, (forall N : zenon_U, (((convergent_lines (parallel_through_point zenon_TL_w zenon_TA_x) M)/\(unorthogonal_lines (parallel_through_point zenon_TL_w zenon_TA_x) M))->(((convergent_lines (parallel_through_point zenon_TL_w zenon_TA_x) N)/\(unorthogonal_lines (parallel_through_point zenon_TL_w zenon_TA_x) N))\/((convergent_lines M N)/\(unorthogonal_lines M N)))))) -> False). % 7.27/7.43 do 2 intro. intros zenon_H76 zenon_H61 zenon_H62 zenon_H34 zenon_H50 zenon_H4f zenon_H5e zenon_H68 zenon_H69 zenon_H6a zenon_H19 zenon_H73 zenon_H2a zenon_H77. % 7.27/7.43 generalize (zenon_H76 (orthogonal_through_point zenon_TL_w zenon_TA_x)). zenon_intro zenon_H45. % 7.27/7.43 generalize (zenon_H77 (orthogonal_through_point zenon_TL_w zenon_TA_x)). zenon_intro zenon_H78. % 7.27/7.43 generalize (zenon_H78 zenon_TL_w). zenon_intro zenon_H79. % 7.27/7.43 apply (zenon_imply_s _ _ zenon_H79); [ zenon_intro zenon_H7b | zenon_intro zenon_H7a ]. % 7.27/7.43 apply (zenon_notand_s _ _ zenon_H7b); [ zenon_intro zenon_H52 | zenon_intro zenon_H6b ]. % 7.27/7.43 apply (zenon_L11_ zenon_TA_x zenon_TL_w); trivial. % 7.27/7.43 apply (zenon_L12_ zenon_TA_x zenon_TL_w); trivial. % 7.27/7.43 apply (zenon_or_s _ _ zenon_H7a); [ zenon_intro zenon_H72 | zenon_intro zenon_H4d ]. % 7.27/7.43 apply (zenon_L13_ zenon_TA_x zenon_TL_w); trivial. % 7.27/7.43 apply (zenon_L8_ zenon_TA_x zenon_TL_w); trivial. % 7.27/7.43 (* end of lemma zenon_L14_ *) % 7.27/7.43 assert (zenon_L15_ : forall (zenon_TA_x : zenon_U) (zenon_TL_w : zenon_U), (forall Y : zenon_U, (forall Z : zenon_U, ((convergent_lines zenon_TL_w Y)->((convergent_lines zenon_TL_w Z)\/(convergent_lines Y Z))))) -> (~(convergent_lines (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TL_w)) -> (~(convergent_lines zenon_TL_w zenon_TL_w)) -> (convergent_lines zenon_TL_w (parallel_through_point zenon_TL_w zenon_TA_x)) -> False). % 7.27/7.43 do 2 intro. intros zenon_H7c zenon_H73 zenon_H7d zenon_H60. % 7.27/7.43 generalize (zenon_H7c (parallel_through_point zenon_TL_w zenon_TA_x)). zenon_intro zenon_H7e. % 7.27/7.43 generalize (zenon_H7e zenon_TL_w). zenon_intro zenon_H7f. % 7.27/7.43 apply (zenon_imply_s _ _ zenon_H7f); [ zenon_intro zenon_H5e | zenon_intro zenon_H80 ]. % 7.27/7.43 exact (zenon_H5e zenon_H60). % 7.27/7.43 apply (zenon_or_s _ _ zenon_H80); [ zenon_intro zenon_H81 | zenon_intro zenon_H75 ]. % 7.27/7.43 exact (zenon_H7d zenon_H81). % 7.27/7.43 exact (zenon_H73 zenon_H75). % 7.27/7.43 (* end of lemma zenon_L15_ *) % 7.27/7.43 assert (zenon_L16_ : forall (zenon_TA_x : zenon_U) (zenon_TL_w : zenon_U), (forall M : zenon_U, ((convergent_lines zenon_TL_w M)\/(unorthogonal_lines zenon_TL_w M))) -> (forall Y : zenon_U, (forall Z : zenon_U, ((convergent_lines zenon_TL_w Y)->((convergent_lines zenon_TL_w Z)\/(convergent_lines Y Z))))) -> (~(convergent_lines (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TL_w)) -> (~(convergent_lines zenon_TL_w zenon_TL_w)) -> (~(unorthogonal_lines zenon_TL_w (parallel_through_point zenon_TL_w zenon_TA_x))) -> False). % 7.27/7.43 do 2 intro. intros zenon_H82 zenon_H7c zenon_H73 zenon_H7d zenon_H83. % 7.27/7.43 generalize (zenon_H82 (parallel_through_point zenon_TL_w zenon_TA_x)). zenon_intro zenon_H84. % 7.27/7.43 apply (zenon_or_s _ _ zenon_H84); [ zenon_intro zenon_H60 | zenon_intro zenon_H5f ]. % 7.27/7.43 apply (zenon_L15_ zenon_TA_x zenon_TL_w); trivial. % 7.27/7.43 exact (zenon_H83 zenon_H5f). % 7.27/7.43 (* end of lemma zenon_L16_ *) % 7.27/7.43 assert (zenon_L17_ : forall (zenon_TL_w : zenon_U), ((convergent_lines zenon_TL_w zenon_TL_w)/\(unorthogonal_lines zenon_TL_w zenon_TL_w)) -> (~(convergent_lines zenon_TL_w zenon_TL_w)) -> False). % 7.27/7.43 do 1 intro. intros zenon_H85 zenon_H7d. % 7.27/7.43 apply (zenon_and_s _ _ zenon_H85). zenon_intro zenon_H81. zenon_intro zenon_H86. % 7.27/7.43 exact (zenon_H7d zenon_H81). % 7.27/7.43 (* end of lemma zenon_L17_ *) % 7.27/7.43 assert (zenon_L18_ : forall (zenon_TA_x : zenon_U) (zenon_TL_w : zenon_U), (forall M : zenon_U, (forall N : zenon_U, (((convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) M)/\(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) M))->(((convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) N)/\(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) N))\/((convergent_lines M N)/\(unorthogonal_lines M N)))))) -> (forall L : zenon_U, (~(unorthogonal_lines (orthogonal_through_point L zenon_TA_x) L))) -> (forall N : zenon_U, (((convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) zenon_TL_w)/\(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) zenon_TL_w))->(((convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) N)/\(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) N))\/((convergent_lines zenon_TL_w N)/\(unorthogonal_lines zenon_TL_w N))))) -> (convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) zenon_TL_w) -> (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) zenon_TL_w) -> (convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) (parallel_through_point zenon_TL_w zenon_TA_x)) -> (forall N : zenon_U, ((distinct_lines (parallel_through_point zenon_TL_w zenon_TA_x) (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x))->((apart_point_and_line zenon_TA_x (parallel_through_point zenon_TL_w zenon_TA_x))\/((apart_point_and_line zenon_TA_x (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x))\/((unorthogonal_lines (parallel_through_point zenon_TL_w zenon_TA_x) N)\/(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) N)))))) -> (distinct_lines (parallel_through_point zenon_TL_w zenon_TA_x) (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x)) -> (~(apart_point_and_line zenon_TA_x (parallel_through_point zenon_TL_w zenon_TA_x))) -> (~(apart_point_and_line zenon_TA_x (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x))) -> (~(convergent_lines (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TL_w)) -> (~(unorthogonal_lines (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TL_w)) -> (forall M : zenon_U, (forall N : zenon_U, (((convergent_lines (parallel_through_point zenon_TL_w zenon_TA_x) M)/\(unorthogonal_lines (parallel_through_point zenon_TL_w zenon_TA_x) M))->(((convergent_lines (parallel_through_point zenon_TL_w zenon_TA_x) N)/\(unorthogonal_lines (parallel_through_point zenon_TL_w zenon_TA_x) N))\/((convergent_lines M N)/\(unorthogonal_lines M N)))))) -> (forall M : zenon_U, ((convergent_lines zenon_TL_w M)\/(unorthogonal_lines zenon_TL_w M))) -> (forall Y : zenon_U, (forall Z : zenon_U, ((convergent_lines zenon_TL_w Y)->((convergent_lines zenon_TL_w Z)\/(convergent_lines Y Z))))) -> (~(convergent_lines zenon_TL_w zenon_TL_w)) -> (forall M : zenon_U, (forall N : zenon_U, (((convergent_lines zenon_TL_w M)/\(unorthogonal_lines zenon_TL_w M))->(((convergent_lines zenon_TL_w N)/\(unorthogonal_lines zenon_TL_w N))\/((convergent_lines M N)/\(unorthogonal_lines M N)))))) -> False). % 7.27/7.43 do 2 intro. intros zenon_H87 zenon_H76 zenon_H61 zenon_H62 zenon_H34 zenon_H50 zenon_H68 zenon_H69 zenon_H6a zenon_H19 zenon_H73 zenon_H2a zenon_H77 zenon_H82 zenon_H7c zenon_H7d zenon_H88. % 7.27/7.43 generalize (zenon_H87 (parallel_through_point zenon_TL_w zenon_TA_x)). zenon_intro zenon_H4f. % 7.27/7.43 generalize (zenon_H88 (parallel_through_point zenon_TL_w zenon_TA_x)). zenon_intro zenon_H89. % 7.27/7.43 generalize (zenon_H89 zenon_TL_w). zenon_intro zenon_H8a. % 7.27/7.43 apply (zenon_imply_s _ _ zenon_H8a); [ zenon_intro zenon_H8c | zenon_intro zenon_H8b ]. % 7.27/7.43 apply (zenon_notand_s _ _ zenon_H8c); [ zenon_intro zenon_H5e | zenon_intro zenon_H83 ]. % 7.27/7.43 apply (zenon_L14_ zenon_TL_w zenon_TA_x); trivial. % 7.27/7.43 apply (zenon_L16_ zenon_TA_x zenon_TL_w); trivial. % 7.27/7.43 apply (zenon_or_s _ _ zenon_H8b); [ zenon_intro zenon_H85 | zenon_intro zenon_H72 ]. % 7.27/7.43 apply (zenon_L17_ zenon_TL_w); trivial. % 7.27/7.43 apply (zenon_L13_ zenon_TA_x zenon_TL_w); trivial. % 7.27/7.43 (* end of lemma zenon_L18_ *) % 7.27/7.43 assert (zenon_L19_ : forall (zenon_TA_x : zenon_U) (zenon_TL_w : zenon_U), (forall Z : zenon_U, ((convergent_lines (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) zenon_TL_w)->((convergent_lines (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) Z)\/(convergent_lines zenon_TL_w Z)))) -> (convergent_lines (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) zenon_TL_w) -> (~(convergent_lines (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) (parallel_through_point zenon_TL_w zenon_TA_x))) -> (forall Y : zenon_U, (forall Z : zenon_U, ((convergent_lines zenon_TL_w Y)->((convergent_lines zenon_TL_w Z)\/(convergent_lines Y Z))))) -> (~(convergent_lines (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TL_w)) -> (~(convergent_lines zenon_TL_w zenon_TL_w)) -> False). % 7.27/7.43 do 2 intro. intros zenon_H8d zenon_H8e zenon_H8f zenon_H7c zenon_H73 zenon_H7d. % 7.27/7.43 generalize (zenon_H8d (parallel_through_point zenon_TL_w zenon_TA_x)). zenon_intro zenon_H90. % 7.27/7.43 apply (zenon_imply_s _ _ zenon_H90); [ zenon_intro zenon_H92 | zenon_intro zenon_H91 ]. % 7.27/7.43 exact (zenon_H92 zenon_H8e). % 7.27/7.43 apply (zenon_or_s _ _ zenon_H91); [ zenon_intro zenon_H93 | zenon_intro zenon_H60 ]. % 7.27/7.43 exact (zenon_H8f zenon_H93). % 7.27/7.43 apply (zenon_L15_ zenon_TA_x zenon_TL_w); trivial. % 7.27/7.43 (* end of lemma zenon_L19_ *) % 7.27/7.43 assert (zenon_L20_ : forall (zenon_TA_x : zenon_U) (zenon_TL_w : zenon_U), (~(convergent_lines zenon_TL_w zenon_TL_w)) -> (~(convergent_lines (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TL_w)) -> (~(convergent_lines (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) (parallel_through_point zenon_TL_w zenon_TA_x))) -> (convergent_lines (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) zenon_TL_w) -> (forall Z : zenon_U, ((convergent_lines (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) zenon_TL_w)->((convergent_lines (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) Z)\/(convergent_lines zenon_TL_w Z)))) -> False). % 7.27/7.43 do 2 intro. intros zenon_H7d zenon_H73 zenon_H8f zenon_H8e zenon_H8d. % 7.27/7.43 generalize (apart6 zenon_TL_w). zenon_intro zenon_H7c. % 7.27/7.43 apply (zenon_L19_ zenon_TA_x zenon_TL_w); trivial. % 7.27/7.43 (* end of lemma zenon_L20_ *) % 7.27/7.43 assert (zenon_L21_ : forall (zenon_TA_x : zenon_U) (zenon_TL_w : zenon_U), (forall Z : zenon_U, ((convergent_lines (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) zenon_TL_w)->((convergent_lines (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) Z)\/(convergent_lines zenon_TL_w Z)))) -> (convergent_lines (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) zenon_TL_w) -> (~(convergent_lines (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) (parallel_through_point zenon_TL_w zenon_TA_x))) -> (~(convergent_lines (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TL_w)) -> False). % 7.27/7.43 do 2 intro. intros zenon_H8d zenon_H8e zenon_H8f zenon_H73. % 7.27/7.43 generalize (apart3 zenon_TL_w). zenon_intro zenon_H7d. % 7.27/7.43 apply (zenon_L20_ zenon_TA_x zenon_TL_w); trivial. % 7.27/7.43 (* end of lemma zenon_L21_ *) % 7.27/7.43 assert (zenon_L22_ : forall (zenon_TA_x : zenon_U) (zenon_TL_w : zenon_U), (forall Y : zenon_U, (forall Z : zenon_U, ((convergent_lines (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) Y)->((convergent_lines (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) Z)\/(convergent_lines Y Z))))) -> (~(convergent_lines (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TL_w)) -> (~(convergent_lines (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) (parallel_through_point zenon_TL_w zenon_TA_x))) -> (convergent_lines (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) zenon_TL_w) -> False). % 7.27/7.43 do 2 intro. intros zenon_H94 zenon_H73 zenon_H8f zenon_H8e. % 7.27/7.43 generalize (zenon_H94 zenon_TL_w). zenon_intro zenon_H8d. % 7.27/7.43 apply (zenon_L21_ zenon_TA_x zenon_TL_w); trivial. % 7.27/7.43 (* end of lemma zenon_L22_ *) % 7.27/7.43 assert (zenon_L23_ : forall (zenon_TL_w : zenon_U) (zenon_TA_x : zenon_U), (forall Y : zenon_U, (~(convergent_lines (parallel_through_point Y zenon_TA_x) Y))) -> (convergent_lines (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) zenon_TL_w) -> (~(convergent_lines (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) (parallel_through_point zenon_TL_w zenon_TA_x))) -> (forall Y : zenon_U, (forall Z : zenon_U, ((convergent_lines (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) Y)->((convergent_lines (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) Z)\/(convergent_lines Y Z))))) -> False). % 7.27/7.43 do 2 intro. intros zenon_H95 zenon_H8e zenon_H8f zenon_H94. % 7.27/7.43 generalize (zenon_H95 zenon_TL_w). zenon_intro zenon_H73. % 7.27/7.43 apply (zenon_L22_ zenon_TA_x zenon_TL_w); trivial. % 7.27/7.43 (* end of lemma zenon_L23_ *) % 7.27/7.43 assert (zenon_L24_ : forall (zenon_TA_x : zenon_U) (zenon_TL_w : zenon_U), (forall Z : zenon_U, ((distinct_lines (parallel_through_point zenon_TL_w zenon_TA_x) (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x))->((distinct_lines (parallel_through_point zenon_TL_w zenon_TA_x) Z)\/(distinct_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) Z)))) -> (distinct_lines (parallel_through_point zenon_TL_w zenon_TA_x) (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x)) -> (forall Y : zenon_U, (forall Z : zenon_U, ((distinct_lines (parallel_through_point zenon_TL_w zenon_TA_x) Y)->((distinct_lines (parallel_through_point zenon_TL_w zenon_TA_x) Z)\/(distinct_lines Y Z))))) -> (~(distinct_lines (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) (parallel_through_point zenon_TL_w zenon_TA_x))) -> (~(distinct_lines (parallel_through_point zenon_TL_w zenon_TA_x) (parallel_through_point zenon_TL_w zenon_TA_x))) -> (forall Y : zenon_U, (~(apart_point_and_line zenon_TA_x (parallel_through_point Y zenon_TA_x)))) -> (forall Z : zenon_U, ((convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) (parallel_through_point zenon_TL_w zenon_TA_x))->((convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) Z)\/(convergent_lines (parallel_through_point zenon_TL_w zenon_TA_x) Z)))) -> (convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) (parallel_through_point zenon_TL_w zenon_TA_x)) -> (~(convergent_lines (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) (parallel_through_point zenon_TL_w zenon_TA_x))) -> (forall Y : zenon_U, (~(convergent_lines (parallel_through_point Y zenon_TA_x) Y))) -> (~(apart_point_and_line zenon_TA_x (parallel_through_point zenon_TL_w zenon_TA_x))) -> (forall L : zenon_U, (~(apart_point_and_line zenon_TA_x (orthogonal_through_point L zenon_TA_x)))) -> (forall Z : zenon_U, ((distinct_lines (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) Z)->((apart_point_and_line zenon_TA_x (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x))\/((apart_point_and_line zenon_TA_x Z)\/(convergent_lines (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) Z))))) -> (convergent_lines (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x)) -> (forall Y : zenon_U, ((convergent_lines (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) Y)->(distinct_lines (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) Y))) -> False). % 7.27/7.43 do 2 intro. intros zenon_H96 zenon_H69 zenon_H1d zenon_H1e zenon_H1f zenon_H1a zenon_H97 zenon_H50 zenon_H8f zenon_H95 zenon_H6a zenon_H18 zenon_H35 zenon_H98 zenon_H99. % 7.27/7.43 generalize (apart6 (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x)). zenon_intro zenon_H94. % 7.27/7.43 generalize (zenon_H18 (orthogonal_through_point zenon_TL_w zenon_TA_x)). zenon_intro zenon_H19. % 7.27/7.43 generalize (zenon_H96 (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x)). zenon_intro zenon_H9a. % 7.27/7.43 apply (zenon_imply_s _ _ zenon_H9a); [ zenon_intro zenon_H6e | zenon_intro zenon_H9b ]. % 7.27/7.43 exact (zenon_H6e zenon_H69). % 7.27/7.43 apply (zenon_or_s _ _ zenon_H9b); [ zenon_intro zenon_H20 | zenon_intro zenon_H37 ]. % 7.27/7.43 apply (zenon_L3_ zenon_TA_x zenon_TL_w); trivial. % 7.27/7.43 generalize (zenon_H1a (parallel_through_point zenon_TL_w zenon_TA_x)). zenon_intro zenon_H1c. % 7.27/7.43 generalize (zenon_H99 (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x)). zenon_intro zenon_H9c. % 7.27/7.43 apply (zenon_imply_s _ _ zenon_H9c); [ zenon_intro zenon_H9d | zenon_intro zenon_H43 ]. % 7.27/7.43 exact (zenon_H9d zenon_H98). % 7.27/7.43 generalize (zenon_H95 zenon_TL_w). zenon_intro zenon_H73. % 7.27/7.43 generalize (zenon_H97 zenon_TL_w). zenon_intro zenon_H9e. % 7.27/7.43 apply (zenon_imply_s _ _ zenon_H9e); [ zenon_intro zenon_H57 | zenon_intro zenon_H9f ]. % 7.27/7.43 exact (zenon_H57 zenon_H50). % 7.27/7.43 apply (zenon_or_s _ _ zenon_H9f); [ zenon_intro zenon_H62 | zenon_intro zenon_H75 ]. % 7.27/7.43 generalize (apart3 zenon_TL_w). zenon_intro zenon_H7d. % 7.27/7.43 generalize (apart6 zenon_TL_w). zenon_intro zenon_H7c. % 7.27/7.43 generalize (apart5 (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x)). zenon_intro zenon_Ha0. % 7.27/7.43 generalize (zenon_Ha0 (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x)). zenon_intro zenon_H36. % 7.27/7.43 generalize (oac1 zenon_TL_w). zenon_intro zenon_H88. % 7.27/7.43 generalize (oac1 (parallel_through_point zenon_TL_w zenon_TA_x)). zenon_intro zenon_H77. % 7.27/7.43 generalize (oac1 (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x)). zenon_intro zenon_H87. % 7.27/7.43 generalize (oac1 (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x)). zenon_intro zenon_Ha1. % 7.27/7.43 generalize (zenon_H94 zenon_TL_w). zenon_intro zenon_H8d. % 7.27/7.43 generalize (zenon_H8d zenon_TL_w). zenon_intro zenon_Ha2. % 7.27/7.43 apply (zenon_imply_s _ _ zenon_Ha2); [ zenon_intro zenon_H92 | zenon_intro zenon_Ha3 ]. % 7.27/7.43 generalize (ooc1 zenon_TA_x). zenon_intro zenon_H76. % 7.27/7.43 generalize (occu1 zenon_TL_w). zenon_intro zenon_H82. % 7.27/7.43 generalize (ouo1 zenon_TA_x). zenon_intro zenon_Ha4. % 7.27/7.43 generalize (zenon_Ha4 (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x)). zenon_intro zenon_H29. % 7.27/7.43 generalize (zenon_Ha4 (parallel_through_point zenon_TL_w zenon_TA_x)). zenon_intro zenon_Ha5. % 7.27/7.43 generalize (zenon_Ha5 (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x)). zenon_intro zenon_H68. % 7.27/7.43 generalize (zenon_Ha4 (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x)). zenon_intro zenon_Ha6. % 7.27/7.43 generalize (zenon_Ha6 (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x)). zenon_intro zenon_H42. % 7.27/7.43 generalize (zenon_H87 zenon_TL_w). zenon_intro zenon_H61. % 7.27/7.43 generalize (zenon_H76 zenon_TL_w). zenon_intro zenon_H2a. % 7.27/7.43 generalize (zenon_H61 zenon_TL_w). zenon_intro zenon_Ha7. % 7.27/7.43 apply (zenon_imply_s _ _ zenon_Ha7); [ zenon_intro zenon_H65 | zenon_intro zenon_Ha8 ]. % 7.27/7.43 apply (zenon_notand_s _ _ zenon_H65); [ zenon_intro zenon_H66 | zenon_intro zenon_H2b ]. % 7.27/7.43 exact (zenon_H66 zenon_H62). % 7.27/7.43 generalize (zenon_H76 (orthogonal_through_point zenon_TL_w zenon_TA_x)). zenon_intro zenon_H45. % 7.27/7.43 generalize (zenon_Ha1 (orthogonal_through_point zenon_TL_w zenon_TA_x)). zenon_intro zenon_Ha9. % 7.27/7.43 generalize (zenon_Ha9 zenon_TL_w). zenon_intro zenon_Haa. % 7.27/7.43 apply (zenon_imply_s _ _ zenon_Haa); [ zenon_intro zenon_Hac | zenon_intro zenon_Hab ]. % 7.27/7.43 apply (zenon_notand_s _ _ zenon_Hac); [ zenon_intro zenon_H38 | zenon_intro zenon_H44 ]. % 7.27/7.43 apply (zenon_L6_ zenon_TA_x zenon_TL_w); trivial. % 7.27/7.43 apply (zenon_L7_ zenon_TA_x zenon_TL_w); trivial. % 7.27/7.43 apply (zenon_or_s _ _ zenon_Hab); [ zenon_intro zenon_Had | zenon_intro zenon_H4d ]. % 7.27/7.43 apply (zenon_and_s _ _ zenon_Had). zenon_intro zenon_H8e. zenon_intro zenon_Hae. % 7.27/7.43 exact (zenon_H92 zenon_H8e). % 7.27/7.43 apply (zenon_L8_ zenon_TA_x zenon_TL_w); trivial. % 7.27/7.43 apply (zenon_or_s _ _ zenon_Ha8); [ zenon_intro zenon_Haf | zenon_intro zenon_H85 ]. % 7.27/7.43 apply (zenon_and_s _ _ zenon_Haf). zenon_intro zenon_H62. zenon_intro zenon_H34. % 7.27/7.43 apply (zenon_L18_ zenon_TA_x zenon_TL_w); trivial. % 7.27/7.43 apply (zenon_L17_ zenon_TL_w); trivial. % 7.27/7.43 apply (zenon_or_s _ _ zenon_Ha3); [ zenon_intro zenon_H8e | zenon_intro zenon_H81 ]. % 7.27/7.43 apply (zenon_L23_ zenon_TL_w zenon_TA_x); trivial. % 7.27/7.43 exact (zenon_H7d zenon_H81). % 7.27/7.43 exact (zenon_H73 zenon_H75). % 7.27/7.43 (* end of lemma zenon_L24_ *) % 7.27/7.43 assert (zenon_L25_ : forall (zenon_TA_x : zenon_U) (zenon_TL_w : zenon_U), (~(distinct_lines (parallel_through_point zenon_TL_w zenon_TA_x) (parallel_through_point zenon_TL_w zenon_TA_x))) -> (distinct_lines (parallel_through_point zenon_TL_w zenon_TA_x) (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x)) -> (~(distinct_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x))) -> (forall Y : zenon_U, (forall Z : zenon_U, ((distinct_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) Y)->((distinct_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) Z)\/(distinct_lines Y Z))))) -> (distinct_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x) (parallel_through_point zenon_TL_w zenon_TA_x)) -> False). % 7.27/7.43 do 2 intro. intros zenon_H1f zenon_H69 zenon_Hb0 zenon_Ha0 zenon_Hb1. % 7.27/7.43 generalize (zenon_Ha0 (parallel_through_point zenon_TL_w zenon_TA_x)). zenon_intro zenon_Hb2. % 7.27/7.43 generalize (apart5 (parallel_through_point zenon_TL_w zenon_TA_x)). zenon_intro zenon_H1d. % 7.27/7.43 generalize (zenon_H1d (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x)). zenon_intro zenon_H96. % 7.27/7.43 generalize (cp2 zenon_TA_x). zenon_intro zenon_H1a. % 7.27/7.43 generalize (zenon_H1a zenon_TL_w). zenon_intro zenon_H6a. % 7.27/7.43 generalize (cup1 zenon_TA_x). zenon_intro zenon_Hb3. % 7.27/7.43 generalize (zenon_Hb3 (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x)). zenon_intro zenon_Hb4. % 7.27/7.43 generalize (zenon_Hb4 (parallel_through_point zenon_TL_w zenon_TA_x)). zenon_intro zenon_Hb5. % 7.27/7.43 apply (zenon_imply_s _ _ zenon_Hb5); [ zenon_intro zenon_Hb7 | zenon_intro zenon_Hb6 ]. % 7.27/7.43 exact (zenon_Hb7 zenon_Hb1). % 7.27/7.43 apply (zenon_or_s _ _ zenon_Hb6); [ zenon_intro zenon_H15 | zenon_intro zenon_Hb8 ]. % 7.27/7.43 apply (zenon_L1_ zenon_TL_w zenon_TA_x); trivial. % 7.27/7.43 apply (zenon_or_s _ _ zenon_Hb8); [ zenon_intro zenon_H70 | zenon_intro zenon_H50 ]. % 7.27/7.43 exact (zenon_H6a zenon_H70). % 7.27/7.43 generalize (ooc2 zenon_TA_x). zenon_intro zenon_H18. % 7.27/7.43 generalize (cp1 zenon_TA_x). zenon_intro zenon_H95. % 7.27/7.43 generalize (zenon_H95 (parallel_through_point zenon_TL_w zenon_TA_x)). zenon_intro zenon_H8f. % 7.27/7.43 generalize (zenon_H18 (orthogonal_through_point zenon_TL_w zenon_TA_x)). zenon_intro zenon_H19. % 7.27/7.43 generalize (zenon_Hb3 (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x)). zenon_intro zenon_H35. % 7.27/7.43 generalize (zenon_H35 (parallel_through_point zenon_TL_w zenon_TA_x)). zenon_intro zenon_Hb9. % 7.27/7.43 apply (zenon_imply_s _ _ zenon_Hb9); [ zenon_intro zenon_H1e | zenon_intro zenon_Hba ]. % 7.27/7.43 generalize (apart6 (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x)). zenon_intro zenon_Hbb. % 7.27/7.43 generalize (zenon_Hbb (parallel_through_point zenon_TL_w zenon_TA_x)). zenon_intro zenon_H97. % 7.27/7.43 generalize (zenon_Hb2 (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x)). zenon_intro zenon_Hbc. % 7.27/7.43 apply (zenon_imply_s _ _ zenon_Hbc); [ zenon_intro zenon_Hb7 | zenon_intro zenon_Hbd ]. % 7.27/7.43 exact (zenon_Hb7 zenon_Hb1). % 7.27/7.43 apply (zenon_or_s _ _ zenon_Hbd); [ zenon_intro zenon_H37 | zenon_intro zenon_H20 ]. % 7.27/7.43 generalize (ceq3 (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x)). zenon_intro zenon_H99. % 7.27/7.43 generalize (zenon_H35 (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x)). zenon_intro zenon_Hbe. % 7.27/7.43 apply (zenon_imply_s _ _ zenon_Hbe); [ zenon_intro zenon_H48 | zenon_intro zenon_Hbf ]. % 7.27/7.43 generalize (zenon_Ha0 (parallel_through_point (parallel_through_point zenon_TL_w zenon_TA_x) zenon_TA_x)). zenon_intro zenon_H36. % 7.27/7.43 generalize (zenon_H36 (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x)). zenon_intro zenon_Hc0. % 7.27/7.43 apply (zenon_imply_s _ _ zenon_Hc0); [ zenon_intro zenon_H3e | zenon_intro zenon_Hc1 ]. % 7.27/7.43 exact (zenon_H3e zenon_H37). % 7.27/7.43 apply (zenon_or_s _ _ zenon_Hc1); [ zenon_intro zenon_Hc2 | zenon_intro zenon_H43 ]. % 7.27/7.43 exact (zenon_Hb0 zenon_Hc2). % 7.27/7.43 exact (zenon_H48 zenon_H43). % 7.27/7.43 apply (zenon_or_s _ _ zenon_Hbf); [ zenon_intro zenon_H1b | zenon_intro zenon_Hc3 ]. % 7.27/7.43 apply (zenon_L2_ zenon_TL_w zenon_TA_x); trivial. % 7.27/7.43 apply (zenon_or_s _ _ zenon_Hc3); [ zenon_intro zenon_H15 | zenon_intro zenon_H98 ]. % 7.27/7.43 exact (zenon_H19 zenon_H15). % 7.27/7.43 apply (zenon_L24_ zenon_TA_x zenon_TL_w); trivial. % 7.27/7.43 apply (zenon_L3_ zenon_TA_x zenon_TL_w); trivial. % 7.27/7.43 apply (zenon_or_s _ _ zenon_Hba); [ zenon_intro zenon_H1b | zenon_intro zenon_Hc4 ]. % 7.27/7.43 apply (zenon_L2_ zenon_TL_w zenon_TA_x); trivial. % 7.27/7.43 apply (zenon_or_s _ _ zenon_Hc4); [ zenon_intro zenon_H70 | zenon_intro zenon_H93 ]. % 7.27/7.43 exact (zenon_H6a zenon_H70). % 7.27/7.43 exact (zenon_H8f zenon_H93). % 7.27/7.43 (* end of lemma zenon_L25_ *) % 7.27/7.43 apply NNPP. intro zenon_G. % 7.27/7.43 apply (zenon_notallex_s (fun A : zenon_U => (forall L : zenon_U, (~(distinct_lines (parallel_through_point L A) (orthogonal_through_point (orthogonal_through_point L A) A))))) zenon_G); [ zenon_intro zenon_Hc5; idtac ]. % 7.27/7.43 elim zenon_Hc5. zenon_intro zenon_TA_x. zenon_intro zenon_Hc6. % 7.27/7.43 apply (zenon_notallex_s (fun L : zenon_U => (~(distinct_lines (parallel_through_point L zenon_TA_x) (orthogonal_through_point (orthogonal_through_point L zenon_TA_x) zenon_TA_x)))) zenon_Hc6); [ zenon_intro zenon_Hc7; idtac ]. % 7.27/7.43 elim zenon_Hc7. zenon_intro zenon_TL_w. zenon_intro zenon_Hc8. % 7.27/7.43 apply zenon_Hc8. zenon_intro zenon_H69. % 7.27/7.43 generalize (apart2 (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x)). zenon_intro zenon_Hb0. % 7.27/7.43 generalize (apart5 (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x)). zenon_intro zenon_Ha0. % 7.27/7.43 generalize (apart2 (parallel_through_point zenon_TL_w zenon_TA_x)). zenon_intro zenon_H1f. % 7.27/7.43 generalize (apart5 (parallel_through_point zenon_TL_w zenon_TA_x)). zenon_intro zenon_H1d. % 7.27/7.43 generalize (zenon_H1d (orthogonal_through_point (orthogonal_through_point zenon_TL_w zenon_TA_x) zenon_TA_x)). zenon_intro zenon_H96. % 7.27/7.43 generalize (zenon_H96 (parallel_through_point zenon_TL_w zenon_TA_x)). zenon_intro zenon_Hc9. % 7.27/7.43 apply (zenon_imply_s _ _ zenon_Hc9); [ zenon_intro zenon_H6e | zenon_intro zenon_Hca ]. % 7.27/7.43 exact (zenon_H6e zenon_H69). % 7.27/7.43 apply (zenon_or_s _ _ zenon_Hca); [ zenon_intro zenon_H26 | zenon_intro zenon_Hb1 ]. % 7.27/7.43 exact (zenon_H1f zenon_H26). % 7.27/7.44 apply (zenon_L25_ zenon_TA_x zenon_TL_w); trivial. % 7.27/7.44 Qed. % 7.27/7.44 % SZS output end Proof % 7.27/7.44 (* END-PROOF *) % 7.27/7.44 nodes searched: 917839 % 7.27/7.44 max branch formulas: 11036 % 7.27/7.44 proof nodes created: 11144 % 7.27/7.44 formulas created: 1041180 % 7.27/7.44 %------------------------------------------------------------------------------