:: HOMOTHET  semantic presentation begin  






































theorem :: HOMOTHET:1 (Bool  "for" (Set (Var "AFP")) "being"   ($#l1_analoaf :::"AffinPlane":::)  (Bool  "for" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "b")) "," (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "p9")) "," (Set (Var "q")) "," (Set (Var "q9")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFP"))  "st" (Bool (Bool (Bool  "not"   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "p")))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "x"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "y"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "o")) "," (Set (Var "p")) "," (Set (Var "p9"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "o")) "," (Set (Var "p")) "," (Set (Var "q"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "o")) "," (Set (Var "p")) "," (Set (Var "q9"))) & (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q"))) & (Bool (Set (Var "o"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q"))) & (Bool (Set (Var "o"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x"))) & (Bool (Set (Var "a")) "," (Set (Var "p"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "p9"))) & (Bool (Set (Var "a")) "," (Set (Var "q"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "q9"))) & (Bool (Set (Var "x")) "," (Set (Var "p"))  ($#r2_analoaf :::"//"::: )  (Set (Var "y")) "," (Set (Var "p9"))) & (Bool (Set (Var "AFP")) "is"   ($#v4_aff_2 :::"Desarguesian"::: )  )) "holds"  (Bool (Set (Var "x")) "," (Set (Var "q"))  ($#r2_analoaf :::"//"::: )  (Set (Var "y")) "," (Set (Var "q9"))))) ; 
 
theorem :: HOMOTHET:2 (Bool  "for" (Set (Var "AFP")) "being"   ($#l1_analoaf :::"AffinPlane":::)  "st" (Bool (Bool  "("   "for" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFP"))  "st" (Bool (Bool (Set (Var "o"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a"))) & (Bool (Set (Var "o"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b")))) "holds"  (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Permutation":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "AFP"))) "st"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v6_transgeo :::"dilatation"::: )  ) & (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "o")))  ($#r1_hidden :::"="::: )  (Set (Var "o"))) & (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "b")))  ")" ))  ")" )) "holds"  (Bool (Set (Var "AFP")) "is"   ($#v4_aff_2 :::"Desarguesian"::: )  )) ; 
 
theorem :: HOMOTHET:3 (Bool  "for" (Set (Var "AFP")) "being"   ($#l1_analoaf :::"AffinPlane":::)  "st" (Bool (Bool (Set (Var "AFP")) "is"   ($#v4_aff_2 :::"Desarguesian"::: )  )) "holds"  (Bool  "for" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFP"))  "st" (Bool (Bool (Set (Var "o"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a"))) & (Bool (Set (Var "o"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b")))) "holds"  (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Permutation":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "AFP"))) "st"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v6_transgeo :::"dilatation"::: )  ) & (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "o")))  ($#r1_hidden :::"="::: )  (Set (Var "o"))) & (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "b")))  ")" )))) ; 
 
theorem :: HOMOTHET:4 (Bool  "for" (Set (Var "AFP")) "being"   ($#l1_analoaf :::"AffinPlane":::) "holds"   (Bool  "("  (Bool (Set (Var "AFP")) "is"   ($#v4_aff_2 :::"Desarguesian"::: )  ) "iff" (Bool  "for" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFP"))  "st" (Bool (Bool (Set (Var "o"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a"))) & (Bool (Set (Var "o"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b")))) "holds"  (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Permutation":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "AFP"))) "st"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v6_transgeo :::"dilatation"::: )  ) & (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "o")))  ($#r1_hidden :::"="::: )  (Set (Var "o"))) & (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "b")))  ")" )))  ")" )) ; 
 definitionlet "AFP" be   ($#l1_analoaf :::"AffinPlane":::); let "f" be   ($#m1_subset_1 :::"Permutation":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Const "AFP"))); let "K" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "AFP")); pred "f" :::"is_Sc"::: "K" means :: HOMOTHET:def 1 (Bool  "("  (Bool "f" "is"   ($#v8_transgeo :::"collineation"::: )  ) & (Bool "K" "is"   ($#v1_aff_1 :::"being_line"::: )  ) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" "AFP"  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "K")) "holds"  (Bool (Set "f"  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "x")))  ")" ) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" "AFP" "holds"  (Bool (Set (Var "x")) "," (Set "f"  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r2_aff_1 :::"//"::: )  "K")  ")" )  ")" ); end; 






:: deftheorem    defines :::"is_Sc"::: HOMOTHET:def 1 :  (Bool  "for" (Set (Var "AFP")) "being"   ($#l1_analoaf :::"AffinPlane":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Permutation":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "AFP")))  (Bool  "for" (Set (Var "K")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AFP")) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r1_homothet :::"is_Sc"::: )  (Set (Var "K"))) "iff" (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v8_transgeo :::"collineation"::: )  ) & (Bool (Set (Var "K")) "is"   ($#v1_aff_1 :::"being_line"::: )  ) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFP"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "K")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "x")))  ")" ) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFP")) "holds"  (Bool (Set (Var "x")) "," (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r2_aff_1 :::"//"::: )  (Set (Var "K")))  ")" )  ")" )  ")" )))); 
 
theorem :: HOMOTHET:5 (Bool  "for" (Set (Var "AFP")) "being"   ($#l1_analoaf :::"AffinPlane":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFP"))  (Bool  "for" (Set (Var "K")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AFP"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Permutation":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "AFP")))  "st" (Bool (Bool (Set (Var "f"))  ($#r1_homothet :::"is_Sc"::: )  (Set (Var "K"))) & (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "p"))) & (Bool (Bool  "not" (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "K"))))) "holds"  (Bool (Set (Var "f"))  ($#r2_relset_1 :::"="::: )  (Set   ($#k6_partfun1 :::"id"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "AFP"))))))))) ; 
 
theorem :: HOMOTHET:6 (Bool  "for" (Set (Var "AFP")) "being"   ($#l1_analoaf :::"AffinPlane":::)  "st" (Bool (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFP"))  (Bool  "for" (Set (Var "K")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AFP"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_aff_1 :::"//"::: )  (Set (Var "K"))) & (Bool (Bool  "not" (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "K"))))) "holds"  (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Permutation":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "AFP"))) "st"  (Bool  "("  (Bool (Set (Var "f"))  ($#r1_homothet :::"is_Sc"::: )  (Set (Var "K"))) & (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "b")))  ")" )))  ")" )) "holds"  (Bool (Set (Var "AFP")) "is"   ($#v7_aff_2 :::"Moufangian"::: )  )) ; 
 
theorem :: HOMOTHET:7 (Bool  "for" (Set (Var "AFP")) "being"   ($#l1_analoaf :::"AffinPlane":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "p9")) "," (Set (Var "q9")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFP"))  (Bool  "for" (Set (Var "K")) "," (Set (Var "M")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AFP"))  "st" (Bool (Bool (Set (Var "K"))  ($#r5_aff_1 :::"//"::: )  (Set (Var "M"))) & (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "K"))) & (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  (Set (Var "K"))) & (Bool (Set (Var "p9"))  ($#r2_hidden :::"in"::: )  (Set (Var "K"))) & (Bool (Set (Var "q9"))  ($#r2_hidden :::"in"::: )  (Set (Var "K"))) & (Bool (Set (Var "AFP")) "is"   ($#v7_aff_2 :::"Moufangian"::: )  ) & (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool (Set (Var "q"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p"))) & (Bool (Set (Var "p")) "," (Set (Var "a"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p9")) "," (Set (Var "x"))) & (Bool (Set (Var "p")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p9")) "," (Set (Var "y"))) & (Bool (Set (Var "q")) "," (Set (Var "a"))  ($#r2_analoaf :::"//"::: )  (Set (Var "q9")) "," (Set (Var "x")))) "holds"  (Bool (Set (Var "q")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "q9")) "," (Set (Var "y")))))) ; 
 
theorem :: HOMOTHET:8 (Bool  "for" (Set (Var "AFP")) "being"   ($#l1_analoaf :::"AffinPlane":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFP"))  (Bool  "for" (Set (Var "K")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AFP"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_aff_1 :::"//"::: )  (Set (Var "K"))) & (Bool (Bool  "not" (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "K")))) & (Bool (Set (Var "AFP")) "is"   ($#v7_aff_2 :::"Moufangian"::: )  )) "holds"  (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Permutation":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "AFP"))) "st"  (Bool  "("  (Bool (Set (Var "f"))  ($#r1_homothet :::"is_Sc"::: )  (Set (Var "K"))) & (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "b")))  ")" ))))) ; 
 
theorem :: HOMOTHET:9 (Bool  "for" (Set (Var "AFP")) "being"   ($#l1_analoaf :::"AffinPlane":::) "holds"   (Bool  "("  (Bool (Set (Var "AFP")) "is"   ($#v7_aff_2 :::"Moufangian"::: )  ) "iff" (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFP"))  (Bool  "for" (Set (Var "K")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AFP"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_aff_1 :::"//"::: )  (Set (Var "K"))) & (Bool (Bool  "not" (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "K"))))) "holds"  (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Permutation":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "AFP"))) "st"  (Bool  "("  (Bool (Set (Var "f"))  ($#r1_homothet :::"is_Sc"::: )  (Set (Var "K"))) & (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "b")))  ")" ))))  ")" )) ;