%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : GEO223+3 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n014.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:04 EDT 2022 % Result : Theorem 1.15s 1.34s % Output : Proof 1.15s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : GEO223+3 : TPTP v8.1.0. Released v4.0.0. % 0.03/0.12 % Command : run_zenon %s %d % 0.12/0.33 % Computer : n014.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Sat Jun 18 18:35:04 EDT 2022 % 0.12/0.33 % CPUTime : % 1.15/1.34 (* PROOF-FOUND *) % 1.15/1.34 % SZS status Theorem % 1.15/1.34 (* BEGIN-PROOF *) % 1.15/1.34 % SZS output start Proof % 1.15/1.34 Theorem con : (forall A : zenon_U, (forall L : zenon_U, (equal_lines (parallel_through_point L A) (orthogonal_through_point (orthogonal_through_point L A) A)))). % 1.15/1.34 Proof. % 1.15/1.34 assert (zenon_L1_ : forall (zenon_TA_bm : zenon_U) (zenon_TL_bn : zenon_U), (~((~(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (parallel_through_point zenon_TL_bn zenon_TA_bm)))\/(~(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (parallel_through_point zenon_TL_bn zenon_TA_bm))))) -> (~(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (parallel_through_point zenon_TL_bn zenon_TA_bm))) -> False). % 1.15/1.34 do 2 intro. intros zenon_H24 zenon_H25. % 1.15/1.34 apply (zenon_notor_s _ _ zenon_H24). zenon_intro zenon_H29. zenon_intro zenon_H28. % 1.15/1.34 exact (zenon_H29 zenon_H25). % 1.15/1.34 (* end of lemma zenon_L1_ *) % 1.15/1.34 assert (zenon_L2_ : forall (zenon_TL_bn : zenon_U) (zenon_TA_bm : zenon_U), (forall Y : zenon_U, (~(convergent_lines (parallel_through_point Y zenon_TA_bm) Y))) -> (convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TL_bn) -> False). % 1.15/1.34 do 2 intro. intros zenon_H2a zenon_H2b. % 1.15/1.34 generalize (zenon_H2a zenon_TL_bn). zenon_intro zenon_H2c. % 1.15/1.34 exact (zenon_H2c zenon_H2b). % 1.15/1.34 (* end of lemma zenon_L2_ *) % 1.15/1.34 assert (zenon_L3_ : forall (zenon_TL_bn : zenon_U) (zenon_TA_bm : zenon_U), (forall L : zenon_U, (~(unorthogonal_lines (orthogonal_through_point L zenon_TA_bm) L))) -> (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (orthogonal_through_point zenon_TL_bn zenon_TA_bm)) -> False). % 1.15/1.34 do 2 intro. intros zenon_H2d zenon_H2e. % 1.15/1.34 generalize (zenon_H2d (orthogonal_through_point zenon_TL_bn zenon_TA_bm)). zenon_intro zenon_H2f. % 1.15/1.34 exact (zenon_H2f zenon_H2e). % 1.15/1.34 (* end of lemma zenon_L3_ *) % 1.15/1.34 assert (zenon_L4_ : forall (zenon_TA_bm : zenon_U) (zenon_TL_bn : zenon_U), (~((~(convergent_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)))\/(~(unorthogonal_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))))) -> (~(convergent_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))) -> False). % 1.15/1.34 do 2 intro. intros zenon_H30 zenon_H31. % 1.15/1.34 apply (zenon_notor_s _ _ zenon_H30). zenon_intro zenon_H33. zenon_intro zenon_H32. % 1.15/1.34 exact (zenon_H33 zenon_H31). % 1.15/1.34 (* end of lemma zenon_L4_ *) % 1.15/1.34 assert (zenon_L5_ : forall (zenon_TA_bm : zenon_U) (zenon_TL_bn : zenon_U), (~(~(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)))) -> (~(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))) -> False). % 1.15/1.34 do 2 intro. intros zenon_H34 zenon_H35. % 1.15/1.34 exact (zenon_H34 zenon_H35). % 1.15/1.34 (* end of lemma zenon_L5_ *) % 1.15/1.34 assert (zenon_L6_ : forall (zenon_TA_bm : zenon_U) (zenon_TL_bn : zenon_U), (~((~(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)))\/(~(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))))) -> (~(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))) -> False). % 1.15/1.34 do 2 intro. intros zenon_H36 zenon_H35. % 1.15/1.34 apply (zenon_notor_s _ _ zenon_H36). zenon_intro zenon_H37. zenon_intro zenon_H34. % 1.15/1.34 exact (zenon_H34 zenon_H35). % 1.15/1.34 (* end of lemma zenon_L6_ *) % 1.15/1.34 assert (zenon_L7_ : forall (zenon_TA_bm : zenon_U) (zenon_TL_bn : zenon_U), (forall N : zenon_U, ((((~(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)))\/(~(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))))/\((~(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) N))\/(~(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) N))))->((~(convergent_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N))\/(~(unorthogonal_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N))))) -> (~(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))) -> (~(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TL_bn)) -> (convergent_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) zenon_TL_bn) -> (unorthogonal_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) zenon_TL_bn) -> False). % 1.15/1.34 do 2 intro. intros zenon_H38 zenon_H35 zenon_H2c zenon_H39 zenon_H3a. % 1.15/1.34 generalize (zenon_H38 zenon_TL_bn). zenon_intro zenon_H3b. % 1.15/1.34 apply (zenon_imply_s _ _ zenon_H3b); [ zenon_intro zenon_H3d | zenon_intro zenon_H3c ]. % 1.15/1.34 apply (zenon_notand_s _ _ zenon_H3d); [ zenon_intro zenon_H36 | zenon_intro zenon_H3e ]. % 1.15/1.34 apply (zenon_L6_ zenon_TA_bm zenon_TL_bn); trivial. % 1.15/1.34 apply (zenon_notor_s _ _ zenon_H3e). zenon_intro zenon_H40. zenon_intro zenon_H3f. % 1.15/1.34 exact (zenon_H40 zenon_H2c). % 1.15/1.34 apply (zenon_or_s _ _ zenon_H3c); [ zenon_intro zenon_H42 | zenon_intro zenon_H41 ]. % 1.15/1.34 exact (zenon_H42 zenon_H39). % 1.15/1.34 exact (zenon_H41 zenon_H3a). % 1.15/1.34 (* end of lemma zenon_L7_ *) % 1.15/1.34 assert (zenon_L8_ : forall (zenon_TA_bm : zenon_U) (zenon_TL_bn : zenon_U), (~(~(unorthogonal_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) zenon_TL_bn))) -> (convergent_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) zenon_TL_bn) -> (~(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TL_bn)) -> (~(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))) -> (forall N : zenon_U, ((((~(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)))\/(~(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))))/\((~(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) N))\/(~(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) N))))->((~(convergent_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N))\/(~(unorthogonal_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N))))) -> False). % 1.15/1.34 do 2 intro. intros zenon_H43 zenon_H39 zenon_H2c zenon_H35 zenon_H38. % 1.15/1.34 apply zenon_H43. zenon_intro zenon_H3a. % 1.15/1.34 apply (zenon_L7_ zenon_TA_bm zenon_TL_bn); trivial. % 1.15/1.34 (* end of lemma zenon_L8_ *) % 1.15/1.34 assert (zenon_L9_ : forall (zenon_TA_bm : zenon_U) (zenon_TL_bn : zenon_U), (~((~(convergent_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) zenon_TL_bn))\/(~(unorthogonal_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) zenon_TL_bn)))) -> (forall N : zenon_U, ((((~(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)))\/(~(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))))/\((~(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) N))\/(~(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) N))))->((~(convergent_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N))\/(~(unorthogonal_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N))))) -> (~(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))) -> (~(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TL_bn)) -> (convergent_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) zenon_TL_bn) -> False). % 1.15/1.34 do 2 intro. intros zenon_H44 zenon_H38 zenon_H35 zenon_H2c zenon_H39. % 1.15/1.34 apply (zenon_notor_s _ _ zenon_H44). zenon_intro zenon_H45. zenon_intro zenon_H43. % 1.15/1.34 apply (zenon_L8_ zenon_TA_bm zenon_TL_bn); trivial. % 1.15/1.34 (* end of lemma zenon_L9_ *) % 1.15/1.34 assert (zenon_L10_ : forall (zenon_TA_bm : zenon_U) (zenon_TL_bn : zenon_U), (forall N : zenon_U, ((((~(convergent_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)))\/(~(unorthogonal_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))))/\((~(convergent_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N))\/(~(unorthogonal_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N))))->((~(convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N))\/(~(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N))))) -> (~(convergent_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))) -> (forall N : zenon_U, ((((~(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)))\/(~(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))))/\((~(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) N))\/(~(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) N))))->((~(convergent_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N))\/(~(unorthogonal_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N))))) -> (~(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))) -> (~(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TL_bn)) -> (convergent_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) zenon_TL_bn) -> (convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) zenon_TL_bn) -> (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) zenon_TL_bn) -> False). % 1.15/1.34 do 2 intro. intros zenon_H46 zenon_H31 zenon_H38 zenon_H35 zenon_H2c zenon_H39 zenon_H47 zenon_H48. % 1.15/1.34 generalize (zenon_H46 zenon_TL_bn). zenon_intro zenon_H49. % 1.15/1.34 apply (zenon_imply_s _ _ zenon_H49); [ zenon_intro zenon_H4b | zenon_intro zenon_H4a ]. % 1.15/1.34 apply (zenon_notand_s _ _ zenon_H4b); [ zenon_intro zenon_H30 | zenon_intro zenon_H44 ]. % 1.15/1.34 apply (zenon_L4_ zenon_TA_bm zenon_TL_bn); trivial. % 1.15/1.34 apply (zenon_L9_ zenon_TA_bm zenon_TL_bn); trivial. % 1.15/1.34 apply (zenon_or_s _ _ zenon_H4a); [ zenon_intro zenon_H4d | zenon_intro zenon_H4c ]. % 1.15/1.34 exact (zenon_H4d zenon_H47). % 1.15/1.34 exact (zenon_H4c zenon_H48). % 1.15/1.34 (* end of lemma zenon_L10_ *) % 1.15/1.34 assert (zenon_L11_ : forall (zenon_TA_bm : zenon_U) (zenon_TL_bn : zenon_U), (forall M : zenon_U, (forall N : zenon_U, (((~(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) M))/\(~(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N)))->(~(convergent_lines M N))))) -> (convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) zenon_TL_bn) -> (convergent_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) zenon_TL_bn) -> (~(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TL_bn)) -> (~(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))) -> (forall N : zenon_U, ((((~(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)))\/(~(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))))/\((~(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) N))\/(~(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) N))))->((~(convergent_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N))\/(~(unorthogonal_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N))))) -> (~(convergent_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))) -> (forall N : zenon_U, ((((~(convergent_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)))\/(~(unorthogonal_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))))/\((~(convergent_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N))\/(~(unorthogonal_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N))))->((~(convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N))\/(~(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N))))) -> (forall L : zenon_U, (~(unorthogonal_lines (orthogonal_through_point L zenon_TA_bm) L))) -> False). % 1.15/1.34 do 2 intro. intros zenon_H4e zenon_H47 zenon_H39 zenon_H2c zenon_H35 zenon_H38 zenon_H31 zenon_H46 zenon_H2d. % 1.15/1.34 generalize (zenon_H2d zenon_TL_bn). zenon_intro zenon_H4f. % 1.15/1.34 generalize (occu1 (orthogonal_through_point zenon_TL_bn zenon_TA_bm)). zenon_intro zenon_H50. % 1.15/1.34 generalize (zenon_H50 zenon_TL_bn). zenon_intro zenon_H51. % 1.15/1.34 apply (zenon_or_s _ _ zenon_H51); [ zenon_intro zenon_H53 | zenon_intro zenon_H52 ]. % 1.15/1.34 generalize (zenon_H4e (orthogonal_through_point zenon_TL_bn zenon_TA_bm)). zenon_intro zenon_H54. % 1.15/1.34 generalize (zenon_H54 zenon_TL_bn). zenon_intro zenon_H55. % 1.15/1.34 apply (zenon_imply_s _ _ zenon_H55); [ zenon_intro zenon_H57 | zenon_intro zenon_H56 ]. % 1.15/1.34 apply (zenon_notand_s _ _ zenon_H57); [ zenon_intro zenon_H59 | zenon_intro zenon_H58 ]. % 1.15/1.34 apply zenon_H59. zenon_intro zenon_H2e. % 1.15/1.34 apply (zenon_L3_ zenon_TL_bn zenon_TA_bm); trivial. % 1.15/1.34 apply zenon_H58. zenon_intro zenon_H48. % 1.15/1.34 apply (zenon_L10_ zenon_TA_bm zenon_TL_bn); trivial. % 1.15/1.34 exact (zenon_H56 zenon_H53). % 1.15/1.34 exact (zenon_H4f zenon_H52). % 1.15/1.34 (* end of lemma zenon_L11_ *) % 1.15/1.34 assert (zenon_L12_ : forall (zenon_TA_bm : zenon_U) (zenon_TL_bn : zenon_U), (forall Z : zenon_U, ((convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))->((convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) Z)\/(convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) Z)))) -> (convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)) -> (~(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TL_bn)) -> (forall M : zenon_U, (forall N : zenon_U, (((~(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) M))/\(~(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N)))->(~(convergent_lines M N))))) -> (convergent_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) zenon_TL_bn) -> (~(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))) -> (forall N : zenon_U, ((((~(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)))\/(~(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))))/\((~(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) N))\/(~(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) N))))->((~(convergent_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N))\/(~(unorthogonal_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N))))) -> (~(convergent_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))) -> (forall N : zenon_U, ((((~(convergent_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)))\/(~(unorthogonal_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))))/\((~(convergent_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N))\/(~(unorthogonal_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N))))->((~(convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N))\/(~(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N))))) -> (forall L : zenon_U, (~(unorthogonal_lines (orthogonal_through_point L zenon_TA_bm) L))) -> False). % 1.15/1.34 do 2 intro. intros zenon_H5a zenon_H5b zenon_H2c zenon_H4e zenon_H39 zenon_H35 zenon_H38 zenon_H31 zenon_H46 zenon_H2d. % 1.15/1.34 generalize (zenon_H5a zenon_TL_bn). zenon_intro zenon_H5c. % 1.15/1.34 apply (zenon_imply_s _ _ zenon_H5c); [ zenon_intro zenon_H5e | zenon_intro zenon_H5d ]. % 1.15/1.34 exact (zenon_H5e zenon_H5b). % 1.15/1.34 apply (zenon_or_s _ _ zenon_H5d); [ zenon_intro zenon_H2b | zenon_intro zenon_H47 ]. % 1.15/1.34 exact (zenon_H2c zenon_H2b). % 1.15/1.34 apply (zenon_L11_ zenon_TA_bm zenon_TL_bn); trivial. % 1.15/1.34 (* end of lemma zenon_L12_ *) % 1.15/1.34 assert (zenon_L13_ : forall (zenon_TA_bm : zenon_U) (zenon_TL_bn : zenon_U), (forall N : zenon_U, (((~(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)))/\(~(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) N)))->(~(convergent_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N)))) -> (~(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))) -> (forall N : zenon_U, ((((~(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (parallel_through_point zenon_TL_bn zenon_TA_bm)))\/(~(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (parallel_through_point zenon_TL_bn zenon_TA_bm))))/\((~(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) N))\/(~(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) N))))->((~(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) N))\/(~(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) N))))) -> (~(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (parallel_through_point zenon_TL_bn zenon_TA_bm))) -> (forall Y : zenon_U, (~(convergent_lines (parallel_through_point Y zenon_TA_bm) Y))) -> (forall Z : zenon_U, ((convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))->((convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) Z)\/(convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) Z)))) -> (convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)) -> (forall M : zenon_U, (forall N : zenon_U, (((~(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) M))/\(~(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N)))->(~(convergent_lines M N))))) -> (convergent_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) zenon_TL_bn) -> (forall N : zenon_U, ((((~(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)))\/(~(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))))/\((~(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) N))\/(~(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) N))))->((~(convergent_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N))\/(~(unorthogonal_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N))))) -> (~(convergent_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))) -> (forall N : zenon_U, ((((~(convergent_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)))\/(~(unorthogonal_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))))/\((~(convergent_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N))\/(~(unorthogonal_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N))))->((~(convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N))\/(~(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N))))) -> (forall L : zenon_U, (~(unorthogonal_lines (orthogonal_through_point L zenon_TA_bm) L))) -> False). % 1.15/1.34 do 2 intro. intros zenon_H5f zenon_H35 zenon_H60 zenon_H25 zenon_H2a zenon_H5a zenon_H5b zenon_H4e zenon_H39 zenon_H38 zenon_H31 zenon_H46 zenon_H2d. % 1.15/1.34 generalize (zenon_H5f zenon_TL_bn). zenon_intro zenon_H61. % 1.15/1.34 apply (zenon_imply_s _ _ zenon_H61); [ zenon_intro zenon_H62 | zenon_intro zenon_H42 ]. % 1.15/1.34 apply (zenon_notand_s _ _ zenon_H62); [ zenon_intro zenon_H34 | zenon_intro zenon_H3f ]. % 1.15/1.34 exact (zenon_H34 zenon_H35). % 1.15/1.34 apply zenon_H3f. zenon_intro zenon_H63. % 1.15/1.34 generalize (zenon_H60 zenon_TL_bn). zenon_intro zenon_H64. % 1.15/1.34 apply (zenon_imply_s _ _ zenon_H64); [ zenon_intro zenon_H66 | zenon_intro zenon_H65 ]. % 1.15/1.34 apply (zenon_notand_s _ _ zenon_H66); [ zenon_intro zenon_H24 | zenon_intro zenon_H3e ]. % 1.15/1.34 apply (zenon_L1_ zenon_TA_bm zenon_TL_bn); trivial. % 1.15/1.34 apply (zenon_notor_s _ _ zenon_H3e). zenon_intro zenon_H40. zenon_intro zenon_H3f. % 1.15/1.34 apply zenon_H40. zenon_intro zenon_H2b. % 1.15/1.34 apply (zenon_L2_ zenon_TL_bn zenon_TA_bm); trivial. % 1.15/1.34 apply (zenon_or_s _ _ zenon_H65); [ zenon_intro zenon_H2c | zenon_intro zenon_H67 ]. % 1.15/1.34 apply (zenon_L12_ zenon_TA_bm zenon_TL_bn); trivial. % 1.15/1.34 exact (zenon_H67 zenon_H63). % 1.15/1.34 exact (zenon_H42 zenon_H39). % 1.15/1.34 (* end of lemma zenon_L13_ *) % 1.15/1.34 assert (zenon_L14_ : forall (zenon_TA_bm : zenon_U) (zenon_TL_bn : zenon_U), (forall M : zenon_U, (forall N : zenon_U, (((~(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) M))/\(~(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) N)))->(~(convergent_lines M N))))) -> (forall L : zenon_U, (~(unorthogonal_lines (orthogonal_through_point L zenon_TA_bm) L))) -> (forall N : zenon_U, ((((~(convergent_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)))\/(~(unorthogonal_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))))/\((~(convergent_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N))\/(~(unorthogonal_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N))))->((~(convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N))\/(~(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N))))) -> (~(convergent_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))) -> (forall N : zenon_U, ((((~(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)))\/(~(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))))/\((~(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) N))\/(~(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) N))))->((~(convergent_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N))\/(~(unorthogonal_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N))))) -> (forall M : zenon_U, (forall N : zenon_U, (((~(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) M))/\(~(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N)))->(~(convergent_lines M N))))) -> (convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)) -> (forall Z : zenon_U, ((convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))->((convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) Z)\/(convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) Z)))) -> (forall Y : zenon_U, (~(convergent_lines (parallel_through_point Y zenon_TA_bm) Y))) -> (~(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (parallel_through_point zenon_TL_bn zenon_TA_bm))) -> (forall N : zenon_U, ((((~(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (parallel_through_point zenon_TL_bn zenon_TA_bm)))\/(~(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (parallel_through_point zenon_TL_bn zenon_TA_bm))))/\((~(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) N))\/(~(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) N))))->((~(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) N))\/(~(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) N))))) -> (~(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))) -> (forall Y : zenon_U, ((distinct_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) Y)->(convergent_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) Y))) -> (convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)) -> (forall Z : zenon_U, ((convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))->((distinct_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) Z)\/(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) Z)))) -> False). % 1.15/1.34 do 2 intro. intros zenon_H68 zenon_H2d zenon_H46 zenon_H31 zenon_H38 zenon_H4e zenon_H5b zenon_H5a zenon_H2a zenon_H25 zenon_H60 zenon_H35 zenon_H69 zenon_H6a zenon_H6b. % 1.15/1.34 generalize (zenon_H68 (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)). zenon_intro zenon_H5f. % 1.15/1.34 generalize (zenon_H6b zenon_TL_bn). zenon_intro zenon_H6c. % 1.15/1.34 apply (zenon_imply_s _ _ zenon_H6c); [ zenon_intro zenon_H6e | zenon_intro zenon_H6d ]. % 1.15/1.34 exact (zenon_H6e zenon_H6a). % 1.15/1.34 apply (zenon_or_s _ _ zenon_H6d); [ zenon_intro zenon_H6f | zenon_intro zenon_H2b ]. % 1.15/1.34 generalize (zenon_H69 zenon_TL_bn). zenon_intro zenon_H70. % 1.15/1.34 apply (zenon_imply_s _ _ zenon_H70); [ zenon_intro zenon_H71 | zenon_intro zenon_H39 ]. % 1.15/1.34 exact (zenon_H71 zenon_H6f). % 1.15/1.34 apply (zenon_L13_ zenon_TA_bm zenon_TL_bn); trivial. % 1.15/1.34 apply (zenon_L2_ zenon_TL_bn zenon_TA_bm); trivial. % 1.15/1.34 (* end of lemma zenon_L14_ *) % 1.15/1.34 assert (zenon_L15_ : forall (zenon_TA_bm : zenon_U) (zenon_TL_bn : zenon_U), ((convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (parallel_through_point zenon_TL_bn zenon_TA_bm))/\(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (parallel_through_point zenon_TL_bn zenon_TA_bm))) -> (~(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (parallel_through_point zenon_TL_bn zenon_TA_bm))) -> False). % 1.15/1.34 do 2 intro. intros zenon_H72 zenon_H25. % 1.15/1.34 apply (zenon_and_s _ _ zenon_H72). zenon_intro zenon_H74. zenon_intro zenon_H73. % 1.15/1.34 exact (zenon_H25 zenon_H74). % 1.15/1.34 (* end of lemma zenon_L15_ *) % 1.15/1.34 assert (zenon_L16_ : forall (zenon_TA_bm : zenon_U) (zenon_TL_bn : zenon_U), ((convergent_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (parallel_through_point zenon_TL_bn zenon_TA_bm))/\(unorthogonal_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (parallel_through_point zenon_TL_bn zenon_TA_bm))) -> (~(unorthogonal_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (parallel_through_point zenon_TL_bn zenon_TA_bm))) -> False). % 1.15/1.34 do 2 intro. intros zenon_H75 zenon_H76. % 1.15/1.34 apply (zenon_and_s _ _ zenon_H75). zenon_intro zenon_H78. zenon_intro zenon_H77. % 1.15/1.34 exact (zenon_H76 zenon_H77). % 1.15/1.34 (* end of lemma zenon_L16_ *) % 1.15/1.34 assert (zenon_L17_ : forall (zenon_TA_bm : zenon_U) (zenon_TL_bn : zenon_U), (forall M : zenon_U, (forall N : zenon_U, (((convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) M)/\(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) M))->(((convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) N)/\(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) N))\/((convergent_lines M N)/\(unorthogonal_lines M N)))))) -> (~(unorthogonal_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (parallel_through_point zenon_TL_bn zenon_TA_bm))) -> (~(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (parallel_through_point zenon_TL_bn zenon_TA_bm))) -> (forall Y : zenon_U, (~(convergent_lines (parallel_through_point Y zenon_TA_bm) Y))) -> (forall Z : zenon_U, ((convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))->((convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) Z)\/(convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) Z)))) -> (convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)) -> (forall M : zenon_U, (forall N : zenon_U, (((~(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) M))/\(~(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N)))->(~(convergent_lines M N))))) -> (~(convergent_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))) -> (forall L : zenon_U, (~(unorthogonal_lines (orthogonal_through_point L zenon_TA_bm) L))) -> (forall Y : zenon_U, (forall Z : zenon_U, ((convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) Y)->((distinct_lines Y Z)\/(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) Z))))) -> (~(convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))) -> (convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (parallel_through_point zenon_TL_bn zenon_TA_bm)) -> (forall Z : zenon_U, ((convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (parallel_through_point zenon_TL_bn zenon_TA_bm))->((convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) Z)\/(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) Z)))) -> False). % 1.15/1.34 do 2 intro. intros zenon_H79 zenon_H76 zenon_H25 zenon_H2a zenon_H5a zenon_H5b zenon_H4e zenon_H31 zenon_H2d zenon_H7a zenon_H7b zenon_H7c zenon_H7d. % 1.15/1.34 generalize (p1 (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)). zenon_intro zenon_H69. % 1.15/1.34 generalize (zenon_H7d (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)). zenon_intro zenon_H7e. % 1.15/1.34 apply (zenon_imply_s _ _ zenon_H7e); [ zenon_intro zenon_H80 | zenon_intro zenon_H7f ]. % 1.15/1.34 exact (zenon_H80 zenon_H7c). % 1.15/1.34 apply (zenon_or_s _ _ zenon_H7f); [ zenon_intro zenon_H81 | zenon_intro zenon_H6a ]. % 1.15/1.34 exact (zenon_H7b zenon_H81). % 1.15/1.34 generalize (zenon_H7a (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)). zenon_intro zenon_H6b. % 1.15/1.34 generalize (cotno1 (parallel_through_point zenon_TL_bn zenon_TA_bm)). zenon_intro zenon_H82. % 1.15/1.34 generalize (zenon_H82 (parallel_through_point zenon_TL_bn zenon_TA_bm)). zenon_intro zenon_H60. % 1.15/1.34 generalize (zenon_H82 (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)). zenon_intro zenon_H38. % 1.15/1.34 generalize (cotno1 (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)). zenon_intro zenon_H83. % 1.15/1.34 generalize (couo1 (parallel_through_point zenon_TL_bn zenon_TA_bm)). zenon_intro zenon_H68. % 1.15/1.34 generalize (zenon_H83 (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)). zenon_intro zenon_H46. % 1.15/1.34 generalize (zenon_H79 (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)). zenon_intro zenon_H84. % 1.15/1.34 generalize (zenon_H84 (parallel_through_point zenon_TL_bn zenon_TA_bm)). zenon_intro zenon_H85. % 1.15/1.34 apply (zenon_imply_s _ _ zenon_H85); [ zenon_intro zenon_H87 | zenon_intro zenon_H86 ]. % 1.15/1.34 apply (zenon_notand_s _ _ zenon_H87); [ zenon_intro zenon_H6e | zenon_intro zenon_H35 ]. % 1.15/1.34 exact (zenon_H6e zenon_H6a). % 1.15/1.34 apply (zenon_L14_ zenon_TA_bm zenon_TL_bn); trivial. % 1.15/1.34 apply (zenon_or_s _ _ zenon_H86); [ zenon_intro zenon_H72 | zenon_intro zenon_H75 ]. % 1.15/1.34 apply (zenon_L15_ zenon_TA_bm zenon_TL_bn); trivial. % 1.15/1.34 apply (zenon_L16_ zenon_TA_bm zenon_TL_bn); trivial. % 1.15/1.34 (* end of lemma zenon_L17_ *) % 1.15/1.34 assert (zenon_L18_ : forall (zenon_TA_bm : zenon_U) (zenon_TL_bn : zenon_U), ((convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (parallel_through_point zenon_TL_bn zenon_TA_bm))/\(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (parallel_through_point zenon_TL_bn zenon_TA_bm))) -> (~(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (parallel_through_point zenon_TL_bn zenon_TA_bm))) -> False). % 1.15/1.34 do 2 intro. intros zenon_H88 zenon_H89. % 1.15/1.34 apply (zenon_and_s _ _ zenon_H88). zenon_intro zenon_H7c. zenon_intro zenon_H8a. % 1.15/1.34 exact (zenon_H89 zenon_H8a). % 1.15/1.34 (* end of lemma zenon_L18_ *) % 1.15/1.34 assert (zenon_L19_ : forall (zenon_TA_bm : zenon_U) (zenon_TL_bn : zenon_U), (forall M : zenon_U, (forall N : zenon_U, (((convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) M)/\(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) M))->(((convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N)/\(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N))\/((convergent_lines M N)/\(unorthogonal_lines M N)))))) -> (~(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (parallel_through_point zenon_TL_bn zenon_TA_bm))) -> (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)) -> (forall Z : zenon_U, ((convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (parallel_through_point zenon_TL_bn zenon_TA_bm))->((convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) Z)\/(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) Z)))) -> (convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (parallel_through_point zenon_TL_bn zenon_TA_bm)) -> (forall Y : zenon_U, (forall Z : zenon_U, ((convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) Y)->((distinct_lines Y Z)\/(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) Z))))) -> (forall L : zenon_U, (~(unorthogonal_lines (orthogonal_through_point L zenon_TA_bm) L))) -> (~(convergent_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))) -> (forall M : zenon_U, (forall N : zenon_U, (((~(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) M))/\(~(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) N)))->(~(convergent_lines M N))))) -> (convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)) -> (forall Z : zenon_U, ((convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))->((convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) Z)\/(convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) Z)))) -> (forall Y : zenon_U, (~(convergent_lines (parallel_through_point Y zenon_TA_bm) Y))) -> (~(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (parallel_through_point zenon_TL_bn zenon_TA_bm))) -> (~(unorthogonal_lines (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (parallel_through_point zenon_TL_bn zenon_TA_bm))) -> (forall M : zenon_U, (forall N : zenon_U, (((convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) M)/\(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) M))->(((convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) N)/\(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) N))\/((convergent_lines M N)/\(unorthogonal_lines M N)))))) -> False). % 1.15/1.34 do 2 intro. intros zenon_H8b zenon_H89 zenon_H8c zenon_H7d zenon_H7c zenon_H7a zenon_H2d zenon_H31 zenon_H4e zenon_H5b zenon_H5a zenon_H2a zenon_H25 zenon_H76 zenon_H79. % 1.15/1.34 generalize (zenon_H8b (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)). zenon_intro zenon_H8d. % 1.15/1.34 generalize (zenon_H8d (parallel_through_point zenon_TL_bn zenon_TA_bm)). zenon_intro zenon_H8e. % 1.15/1.34 apply (zenon_imply_s _ _ zenon_H8e); [ zenon_intro zenon_H90 | zenon_intro zenon_H8f ]. % 1.15/1.34 apply (zenon_notand_s _ _ zenon_H90); [ zenon_intro zenon_H7b | zenon_intro zenon_H91 ]. % 1.15/1.34 apply (zenon_L17_ zenon_TA_bm zenon_TL_bn); trivial. % 1.15/1.34 exact (zenon_H91 zenon_H8c). % 1.15/1.34 apply (zenon_or_s _ _ zenon_H8f); [ zenon_intro zenon_H88 | zenon_intro zenon_H75 ]. % 1.15/1.34 apply (zenon_L18_ zenon_TA_bm zenon_TL_bn); trivial. % 1.15/1.34 apply (zenon_L16_ zenon_TA_bm zenon_TL_bn); trivial. % 1.15/1.34 (* end of lemma zenon_L19_ *) % 1.15/1.34 assert (zenon_L20_ : forall (zenon_TA_bm : zenon_U) (zenon_TL_bn : zenon_U), (~(convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))) -> (forall M : zenon_U, (forall N : zenon_U, (((convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) M)/\(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) M))->(((convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) N)/\(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) N))\/((convergent_lines M N)/\(unorthogonal_lines M N)))))) -> (~(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (parallel_through_point zenon_TL_bn zenon_TA_bm))) -> (forall Y : zenon_U, (~(convergent_lines (parallel_through_point Y zenon_TA_bm) Y))) -> (forall Z : zenon_U, ((convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))->((convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) Z)\/(convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) Z)))) -> (convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)) -> (forall Y : zenon_U, (forall Z : zenon_U, ((convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) Y)->((distinct_lines Y Z)\/(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) Z))))) -> (convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (parallel_through_point zenon_TL_bn zenon_TA_bm)) -> (forall Z : zenon_U, ((convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (parallel_through_point zenon_TL_bn zenon_TA_bm))->((convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) Z)\/(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) Z)))) -> (~(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (parallel_through_point zenon_TL_bn zenon_TA_bm))) -> False). % 1.15/1.34 do 2 intro. intros zenon_H92 zenon_H79 zenon_H25 zenon_H2a zenon_H5a zenon_H5b zenon_H7a zenon_H7c zenon_H7d zenon_H89. % 1.15/1.34 generalize (couo1 (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)). zenon_intro zenon_H4e. % 1.15/1.34 generalize (ooc1 zenon_TA_bm). zenon_intro zenon_H2d. % 1.15/1.34 generalize (zenon_H2d (parallel_through_point zenon_TL_bn zenon_TA_bm)). zenon_intro zenon_H76. % 1.15/1.34 generalize (oac1 (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)). zenon_intro zenon_H8b. % 1.15/1.34 generalize (occu1 (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)). zenon_intro zenon_H93. % 1.15/1.34 generalize (zenon_H93 (parallel_through_point zenon_TL_bn zenon_TA_bm)). zenon_intro zenon_H94. % 1.15/1.34 apply (zenon_or_s _ _ zenon_H94); [ zenon_intro zenon_H78 | zenon_intro zenon_H77 ]. % 1.15/1.34 generalize (couo1 (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)). zenon_intro zenon_H95. % 1.15/1.34 generalize (ax6 (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)). zenon_intro zenon_H96. % 1.15/1.34 generalize (zenon_H95 (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)). zenon_intro zenon_H97. % 1.15/1.34 generalize (zenon_H97 (parallel_through_point zenon_TL_bn zenon_TA_bm)). zenon_intro zenon_H98. % 1.15/1.34 apply (zenon_imply_s _ _ zenon_H98); [ zenon_intro zenon_H99 | zenon_intro zenon_H80 ]. % 1.15/1.34 apply (zenon_notand_s _ _ zenon_H99); [ zenon_intro zenon_H32 | zenon_intro zenon_H9a ]. % 1.15/1.34 apply zenon_H32. zenon_intro zenon_H9b. % 1.15/1.34 generalize (zenon_H96 (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)). zenon_intro zenon_H9c. % 1.15/1.34 generalize (zenon_H4e (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)). zenon_intro zenon_H9d. % 1.15/1.34 generalize (zenon_H9d (parallel_through_point zenon_TL_bn zenon_TA_bm)). zenon_intro zenon_H9e. % 1.15/1.34 apply (zenon_imply_s _ _ zenon_H9e); [ zenon_intro zenon_Ha0 | zenon_intro zenon_H9f ]. % 1.15/1.34 apply (zenon_notand_s _ _ zenon_Ha0); [ zenon_intro zenon_Ha2 | zenon_intro zenon_Ha1 ]. % 1.15/1.34 apply zenon_Ha2. zenon_intro zenon_H8c. % 1.15/1.34 generalize (oac1 (orthogonal_through_point (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)). zenon_intro zenon_Ha3. % 1.15/1.34 generalize (zenon_H9c (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)). zenon_intro zenon_Ha4. % 1.15/1.34 apply (zenon_imply_s _ _ zenon_Ha4); [ zenon_intro zenon_H31 | zenon_intro zenon_Ha5 ]. % 1.15/1.34 apply (zenon_L19_ zenon_TA_bm zenon_TL_bn); trivial. % 1.15/1.34 apply (zenon_or_s _ _ zenon_Ha5); [ zenon_intro zenon_Ha7 | zenon_intro zenon_Ha6 ]. % 1.15/1.34 generalize (zenon_Ha3 (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)). zenon_intro zenon_Ha8. % 1.15/1.34 generalize (zenon_Ha8 (parallel_through_point zenon_TL_bn zenon_TA_bm)). zenon_intro zenon_Ha9. % 1.15/1.34 apply (zenon_imply_s _ _ zenon_Ha9); [ zenon_intro zenon_Hab | zenon_intro zenon_Haa ]. % 1.15/1.34 apply (zenon_notand_s _ _ zenon_Hab); [ zenon_intro zenon_H31 | zenon_intro zenon_Hac ]. % 1.15/1.34 exact (zenon_H31 zenon_Ha7). % 1.15/1.34 exact (zenon_Hac zenon_H9b). % 1.15/1.34 apply (zenon_or_s _ _ zenon_Haa); [ zenon_intro zenon_H75 | zenon_intro zenon_H88 ]. % 1.15/1.34 apply (zenon_L16_ zenon_TA_bm zenon_TL_bn); trivial. % 1.15/1.34 apply (zenon_L18_ zenon_TA_bm zenon_TL_bn); trivial. % 1.15/1.34 exact (zenon_H92 zenon_Ha6). % 1.15/1.34 exact (zenon_Ha1 zenon_H89). % 1.15/1.34 exact (zenon_H9f zenon_H78). % 1.15/1.34 exact (zenon_H9a zenon_H76). % 1.15/1.34 exact (zenon_H80 zenon_H7c). % 1.15/1.34 exact (zenon_H76 zenon_H77). % 1.15/1.34 (* end of lemma zenon_L20_ *) % 1.15/1.34 assert (zenon_L21_ : forall (zenon_TA_bm : zenon_U) (zenon_TL_bn : zenon_U), (~(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (parallel_through_point zenon_TL_bn zenon_TA_bm))) -> (forall Z : zenon_U, ((convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (parallel_through_point zenon_TL_bn zenon_TA_bm))->((convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) Z)\/(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) Z)))) -> (convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (parallel_through_point zenon_TL_bn zenon_TA_bm)) -> (forall Y : zenon_U, (forall Z : zenon_U, ((convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) Y)->((distinct_lines Y Z)\/(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) Z))))) -> (convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)) -> (forall Z : zenon_U, ((convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))->((convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) Z)\/(convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) Z)))) -> (forall Y : zenon_U, (~(convergent_lines (parallel_through_point Y zenon_TA_bm) Y))) -> (~(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (parallel_through_point zenon_TL_bn zenon_TA_bm))) -> (~(convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))) -> False). % 1.15/1.34 do 2 intro. intros zenon_H89 zenon_H7d zenon_H7c zenon_H7a zenon_H5b zenon_H5a zenon_H2a zenon_H25 zenon_H92. % 1.15/1.34 generalize (oac1 (parallel_through_point zenon_TL_bn zenon_TA_bm)). zenon_intro zenon_H79. % 1.15/1.34 apply (zenon_L20_ zenon_TA_bm zenon_TL_bn); trivial. % 1.15/1.34 (* end of lemma zenon_L21_ *) % 1.15/1.34 assert (zenon_L22_ : forall (zenon_TA_bm : zenon_U) (zenon_TL_bn : zenon_U), ((convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))/\(unorthogonal_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))) -> (~(convergent_lines (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm) (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm))) -> False). % 1.15/1.34 do 2 intro. intros zenon_Had zenon_H92. % 1.15/1.34 apply (zenon_and_s _ _ zenon_Had). zenon_intro zenon_Ha6. zenon_intro zenon_Hae. % 1.15/1.34 exact (zenon_H92 zenon_Ha6). % 1.15/1.34 (* end of lemma zenon_L22_ *) % 1.15/1.34 assert (zenon_L23_ : forall (zenon_TA_bm : zenon_U) (zenon_TL_bn : zenon_U), ((convergent_lines (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TL_bn)/\(unorthogonal_lines (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TL_bn)) -> (~(unorthogonal_lines (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TL_bn)) -> False). % 1.15/1.34 do 2 intro. intros zenon_Haf zenon_H4f. % 1.15/1.34 apply (zenon_and_s _ _ zenon_Haf). zenon_intro zenon_H53. zenon_intro zenon_H52. % 1.15/1.34 exact (zenon_H4f zenon_H52). % 1.15/1.34 (* end of lemma zenon_L23_ *) % 1.15/1.34 assert (zenon_L24_ : forall (zenon_TA_bm : zenon_U) (zenon_TL_bn : zenon_U), (forall M : zenon_U, (forall N : zenon_U, (((convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) M)/\(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) M))->(((convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) N)/\(unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) N))\/((convergent_lines M N)/\(unorthogonal_lines M N)))))) -> (~(unorthogonal_lines (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TL_bn)) -> (~(convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) zenon_TL_bn)) -> (unorthogonal_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point zenon_TL_bn zenon_TA_bm)) -> (convergent_lines (parallel_through_point zenon_TL_bn zenon_TA_bm) (orthogonal_through_point zenon_TL_bn zenon_TA_bm)) -> False). % 1.15/1.34 do 2 intro. intros zenon_H79 zenon_H4f zenon_H2c zenon_Hb0 zenon_Hb1. % 1.15/1.34 generalize (zenon_H79 (orthogonal_through_point zenon_TL_bn zenon_TA_bm)). zenon_intro zenon_Hb2. % 1.15/1.34 generalize (zenon_Hb2 zenon_TL_bn). zenon_intro zenon_Hb3. % 1.15/1.34 apply (zenon_imply_s _ _ zenon_Hb3); [ zenon_intro zenon_Hb5 | zenon_intro zenon_Hb4 ]. % 1.15/1.34 apply (zenon_notand_s _ _ zenon_Hb5); [ zenon_intro zenon_Hb7 | zenon_intro zenon_Hb6 ]. % 1.15/1.34 exact (zenon_Hb7 zenon_Hb1). % 1.15/1.34 exact (zenon_Hb6 zenon_Hb0). % 1.15/1.34 apply (zenon_or_s _ _ zenon_Hb4); [ zenon_intro zenon_Hb8 | zenon_intro zenon_Haf ]. % 1.15/1.34 apply (zenon_and_s _ _ zenon_Hb8). zenon_intro zenon_H2b. zenon_intro zenon_H63. % 1.15/1.34 exact (zenon_H2c zenon_H2b). % 1.15/1.34 apply (zenon_L23_ zenon_TA_bm zenon_TL_bn); trivial. % 1.15/1.34 (* end of lemma zenon_L24_ *) % 1.15/1.34 apply NNPP. intro zenon_G. % 1.15/1.34 apply (zenon_notallex_s (fun A : zenon_U => (forall L : zenon_U, (equal_lines (parallel_through_point L A) (orthogonal_through_point (orthogonal_through_point L A) A)))) zenon_G); [ zenon_intro zenon_Hb9; idtac ]. % 1.15/1.34 elim zenon_Hb9. zenon_intro zenon_TA_bm. zenon_intro zenon_Hba. % 1.15/1.34 apply (zenon_notallex_s (fun L : zenon_U => (equal_lines (parallel_through_point L zenon_TA_bm) (orthogonal_through_point (orthogonal_through_point L zenon_TA_bm) zenon_TA_bm))) zenon_Hba); [ zenon_intro zenon_Hbb; idtac ]. % 1.15/1.34 elim zenon_Hbb. zenon_intro zenon_TL_bn. zenon_intro zenon_Hbc. % 1.15/1.34 generalize (ax2 (parallel_through_point zenon_TL_bn zenon_TA_bm)). zenon_intro zenon_Hbd. % 1.15/1.34 generalize (zenon_Hbd (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)). zenon_intro zenon_Hbe. % 1.15/1.34 apply (zenon_equiv_s _ _ zenon_Hbe); [ zenon_intro zenon_Hbc; zenon_intro zenon_Hc1 | zenon_intro zenon_Hc0; zenon_intro zenon_Hbf ]. % 1.15/1.34 apply zenon_Hc1. zenon_intro zenon_Hc2. % 1.15/1.34 generalize (apart5 (parallel_through_point zenon_TL_bn zenon_TA_bm)). zenon_intro zenon_Hc3. % 1.15/1.34 generalize (apart3 (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)). zenon_intro zenon_H92. % 1.15/1.34 generalize (zenon_Hc3 (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)). zenon_intro zenon_Hc4. % 1.15/1.34 generalize (ooc2 zenon_TA_bm). zenon_intro zenon_Hc5. % 1.15/1.34 generalize (zenon_Hc5 (orthogonal_through_point zenon_TL_bn zenon_TA_bm)). zenon_intro zenon_Hc6. % 1.15/1.34 generalize (cup1 zenon_TA_bm). zenon_intro zenon_Hc7. % 1.15/1.34 generalize (zenon_Hc7 (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)). zenon_intro zenon_Hc8. % 1.15/1.34 generalize (apart2 (parallel_through_point zenon_TL_bn zenon_TA_bm)). zenon_intro zenon_Hc9. % 1.15/1.34 generalize (zenon_Hc4 (parallel_through_point zenon_TL_bn zenon_TA_bm)). zenon_intro zenon_Hca. % 1.15/1.34 apply (zenon_imply_s _ _ zenon_Hca); [ zenon_intro zenon_Hbf | zenon_intro zenon_Hcb ]. % 1.15/1.34 exact (zenon_Hbf zenon_Hc2). % 1.15/1.34 apply (zenon_or_s _ _ zenon_Hcb); [ zenon_intro zenon_Hcd | zenon_intro zenon_Hcc ]. % 1.15/1.34 exact (zenon_Hc9 zenon_Hcd). % 1.15/1.34 generalize (zenon_Hc8 (parallel_through_point zenon_TL_bn zenon_TA_bm)). zenon_intro zenon_Hce. % 1.15/1.34 apply (zenon_imply_s _ _ zenon_Hce); [ zenon_intro zenon_Hd0 | zenon_intro zenon_Hcf ]. % 1.15/1.34 exact (zenon_Hd0 zenon_Hcc). % 1.15/1.34 apply (zenon_or_s _ _ zenon_Hcf); [ zenon_intro zenon_Hd2 | zenon_intro zenon_Hd1 ]. % 1.15/1.34 exact (zenon_Hc6 zenon_Hd2). % 1.15/1.34 apply (zenon_or_s _ _ zenon_Hd1); [ zenon_intro zenon_Hd3 | zenon_intro zenon_H7c ]. % 1.15/1.34 generalize (cp2 zenon_TA_bm). zenon_intro zenon_Hd4. % 1.15/1.34 generalize (zenon_Hd4 zenon_TL_bn). zenon_intro zenon_Hd5. % 1.15/1.34 exact (zenon_Hd5 zenon_Hd3). % 1.15/1.34 generalize (apart3 (parallel_through_point zenon_TL_bn zenon_TA_bm)). zenon_intro zenon_H25. % 1.15/1.34 generalize (ax6 (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)). zenon_intro zenon_Hd6. % 1.15/1.34 generalize (zenon_Hd6 (parallel_through_point zenon_TL_bn zenon_TA_bm)). zenon_intro zenon_H7d. % 1.15/1.34 generalize (zenon_H7d (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)). zenon_intro zenon_Hd7. % 1.15/1.34 apply (zenon_imply_s _ _ zenon_Hd7); [ zenon_intro zenon_H80 | zenon_intro zenon_Hd8 ]. % 1.15/1.34 exact (zenon_H80 zenon_H7c). % 1.15/1.34 apply (zenon_or_s _ _ zenon_Hd8); [ zenon_intro zenon_Ha6 | zenon_intro zenon_H5b ]. % 1.15/1.34 exact (zenon_H92 zenon_Ha6). % 1.15/1.34 generalize (cp1 zenon_TA_bm). zenon_intro zenon_H2a. % 1.15/1.34 generalize (ax6 (parallel_through_point zenon_TL_bn zenon_TA_bm)). zenon_intro zenon_Hd9. % 1.15/1.34 generalize (ceq3 (parallel_through_point zenon_TL_bn zenon_TA_bm)). zenon_intro zenon_H7a. % 1.15/1.34 generalize (zenon_Hd9 (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)). zenon_intro zenon_H5a. % 1.15/1.34 generalize (oac1 (parallel_through_point zenon_TL_bn zenon_TA_bm)). zenon_intro zenon_H79. % 1.15/1.34 generalize (oac1 (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)). zenon_intro zenon_H8b. % 1.15/1.34 generalize (zenon_H8b (parallel_through_point zenon_TL_bn zenon_TA_bm)). zenon_intro zenon_Hda. % 1.15/1.34 generalize (zenon_Hda (parallel_through_point zenon_TL_bn zenon_TA_bm)). zenon_intro zenon_Hdb. % 1.15/1.34 apply (zenon_imply_s _ _ zenon_Hdb); [ zenon_intro zenon_Hdd | zenon_intro zenon_Hdc ]. % 1.15/1.34 apply (zenon_notand_s _ _ zenon_Hdd); [ zenon_intro zenon_H80 | zenon_intro zenon_H89 ]. % 1.15/1.34 exact (zenon_H80 zenon_H7c). % 1.15/1.34 apply (zenon_L21_ zenon_TA_bm zenon_TL_bn); trivial. % 1.15/1.34 apply (zenon_or_s _ _ zenon_Hdc); [ zenon_intro zenon_H88 | zenon_intro zenon_H72 ]. % 1.15/1.34 apply (zenon_and_s _ _ zenon_H88). zenon_intro zenon_H7c. zenon_intro zenon_H8a. % 1.15/1.34 generalize (ooc1 zenon_TA_bm). zenon_intro zenon_H2d. % 1.15/1.34 generalize (zenon_H79 (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)). zenon_intro zenon_Hde. % 1.15/1.34 generalize (zenon_Hda (orthogonal_through_point (orthogonal_through_point zenon_TL_bn zenon_TA_bm) zenon_TA_bm)). zenon_intro zenon_Hdf. % 1.15/1.34 apply (zenon_imply_s _ _ zenon_Hdf); [ zenon_intro zenon_Hdd | zenon_intro zenon_He0 ]. % 1.15/1.34 apply (zenon_notand_s _ _ zenon_Hdd); [ zenon_intro zenon_H80 | zenon_intro zenon_H89 ]. % 1.15/1.34 exact (zenon_H80 zenon_H7c). % 1.15/1.34 exact (zenon_H89 zenon_H8a). % 1.15/1.34 apply (zenon_or_s _ _ zenon_He0); [ zenon_intro zenon_Had | zenon_intro zenon_He1 ]. % 1.15/1.34 apply (zenon_L22_ zenon_TA_bm zenon_TL_bn); trivial. % 1.15/1.34 apply (zenon_and_s _ _ zenon_He1). zenon_intro zenon_H5b. zenon_intro zenon_He2. % 1.15/1.34 generalize (zenon_H2a zenon_TL_bn). zenon_intro zenon_H2c. % 1.15/1.34 generalize (zenon_H2d zenon_TL_bn). zenon_intro zenon_H4f. % 1.15/1.34 generalize (zenon_Hde (orthogonal_through_point zenon_TL_bn zenon_TA_bm)). zenon_intro zenon_He3. % 1.15/1.34 apply (zenon_imply_s _ _ zenon_He3); [ zenon_intro zenon_He5 | zenon_intro zenon_He4 ]. % 1.15/1.34 apply (zenon_notand_s _ _ zenon_He5); [ zenon_intro zenon_H5e | zenon_intro zenon_He6 ]. % 1.15/1.34 exact (zenon_H5e zenon_H5b). % 1.15/1.34 exact (zenon_He6 zenon_He2). % 1.15/1.34 apply (zenon_or_s _ _ zenon_He4); [ zenon_intro zenon_He8 | zenon_intro zenon_He7 ]. % 1.15/1.34 apply (zenon_and_s _ _ zenon_He8). zenon_intro zenon_Hb1. zenon_intro zenon_Hb0. % 1.15/1.34 apply (zenon_L24_ zenon_TA_bm zenon_TL_bn); trivial. % 1.15/1.34 apply (zenon_and_s _ _ zenon_He7). zenon_intro zenon_He9. zenon_intro zenon_H2e. % 1.15/1.34 apply (zenon_L3_ zenon_TL_bn zenon_TA_bm); trivial. % 1.15/1.34 apply (zenon_L15_ zenon_TA_bm zenon_TL_bn); trivial. % 1.15/1.34 exact (zenon_Hbc zenon_Hc0). % 1.15/1.34 Qed. % 1.15/1.34 % SZS output end Proof % 1.15/1.34 (* END-PROOF *) % 1.15/1.34 nodes searched: 87832 % 1.15/1.34 max branch formulas: 6772 % 1.15/1.34 proof nodes created: 2874 % 1.15/1.34 formulas created: 192466 % 1.15/1.34 %------------------------------------------------------------------------------