:: TRANSLAC  semantic presentation begin  













definitionlet "AS" be   ($#l1_analoaf :::"AffinSpace":::); attr "AS" is  :::"Fanoian":::  means :: TRANSLAC:def 1 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" "AS"  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "d"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "c")))) "holds"  (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")))); end; 




:: deftheorem    defines :::"Fanoian"::: TRANSLAC:def 1 :  (Bool  "for" (Set (Var "AS")) "being"   ($#l1_analoaf :::"AffinSpace":::) "holds"   (Bool  "("  (Bool (Set (Var "AS")) "is"   ($#v1_translac :::"Fanoian"::: )  ) "iff" (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "d"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "c")))) "holds"  (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))))  ")" )); 
 
theorem :: TRANSLAC:1 (Bool  "for" (Set (Var "AS")) "being"   ($#l1_analoaf :::"AffinSpace":::)  "st" (Bool (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st"  (Bool  "("  (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c"))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c")))  ")" ))) "holds"  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool  "ex" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st"  (Bool  "("  (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r"))) & (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "r"))) & (Bool (Set (Var "q"))  ($#r1_hidden :::"<>"::: )  (Set (Var "r")))  ")" )))) ; 
 


































theorem :: TRANSLAC:2 (Bool  "for" (Set (Var "AFP")) "being"   ($#l1_analoaf :::"AffinPlane":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFP"))  "st" (Bool (Bool (Set (Var "AFP")) "is"   ($#v1_translac :::"Fanoian"::: )  ) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "d"))) & (Bool (Bool  "not"   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))))) "holds"  (Bool  "ex" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFP")) "st"  (Bool  "("  (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "p"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "a")) "," (Set (Var "d")) "," (Set (Var "p")))  ")" )))) ; 
 
theorem :: TRANSLAC:3 (Bool  "for" (Set (Var "AFP")) "being"   ($#l1_analoaf :::"AffinPlane":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "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")) "is"   ($#v7_transgeo :::"translation"::: )  ) & (Bool (Bool  "not"   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "a")) "," (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a"))) "," (Set (Var "x")))) & (Bool (Set (Var "a")) "," (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a")))  ($#r2_analoaf :::"//"::: )  (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "a")) "," (Set (Var "x"))  ($#r2_analoaf :::"//"::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a"))) "," (Set (Var "y")))) "holds"  (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x"))))))) ; 
 
theorem :: TRANSLAC:4 (Bool  "for" (Set (Var "AFP")) "being"   ($#l1_analoaf :::"AffinPlane":::) "holds"   (Bool  "("  (Bool (Set (Var "AFP")) "is"   ($#v11_aff_2 :::"translational"::: )  ) "iff" (Bool  "for" (Set (Var "a")) "," (Set (Var "a9")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "b9")) "," (Set (Var "c9")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFP"))  "st" (Bool (Bool (Bool  "not"   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "a")) "," (Set (Var "a9")) "," (Set (Var "b")))) & (Bool (Bool  "not"   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "a")) "," (Set (Var "a9")) "," (Set (Var "c")))) & (Bool (Set (Var "a")) "," (Set (Var "a9"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "b9"))) & (Bool (Set (Var "a")) "," (Set (Var "a9"))  ($#r2_analoaf :::"//"::: )  (Set (Var "c")) "," (Set (Var "c9"))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a9")) "," (Set (Var "b9"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a9")) "," (Set (Var "c9")))) "holds"  (Bool (Set (Var "b")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b9")) "," (Set (Var "c9"))))  ")" )) ; 
 
theorem :: TRANSLAC:5 (Bool  "for" (Set (Var "AFP")) "being"   ($#l1_analoaf :::"AffinPlane":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFP")) (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"   ($#v7_transgeo :::"translation"::: )  ) & (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")" )))) ; 
 
theorem :: TRANSLAC:6 (Bool  "for" (Set (Var "AFP")) "being"   ($#l1_analoaf :::"AffinPlane":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFP"))  "st" (Bool (Bool  "("   "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFP"))  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r"))) & (Bool (Bool  "not" (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Var "p"))))) "holds"  (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Var "q")))  ")" ) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "p"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "q"))) & (Bool (Bool  "not"   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p"))))) "holds"  (Bool (Set (Var "a")) "," (Set (Var "q"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "p"))))) ; 
 
theorem :: TRANSLAC:7 (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"))  "st" (Bool (Bool (Set (Var "AFP")) "is"   ($#v11_aff_2 :::"translational"::: )  )) "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"   ($#v7_transgeo :::"translation"::: )  ) & (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "b")))  ")" )))) ; 
 
theorem :: TRANSLAC:8 (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  "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"   ($#v7_transgeo :::"translation"::: )  ) & (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "b")))  ")" ))  ")" )) "holds"  (Bool (Set (Var "AFP")) "is"   ($#v11_aff_2 :::"translational"::: )  )) ; 
 
theorem :: TRANSLAC:9 (Bool  "for" (Set (Var "AFP")) "being"   ($#l1_analoaf :::"AffinPlane":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFP"))  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Permutation":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "AFP")))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v7_transgeo :::"translation"::: )  ) & (Bool (Set (Var "g")) "is"   ($#v7_transgeo :::"translation"::: )  ) & (Bool (Bool  "not"   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "a")) "," (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a"))) "," (Set (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a")))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_transgeo :::"*"::: )  (Set (Var "g")))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "g"))  ($#k1_transgeo :::"*"::: )  (Set (Var "f"))))))) ; 
 
theorem :: TRANSLAC:10 (Bool  "for" (Set (Var "AFP")) "being"   ($#l1_analoaf :::"AffinPlane":::)  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Permutation":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "AFP")))  "st" (Bool (Bool (Set (Var "AFP")) "is"   ($#v11_aff_2 :::"translational"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v7_transgeo :::"translation"::: )  ) & (Bool (Set (Var "g")) "is"   ($#v7_transgeo :::"translation"::: )  )) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_transgeo :::"*"::: )  (Set (Var "g")))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "g"))  ($#k1_transgeo :::"*"::: )  (Set (Var "f")))))) ; 
 
theorem :: TRANSLAC:11 (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 "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Permutation":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "AFP")))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v7_transgeo :::"translation"::: )  ) & (Bool (Set (Var "g")) "is"   ($#v7_transgeo :::"translation"::: )  ) & (Bool (Set (Var "p")) "," (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p"))))) "holds"  (Bool (Set (Var "p")) "," (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Set  "(" (Set (Var "f"))  ($#k1_transgeo :::"*"::: )  (Set (Var "g")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "p"))))))) ; 
 
theorem :: TRANSLAC:12 (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")))  "st" (Bool (Bool (Set (Var "AFP")) "is"   ($#v1_translac :::"Fanoian"::: )  ) & (Bool (Set (Var "AFP")) "is"   ($#v11_aff_2 :::"translational"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v7_transgeo :::"translation"::: )  )) "holds"  (Bool  "ex" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Permutation":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "AFP"))) "st"  (Bool  "("  (Bool (Set (Var "g")) "is"   ($#v7_transgeo :::"translation"::: )  ) & (Bool (Set (Set (Var "g"))  ($#k1_transgeo :::"*"::: )  (Set (Var "g")))  ($#r2_funct_2 :::"="::: )  (Set (Var "f")))  ")" )))) ; 
 
theorem :: TRANSLAC:13 (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")))  "st" (Bool (Bool (Set (Var "AFP")) "is"   ($#v1_translac :::"Fanoian"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v7_transgeo :::"translation"::: )  ) & (Bool (Set (Set (Var "f"))  ($#k1_transgeo :::"*"::: )  (Set (Var "f")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k6_partfun1 :::"id"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "AFP")))))) "holds"  (Bool (Set (Var "f"))  ($#r2_funct_2 :::"="::: )  (Set   ($#k6_partfun1 :::"id"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "AFP"))))))) ; 
 
theorem :: TRANSLAC:14 (Bool  "for" (Set (Var "AFP")) "being"   ($#l1_analoaf :::"AffinPlane":::)  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Permutation":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "AFP")))  "st" (Bool (Bool (Set (Var "AFP")) "is"   ($#v11_aff_2 :::"translational"::: )  ) & (Bool (Set (Var "AFP")) "is"   ($#v1_translac :::"Fanoian"::: )  ) & (Bool (Set (Var "f1")) "is"   ($#v7_transgeo :::"translation"::: )  ) & (Bool (Set (Var "f2")) "is"   ($#v7_transgeo :::"translation"::: )  ) & (Bool (Set (Var "g"))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "f1"))  ($#k1_transgeo :::"*"::: )  (Set (Var "f1")))) & (Bool (Set (Var "g"))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "f2"))  ($#k1_transgeo :::"*"::: )  (Set (Var "f2"))))) "holds"  (Bool (Set (Var "f1"))  ($#r2_funct_2 :::"="::: )  (Set (Var "f2"))))) ;