:: TRANSGEO semantic presentation begin definitionlet "A" be ($#m1_hidden :::"set"::: ) ; let "f", "g" be ($#m1_subset_1 :::"Permutation":::) "of" (Set (Const "A")); :: original: :::"*"::: redefine func "g" :::"*"::: "f" -> ($#m1_subset_1 :::"Permutation":::) "of" "A"; end; theorem :: TRANSGEO:1 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "A")) (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "st" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "y"))))))) ; theorem :: TRANSGEO:2 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "y"))) "iff" (Bool (Set (Set "(" (Set (Var "f")) ($#k2_funct_2 :::"""::: ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" )))) ; definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f", "g" be ($#m1_subset_1 :::"Permutation":::) "of" (Set (Const "A")); func "f" :::"\"::: "g" -> ($#m1_subset_1 :::"Permutation":::) "of" "A" equals :: TRANSGEO:def 1 (Set (Set "(" "g" ($#k1_transgeo :::"*"::: ) "f" ")" ) ($#k1_transgeo :::"*"::: ) (Set "(" "g" ($#k2_funct_2 :::"""::: ) ")" )); end; :: deftheorem defines :::"\"::: TRANSGEO:def 1 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "f")) ($#k2_transgeo :::"\"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "g")) ($#k1_transgeo :::"*"::: ) (Set (Var "f")) ")" ) ($#k1_transgeo :::"*"::: ) (Set "(" (Set (Var "g")) ($#k2_funct_2 :::"""::: ) ")" ))))); scheme :: TRANSGEO:sch 1 EXPermutation{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set F1 "(" ")" ) "st" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "y"))) "iff" (Bool P1[(Set (Var "x")) "," (Set (Var "y"))]) ")" ))) provided (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool P1[(Set (Var "x")) "," (Set (Var "y"))]))) and (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool P1[(Set (Var "x")) "," (Set (Var "y"))]))) and (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "x9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool P1[(Set (Var "x")) "," (Set (Var "y"))]) & (Bool P1[(Set (Var "x9")) "," (Set (Var "y"))])) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x9")))) and (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool P1[(Set (Var "x")) "," (Set (Var "y"))]) & (Bool P1[(Set (Var "x")) "," (Set (Var "y9"))])) "holds" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "y9")))) proof end; theorem :: TRANSGEO:3 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k2_funct_2 :::"""::: ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set "(" (Set (Var "f")) ($#k2_funct_2 :::"""::: ) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" )))) ; theorem :: TRANSGEO:4 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "f")) ($#k1_transgeo :::"*"::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "A")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "A")) ")" ) ($#k1_transgeo :::"*"::: ) (Set (Var "f")))))) ; theorem :: TRANSGEO:5 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g")) "," (Set (Var "f")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "A")) "st" (Bool (Bool "(" (Bool (Set (Set (Var "g")) ($#k1_transgeo :::"*"::: ) (Set (Var "f"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "h")) ($#k1_transgeo :::"*"::: ) (Set (Var "f")))) "or" (Bool (Set (Set (Var "f")) ($#k1_transgeo :::"*"::: ) (Set (Var "g"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "f")) ($#k1_transgeo :::"*"::: ) (Set (Var "h")))) ")" )) "holds" (Bool (Set (Var "g")) ($#r2_funct_2 :::"="::: ) (Set (Var "h"))))) ; theorem :: TRANSGEO:6 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_transgeo :::"*"::: ) (Set (Var "g")) ")" ) ($#k2_transgeo :::"\"::: ) (Set (Var "h"))) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k2_transgeo :::"\"::: ) (Set (Var "h")) ")" ) ($#k1_transgeo :::"*"::: ) (Set "(" (Set (Var "g")) ($#k2_transgeo :::"\"::: ) (Set (Var "h")) ")" ))))) ; theorem :: TRANSGEO:7 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k2_funct_2 :::"""::: ) ")" ) ($#k2_transgeo :::"\"::: ) (Set (Var "g"))) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k2_transgeo :::"\"::: ) (Set (Var "g")) ")" ) ($#k2_funct_2 :::"""::: ) )))) ; theorem :: TRANSGEO:8 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "f")) ($#k2_transgeo :::"\"::: ) (Set "(" (Set (Var "g")) ($#k1_transgeo :::"*"::: ) (Set (Var "h")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k2_transgeo :::"\"::: ) (Set (Var "h")) ")" ) ($#k2_transgeo :::"\"::: ) (Set (Var "g")))))) ; theorem :: TRANSGEO:9 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "A")) ")" ) ($#k2_transgeo :::"\"::: ) (Set (Var "f"))) ($#r2_funct_2 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "A")))))) ; theorem :: TRANSGEO:10 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "f")) ($#k2_transgeo :::"\"::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "A")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Var "f"))))) ; theorem :: TRANSGEO:11 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a")))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k2_transgeo :::"\"::: ) (Set (Var "g")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))))))) ; definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Permutation":::) "of" (Set (Const "A")); let "R" be ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "A")) "," (Set (Const "A")) ($#k2_zfmisc_1 :::":]"::: ) ); pred "f" :::"is_FormalIz_of"::: "R" means :: TRANSGEO:def 2 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "A" "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set "(" "f" ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) "," (Set "(" "f" ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R")); end; :: deftheorem defines :::"is_FormalIz_of"::: TRANSGEO:def 2 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "A")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_transgeo :::"is_FormalIz_of"::: ) (Set (Var "R"))) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R")))) ")" )))); theorem :: TRANSGEO:12 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "A")) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "R")) ($#r1_relat_2 :::"is_reflexive_in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "A")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "A"))) ($#r1_transgeo :::"is_FormalIz_of"::: ) (Set (Var "R"))))) ; theorem :: TRANSGEO:13 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "A")) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "R")) ($#r3_relat_2 :::"is_symmetric_in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "A")) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set (Var "f")) ($#r1_transgeo :::"is_FormalIz_of"::: ) (Set (Var "R")))) "holds" (Bool (Set (Set (Var "f")) ($#k2_funct_2 :::"""::: ) ) ($#r1_transgeo :::"is_FormalIz_of"::: ) (Set (Var "R")))))) ; theorem :: TRANSGEO:14 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "A")) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "R")) ($#r8_relat_2 :::"is_transitive_in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "A")) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set (Var "f")) ($#r1_transgeo :::"is_FormalIz_of"::: ) (Set (Var "R"))) & (Bool (Set (Var "g")) ($#r1_transgeo :::"is_FormalIz_of"::: ) (Set (Var "R")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_transgeo :::"*"::: ) (Set (Var "g"))) ($#r1_transgeo :::"is_FormalIz_of"::: ) (Set (Var "R")))))) ; theorem :: TRANSGEO:15 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "A")) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "z")) "," (Set (Var "t")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "z")) "," (Set (Var "t")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) ")" ) & (Bool (Set (Var "f")) ($#r1_transgeo :::"is_FormalIz_of"::: ) (Set (Var "R"))) & (Bool (Set (Var "g")) ($#r1_transgeo :::"is_FormalIz_of"::: ) (Set (Var "R")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_transgeo :::"*"::: ) (Set (Var "g"))) ($#r1_transgeo :::"is_FormalIz_of"::: ) (Set (Var "R")))))) ; definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Permutation":::) "of" (Set (Const "A")); let "R" be ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "A")) "," (Set (Const "A")) ($#k2_zfmisc_1 :::":]"::: ) ); pred "f" :::"is_automorphism_of"::: "R" means :: TRANSGEO:def 3 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "A" "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "z")) "," (Set (Var "t")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R") "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" "f" ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) "," (Set "(" "f" ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set "(" "f" ($#k3_funct_2 :::"."::: ) (Set (Var "z")) ")" ) "," (Set "(" "f" ($#k3_funct_2 :::"."::: ) (Set (Var "t")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R") ")" )); end; :: deftheorem defines :::"is_automorphism_of"::: TRANSGEO:def 3 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "A")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_transgeo :::"is_automorphism_of"::: ) (Set (Var "R"))) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "z")) "," (Set (Var "t")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "z")) ")" ) "," (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "t")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) ")" )) ")" )))); theorem :: TRANSGEO:16 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "A")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "A"))) ($#r2_transgeo :::"is_automorphism_of"::: ) (Set (Var "R"))))) ; theorem :: TRANSGEO:17 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "A")) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r2_transgeo :::"is_automorphism_of"::: ) (Set (Var "R")))) "holds" (Bool (Set (Set (Var "f")) ($#k2_funct_2 :::"""::: ) ) ($#r2_transgeo :::"is_automorphism_of"::: ) (Set (Var "R")))))) ; theorem :: TRANSGEO:18 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "A")) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r2_transgeo :::"is_automorphism_of"::: ) (Set (Var "R"))) & (Bool (Set (Var "g")) ($#r2_transgeo :::"is_automorphism_of"::: ) (Set (Var "R")))) "holds" (Bool (Set (Set (Var "g")) ($#k1_transgeo :::"*"::: ) (Set (Var "f"))) ($#r2_transgeo :::"is_automorphism_of"::: ) (Set (Var "R")))))) ; theorem :: TRANSGEO:19 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "A")) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "R")) ($#r3_relat_2 :::"is_symmetric_in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "A")) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set (Var "R")) ($#r8_relat_2 :::"is_transitive_in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "A")) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set (Var "f")) ($#r1_transgeo :::"is_FormalIz_of"::: ) (Set (Var "R")))) "holds" (Bool (Set (Var "f")) ($#r2_transgeo :::"is_automorphism_of"::: ) (Set (Var "R")))))) ; theorem :: TRANSGEO:20 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "A")) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "z")) "," (Set (Var "t")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "z")) "," (Set (Var "t")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) ")" ) & (Bool (Set (Var "R")) ($#r3_relat_2 :::"is_symmetric_in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "A")) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set (Var "f")) ($#r1_transgeo :::"is_FormalIz_of"::: ) (Set (Var "R")))) "holds" (Bool (Set (Var "f")) ($#r2_transgeo :::"is_automorphism_of"::: ) (Set (Var "R")))))) ; theorem :: TRANSGEO:21 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "A")) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_transgeo :::"is_FormalIz_of"::: ) (Set (Var "R"))) & (Bool (Set (Var "g")) ($#r2_transgeo :::"is_automorphism_of"::: ) (Set (Var "R")))) "holds" (Bool (Set (Set (Var "f")) ($#k2_transgeo :::"\"::: ) (Set (Var "g"))) ($#r1_transgeo :::"is_FormalIz_of"::: ) (Set (Var "R")))))) ; definitionlet "AS" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) ; let "f" be ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "AS"))); pred "f" :::"is_DIL_of"::: "AS" means :: TRANSGEO:def 4 (Bool "f" ($#r1_transgeo :::"is_FormalIz_of"::: ) (Set "the" ($#u1_analoaf :::"CONGR"::: ) "of" "AS")); end; :: deftheorem defines :::"is_DIL_of"::: TRANSGEO:def 4 : (Bool "for" (Set (Var "AS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AS"))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r3_transgeo :::"is_DIL_of"::: ) (Set (Var "AS"))) "iff" (Bool (Set (Var "f")) ($#r1_transgeo :::"is_FormalIz_of"::: ) (Set "the" ($#u1_analoaf :::"CONGR"::: ) "of" (Set (Var "AS")))) ")" ))); theorem :: TRANSGEO:22 (Bool "for" (Set (Var "AS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AS"))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r3_transgeo :::"is_DIL_of"::: ) (Set (Var "AS"))) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "b"))))) ")" ))) ; definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) ; attr "IT" is :::"CongrSpace-like"::: means :: TRANSGEO:def 5 (Bool "(" (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "t")) "," (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "z")) "," (Set (Var "t"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "z")) "," (Set (Var "t"))) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool (Set (Var "x")) "," (Set (Var "x")) ($#r2_analoaf :::"//"::: ) (Set (Var "y")) "," (Set (Var "z"))) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "z")) "," (Set (Var "t")))) "holds" (Bool (Set (Var "z")) "," (Set (Var "t")) ($#r2_analoaf :::"//"::: ) (Set (Var "x")) "," (Set (Var "y"))) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "x")) "," (Set (Var "y"))) ")" ) ")" ); end; :: deftheorem defines :::"CongrSpace-like"::: TRANSGEO:def 5 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_transgeo :::"CongrSpace-like"::: ) ) "iff" (Bool "(" (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "t")) "," (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "z")) "," (Set (Var "t"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "z")) "," (Set (Var "t"))) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Var "x")) "," (Set (Var "x")) ($#r2_analoaf :::"//"::: ) (Set (Var "y")) "," (Set (Var "z"))) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "z")) "," (Set (Var "t")))) "holds" (Bool (Set (Var "z")) "," (Set (Var "t")) ($#r2_analoaf :::"//"::: ) (Set (Var "x")) "," (Set (Var "y"))) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "x")) "," (Set (Var "y"))) ")" ) ")" ) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_analoaf :::"strict"::: ) ($#v1_transgeo :::"CongrSpace-like"::: ) for ($#l1_analoaf :::"AffinStruct"::: ) ; end; definitionmode CongrSpace is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_transgeo :::"CongrSpace-like"::: ) ($#l1_analoaf :::"AffinStruct"::: ) ; end; theorem :: TRANSGEO:23 (Bool "for" (Set (Var "CS")) "being" ($#l1_analoaf :::"CongrSpace":::) "holds" (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "CS")))) ($#r3_transgeo :::"is_DIL_of"::: ) (Set (Var "CS")))) ; theorem :: TRANSGEO:24 (Bool "for" (Set (Var "CS")) "being" ($#l1_analoaf :::"CongrSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "CS"))) "st" (Bool (Bool (Set (Var "f")) ($#r3_transgeo :::"is_DIL_of"::: ) (Set (Var "CS")))) "holds" (Bool (Set (Set (Var "f")) ($#k2_funct_2 :::"""::: ) ) ($#r3_transgeo :::"is_DIL_of"::: ) (Set (Var "CS"))))) ; theorem :: TRANSGEO:25 (Bool "for" (Set (Var "CS")) "being" ($#l1_analoaf :::"CongrSpace":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "CS"))) "st" (Bool (Bool (Set (Var "f")) ($#r3_transgeo :::"is_DIL_of"::: ) (Set (Var "CS"))) & (Bool (Set (Var "g")) ($#r3_transgeo :::"is_DIL_of"::: ) (Set (Var "CS")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_transgeo :::"*"::: ) (Set (Var "g"))) ($#r3_transgeo :::"is_DIL_of"::: ) (Set (Var "CS"))))) ; theorem :: TRANSGEO:26 (Bool "for" (Set (Var "OAS")) "being" ($#l1_analoaf :::"OAffinSpace":::) "holds" (Bool (Set (Var "OAS")) "is" ($#v1_transgeo :::"CongrSpace-like"::: ) )) ; definitionlet "OAS" be ($#l1_analoaf :::"OAffinSpace":::); let "f" be ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "OAS"))); attr "f" is :::"positive_dilatation"::: means :: TRANSGEO:def 6 (Bool "f" ($#r3_transgeo :::"is_DIL_of"::: ) "OAS"); end; :: deftheorem defines :::"positive_dilatation"::: TRANSGEO:def 6 : (Bool "for" (Set (Var "OAS")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "OAS"))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_transgeo :::"positive_dilatation"::: ) ) "iff" (Bool (Set (Var "f")) ($#r3_transgeo :::"is_DIL_of"::: ) (Set (Var "OAS"))) ")" ))); theorem :: TRANSGEO:27 (Bool "for" (Set (Var "OAS")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "OAS"))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_transgeo :::"positive_dilatation"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS")) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "b"))))) ")" ))) ; definitionlet "OAS" be ($#l1_analoaf :::"OAffinSpace":::); let "f" be ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "OAS"))); attr "f" is :::"negative_dilatation"::: means :: TRANSGEO:def 7 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "OAS" "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set "f" ($#k3_funct_2 :::"."::: ) (Set (Var "b"))) "," (Set "f" ($#k3_funct_2 :::"."::: ) (Set (Var "a"))))); end; :: deftheorem defines :::"negative_dilatation"::: TRANSGEO:def 7 : (Bool "for" (Set (Var "OAS")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "OAS"))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v3_transgeo :::"negative_dilatation"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS")) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "b"))) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))))) ")" ))); theorem :: TRANSGEO:28 (Bool "for" (Set (Var "OAS")) "being" ($#l1_analoaf :::"OAffinSpace":::) "holds" (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "OAS")))) "is" ($#v2_transgeo :::"positive_dilatation"::: ) )) ; theorem :: TRANSGEO:29 (Bool "for" (Set (Var "OAS")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "OAS"))) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_transgeo :::"positive_dilatation"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k2_funct_2 :::"""::: ) ) "is" ($#v2_transgeo :::"positive_dilatation"::: ) ))) ; theorem :: TRANSGEO:30 (Bool "for" (Set (Var "OAS")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "OAS"))) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_transgeo :::"positive_dilatation"::: ) ) & (Bool (Set (Var "g")) "is" ($#v2_transgeo :::"positive_dilatation"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k1_transgeo :::"*"::: ) (Set (Var "g"))) "is" ($#v2_transgeo :::"positive_dilatation"::: ) ))) ; theorem :: TRANSGEO:31 (Bool "for" (Set (Var "OAS")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "OAS"))) "holds" (Bool "(" "not" (Bool (Set (Var "f")) "is" ($#v3_transgeo :::"negative_dilatation"::: ) ) "or" "not" (Bool (Set (Var "f")) "is" ($#v2_transgeo :::"positive_dilatation"::: ) ) ")" ))) ; theorem :: TRANSGEO:32 (Bool "for" (Set (Var "OAS")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "OAS"))) "st" (Bool (Bool (Set (Var "f")) "is" ($#v3_transgeo :::"negative_dilatation"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k2_funct_2 :::"""::: ) ) "is" ($#v3_transgeo :::"negative_dilatation"::: ) ))) ; theorem :: TRANSGEO:33 (Bool "for" (Set (Var "OAS")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "OAS"))) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_transgeo :::"positive_dilatation"::: ) ) & (Bool (Set (Var "g")) "is" ($#v3_transgeo :::"negative_dilatation"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_transgeo :::"*"::: ) (Set (Var "g"))) "is" ($#v3_transgeo :::"negative_dilatation"::: ) ) & (Bool (Set (Set (Var "g")) ($#k1_transgeo :::"*"::: ) (Set (Var "f"))) "is" ($#v3_transgeo :::"negative_dilatation"::: ) ) ")" ))) ; definitionlet "OAS" be ($#l1_analoaf :::"OAffinSpace":::); let "f" be ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "OAS"))); attr "f" is :::"dilatation"::: means :: TRANSGEO:def 8 (Bool "f" ($#r1_transgeo :::"is_FormalIz_of"::: ) (Set ($#k1_diraf :::"lambda"::: ) (Set "the" ($#u1_analoaf :::"CONGR"::: ) "of" "OAS"))); end; :: deftheorem defines :::"dilatation"::: TRANSGEO:def 8 : (Bool "for" (Set (Var "OAS")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "OAS"))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v4_transgeo :::"dilatation"::: ) ) "iff" (Bool (Set (Var "f")) ($#r1_transgeo :::"is_FormalIz_of"::: ) (Set ($#k1_diraf :::"lambda"::: ) (Set "the" ($#u1_analoaf :::"CONGR"::: ) "of" (Set (Var "OAS"))))) ")" ))); theorem :: TRANSGEO:34 (Bool "for" (Set (Var "OAS")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "OAS"))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v4_transgeo :::"dilatation"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS")) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_diraf :::"'||'"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "b"))))) ")" ))) ; theorem :: TRANSGEO:35 (Bool "for" (Set (Var "OAS")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "OAS"))) "st" (Bool (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_transgeo :::"positive_dilatation"::: ) ) "or" (Bool (Set (Var "f")) "is" ($#v3_transgeo :::"negative_dilatation"::: ) ) ")" )) "holds" (Bool (Set (Var "f")) "is" ($#v4_transgeo :::"dilatation"::: ) ))) ; theorem :: TRANSGEO:36 (Bool "for" (Set (Var "OAS")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "OAS"))) "st" (Bool (Bool (Set (Var "f")) "is" ($#v4_transgeo :::"dilatation"::: ) )) "holds" (Bool "ex" (Set (Var "f9")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k2_diraf :::"Lambda"::: ) (Set (Var "OAS")) ")" )) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_funct_2 :::"="::: ) (Set (Var "f9"))) & (Bool (Set (Var "f9")) ($#r3_transgeo :::"is_DIL_of"::: ) (Set ($#k2_diraf :::"Lambda"::: ) (Set (Var "OAS")))) ")" )))) ; theorem :: TRANSGEO:37 (Bool "for" (Set (Var "OAS")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k2_diraf :::"Lambda"::: ) (Set (Var "OAS")) ")" )) "st" (Bool (Bool (Set (Var "f")) ($#r3_transgeo :::"is_DIL_of"::: ) (Set ($#k2_diraf :::"Lambda"::: ) (Set (Var "OAS"))))) "holds" (Bool "ex" (Set (Var "f9")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "OAS"))) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_funct_2 :::"="::: ) (Set (Var "f9"))) & (Bool (Set (Var "f9")) "is" ($#v4_transgeo :::"dilatation"::: ) ) ")" )))) ; theorem :: TRANSGEO:38 (Bool "for" (Set (Var "OAS")) "being" ($#l1_analoaf :::"OAffinSpace":::) "holds" (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "OAS")))) "is" ($#v4_transgeo :::"dilatation"::: ) )) ; theorem :: TRANSGEO:39 (Bool "for" (Set (Var "OAS")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "OAS"))) "st" (Bool (Bool (Set (Var "f")) "is" ($#v4_transgeo :::"dilatation"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k2_funct_2 :::"""::: ) ) "is" ($#v4_transgeo :::"dilatation"::: ) ))) ; theorem :: TRANSGEO:40 (Bool "for" (Set (Var "OAS")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "OAS"))) "st" (Bool (Bool (Set (Var "f")) "is" ($#v4_transgeo :::"dilatation"::: ) ) & (Bool (Set (Var "g")) "is" ($#v4_transgeo :::"dilatation"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k1_transgeo :::"*"::: ) (Set (Var "g"))) "is" ($#v4_transgeo :::"dilatation"::: ) ))) ; theorem :: TRANSGEO:41 (Bool "for" (Set (Var "OAS")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "OAS"))) "st" (Bool (Bool (Set (Var "f")) "is" ($#v4_transgeo :::"dilatation"::: ) )) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS")) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_diraf :::"'||'"::: ) (Set (Var "c")) "," (Set (Var "d"))) "iff" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "b"))) ($#r2_diraf :::"'||'"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "c"))) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "d")))) ")" )))) ; theorem :: TRANSGEO:42 (Bool "for" (Set (Var "OAS")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "OAS"))) "st" (Bool (Bool (Set (Var "f")) "is" ($#v4_transgeo :::"dilatation"::: ) )) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS")) "holds" (Bool "(" (Bool ($#r3_diraf :::"LIN"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))) "iff" (Bool ($#r3_diraf :::"LIN"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "b"))) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "c")))) ")" )))) ; theorem :: TRANSGEO:43 (Bool "for" (Set (Var "OAS")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "OAS"))) "st" (Bool (Bool (Set (Var "f")) "is" ($#v4_transgeo :::"dilatation"::: ) ) & (Bool ($#r3_diraf :::"LIN"::: ) (Set (Var "x")) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) "," (Set (Var "y")))) "holds" (Bool ($#r3_diraf :::"LIN"::: ) (Set (Var "x")) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))))))) ; theorem :: TRANSGEO:44 (Bool "for" (Set (Var "OAS")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS")) "holds" (Bool "(" "not" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_diraf :::"'||'"::: ) (Set (Var "c")) "," (Set (Var "d"))) "or" (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_diraf :::"'||'"::: ) (Set (Var "b")) "," (Set (Var "d"))) "or" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS")) "st" (Bool "(" (Bool ($#r3_diraf :::"LIN"::: ) (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "x"))) & (Bool ($#r3_diraf :::"LIN"::: ) (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "x"))) ")" )) ")" ))) ; theorem :: TRANSGEO:45 (Bool "for" (Set (Var "OAS")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "OAS"))) "st" (Bool (Bool (Set (Var "f")) "is" ($#v4_transgeo :::"dilatation"::: ) )) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "f")) ($#r2_funct_2 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "OAS"))))) "or" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS")) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set (Var "x")))) ")" ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS")) "holds" (Bool (Set (Var "x")) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r2_diraf :::"'||'"::: ) (Set (Var "y")) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))))) ")" ))) ; theorem :: TRANSGEO:46 (Bool "for" (Set (Var "OAS")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "OAS"))) "st" (Bool (Bool (Set (Var "f")) "is" ($#v4_transgeo :::"dilatation"::: ) ) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Bool "not" ($#r3_diraf :::"LIN"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x"))))) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))))) ; theorem :: TRANSGEO:47 (Bool "for" (Set (Var "OAS")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "OAS"))) "st" (Bool (Bool (Set (Var "f")) "is" ($#v4_transgeo :::"dilatation"::: ) ) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "f")) ($#r2_funct_2 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "OAS")))))))) ; theorem :: TRANSGEO:48 (Bool "for" (Set (Var "OAS")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "OAS"))) "st" (Bool (Bool (Set (Var "f")) "is" ($#v4_transgeo :::"dilatation"::: ) ) & (Bool (Set (Var "g")) "is" ($#v4_transgeo :::"dilatation"::: ) ) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "a")))) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "b")))) & (Bool (Bool "not" (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) "holds" (Bool (Set (Var "f")) ($#r2_funct_2 :::"="::: ) (Set (Var "g")))))) ; definitionlet "OAS" be ($#l1_analoaf :::"OAffinSpace":::); let "f" be ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "OAS"))); attr "f" is :::"translation"::: means :: TRANSGEO:def 9 (Bool "(" (Bool "f" "is" ($#v4_transgeo :::"dilatation"::: ) ) & (Bool "(" (Bool "f" ($#r2_funct_2 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "OAS"))) "or" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "OAS" "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set "f" ($#k3_funct_2 :::"."::: ) (Set (Var "a"))))) ")" ) ")" ); end; :: deftheorem defines :::"translation"::: TRANSGEO:def 9 : (Bool "for" (Set (Var "OAS")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "OAS"))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_transgeo :::"translation"::: ) ) "iff" (Bool "(" (Bool (Set (Var "f")) "is" ($#v4_transgeo :::"dilatation"::: ) ) & (Bool "(" (Bool (Set (Var "f")) ($#r2_funct_2 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "OAS"))))) "or" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS")) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))))) ")" ) ")" ) ")" ))); theorem :: TRANSGEO:49 (Bool "for" (Set (Var "OAS")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "OAS"))) "st" (Bool (Bool (Set (Var "f")) "is" ($#v4_transgeo :::"dilatation"::: ) )) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_transgeo :::"translation"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS")) "holds" (Bool (Set (Var "x")) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r2_diraf :::"'||'"::: ) (Set (Var "y")) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))))) ")" ))) ; theorem :: TRANSGEO:50 (Bool "for" (Set (Var "OAS")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "OAS"))) "st" (Bool (Bool (Set (Var "f")) "is" ($#v5_transgeo :::"translation"::: ) ) & (Bool (Set (Var "g")) "is" ($#v5_transgeo :::"translation"::: ) ) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "a")))) & (Bool (Bool "not" ($#r3_diraf :::"LIN"::: ) (Set (Var "a")) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) "," (Set (Var "x"))))) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))))))) ; theorem :: TRANSGEO:51 (Bool "for" (Set (Var "OAS")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "OAS"))) "st" (Bool (Bool (Set (Var "f")) "is" ($#v5_transgeo :::"translation"::: ) ) & (Bool (Set (Var "g")) "is" ($#v5_transgeo :::"translation"::: ) ) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))))) "holds" (Bool (Set (Var "f")) ($#r2_funct_2 :::"="::: ) (Set (Var "g")))))) ; theorem :: TRANSGEO:52 (Bool "for" (Set (Var "OAS")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "OAS"))) "st" (Bool (Bool (Set (Var "f")) "is" ($#v5_transgeo :::"translation"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k2_funct_2 :::"""::: ) ) "is" ($#v5_transgeo :::"translation"::: ) ))) ; theorem :: TRANSGEO:53 (Bool "for" (Set (Var "OAS")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "OAS"))) "st" (Bool (Bool (Set (Var "f")) "is" ($#v5_transgeo :::"translation"::: ) ) & (Bool (Set (Var "g")) "is" ($#v5_transgeo :::"translation"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k1_transgeo :::"*"::: ) (Set (Var "g"))) "is" ($#v5_transgeo :::"translation"::: ) ))) ; theorem :: TRANSGEO:54 (Bool "for" (Set (Var "OAS")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "OAS"))) "st" (Bool (Bool (Set (Var "f")) "is" ($#v5_transgeo :::"translation"::: ) )) "holds" (Bool (Set (Var "f")) "is" ($#v2_transgeo :::"positive_dilatation"::: ) ))) ; theorem :: TRANSGEO:55 (Bool "for" (Set (Var "OAS")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "OAS"))) "st" (Bool (Bool (Set (Var "f")) "is" ($#v4_transgeo :::"dilatation"::: ) ) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool ($#r1_diraf :::"Mid"::: ) (Set (Var "q")) "," (Set (Var "p")) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "q")))) & (Bool (Bool "not" ($#r3_diraf :::"LIN"::: ) (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "x"))))) "holds" (Bool ($#r1_diraf :::"Mid"::: ) (Set (Var "x")) "," (Set (Var "p")) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))))))) ; theorem :: TRANSGEO:56 (Bool "for" (Set (Var "OAS")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "OAS"))) "st" (Bool (Bool (Set (Var "f")) "is" ($#v4_transgeo :::"dilatation"::: ) ) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool ($#r1_diraf :::"Mid"::: ) (Set (Var "q")) "," (Set (Var "p")) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "q")))) & (Bool (Set (Var "q")) ($#r1_hidden :::"<>"::: ) (Set (Var "p")))) "holds" (Bool ($#r1_diraf :::"Mid"::: ) (Set (Var "x")) "," (Set (Var "p")) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))))))) ; theorem :: TRANSGEO:57 (Bool "for" (Set (Var "OAS")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "OAS"))) "st" (Bool (Bool (Set (Var "f")) "is" ($#v4_transgeo :::"dilatation"::: ) ) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"<>"::: ) (Set (Var "p"))) & (Bool ($#r1_diraf :::"Mid"::: ) (Set (Var "q")) "," (Set (Var "p")) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "q")))) & (Bool (Bool "not" ($#r3_diraf :::"LIN"::: ) (Set (Var "p")) "," (Set (Var "x")) "," (Set (Var "y"))))) "holds" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))))))) ; theorem :: TRANSGEO:58 (Bool "for" (Set (Var "OAS")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "OAS"))) "st" (Bool (Bool (Set (Var "f")) "is" ($#v4_transgeo :::"dilatation"::: ) ) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"<>"::: ) (Set (Var "p"))) & (Bool ($#r1_diraf :::"Mid"::: ) (Set (Var "q")) "," (Set (Var "p")) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "q")))) & (Bool ($#r3_diraf :::"LIN"::: ) (Set (Var "p")) "," (Set (Var "x")) "," (Set (Var "y")))) "holds" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))))))) ; theorem :: TRANSGEO:59 (Bool "for" (Set (Var "OAS")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "OAS"))) "st" (Bool (Bool (Set (Var "f")) "is" ($#v4_transgeo :::"dilatation"::: ) ) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"<>"::: ) (Set (Var "p"))) & (Bool ($#r1_diraf :::"Mid"::: ) (Set (Var "q")) "," (Set (Var "p")) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "q"))))) "holds" (Bool (Set (Var "f")) "is" ($#v3_transgeo :::"negative_dilatation"::: ) )))) ; theorem :: TRANSGEO:60 (Bool "for" (Set (Var "OAS")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "OAS"))) "st" (Bool (Bool (Set (Var "f")) "is" ($#v4_transgeo :::"dilatation"::: ) ) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS")) "holds" (Bool (Set (Var "p")) "," (Set (Var "x")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")))) ")" )) "holds" (Bool "for" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS")) "holds" (Bool (Set (Var "y")) "," (Set (Var "z")) ($#r2_analoaf :::"//"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "z")))))))) ; theorem :: TRANSGEO:61 (Bool "for" (Set (Var "OAS")) "being" ($#l1_analoaf :::"OAffinSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "OAS"))) "holds" (Bool "(" "not" (Bool (Set (Var "f")) "is" ($#v4_transgeo :::"dilatation"::: ) ) "or" (Bool (Set (Var "f")) "is" ($#v2_transgeo :::"positive_dilatation"::: ) ) "or" (Bool (Set (Var "f")) "is" ($#v3_transgeo :::"negative_dilatation"::: ) ) ")" ))) ; theorem :: TRANSGEO:62 (Bool "for" (Set (Var "AFS")) "being" ($#l1_analoaf :::"AffinSpace":::) "holds" (Bool (Set (Var "AFS")) "is" ($#v1_transgeo :::"CongrSpace-like"::: ) )) ; theorem :: TRANSGEO:63 (Bool "for" (Set (Var "OAS")) "being" ($#l1_analoaf :::"OAffinSpace":::) "holds" (Bool (Set ($#k2_diraf :::"Lambda"::: ) (Set (Var "OAS"))) "is" ($#l1_analoaf :::"CongrSpace":::))) ; definitionlet "AFS" be ($#l1_analoaf :::"AffinSpace":::); let "f" be ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "AFS"))); attr "f" is :::"dilatation"::: means :: TRANSGEO:def 10 (Bool "f" ($#r3_transgeo :::"is_DIL_of"::: ) "AFS"); end; :: deftheorem defines :::"dilatation"::: TRANSGEO:def 10 : (Bool "for" (Set (Var "AFS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AFS"))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v6_transgeo :::"dilatation"::: ) ) "iff" (Bool (Set (Var "f")) ($#r3_transgeo :::"is_DIL_of"::: ) (Set (Var "AFS"))) ")" ))); theorem :: TRANSGEO:64 (Bool "for" (Set (Var "AFS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AFS"))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v6_transgeo :::"dilatation"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFS")) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "b"))))) ")" ))) ; theorem :: TRANSGEO:65 (Bool "for" (Set (Var "AFS")) "being" ($#l1_analoaf :::"AffinSpace":::) "holds" (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AFS")))) "is" ($#v6_transgeo :::"dilatation"::: ) )) ; theorem :: TRANSGEO:66 (Bool "for" (Set (Var "AFS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AFS"))) "st" (Bool (Bool (Set (Var "f")) "is" ($#v6_transgeo :::"dilatation"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k2_funct_2 :::"""::: ) ) "is" ($#v6_transgeo :::"dilatation"::: ) ))) ; theorem :: TRANSGEO:67 (Bool "for" (Set (Var "AFS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AFS"))) "st" (Bool (Bool (Set (Var "f")) "is" ($#v6_transgeo :::"dilatation"::: ) ) & (Bool (Set (Var "g")) "is" ($#v6_transgeo :::"dilatation"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k1_transgeo :::"*"::: ) (Set (Var "g"))) "is" ($#v6_transgeo :::"dilatation"::: ) ))) ; theorem :: TRANSGEO:68 (Bool "for" (Set (Var "AFS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AFS"))) "st" (Bool (Bool (Set (Var "f")) "is" ($#v6_transgeo :::"dilatation"::: ) )) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFS")) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) "iff" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "b"))) ($#r2_analoaf :::"//"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "c"))) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "d")))) ")" )))) ; theorem :: TRANSGEO:69 (Bool "for" (Set (Var "AFS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AFS"))) "st" (Bool (Bool (Set (Var "f")) "is" ($#v6_transgeo :::"dilatation"::: ) )) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFS")) "holds" (Bool "(" (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))) "iff" (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "b"))) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "c")))) ")" )))) ; theorem :: TRANSGEO:70 (Bool "for" (Set (Var "AFS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFS")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AFS"))) "st" (Bool (Bool (Set (Var "f")) "is" ($#v6_transgeo :::"dilatation"::: ) ) & (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "x")) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) "," (Set (Var "y")))) "holds" (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "x")) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))))))) ; theorem :: TRANSGEO:71 (Bool "for" (Set (Var "AFS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFS")) "holds" (Bool "(" "not" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) "or" (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "d"))) "or" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFS")) "st" (Bool "(" (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "x"))) & (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "x"))) ")" )) ")" ))) ; theorem :: TRANSGEO:72 (Bool "for" (Set (Var "AFS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AFS"))) "st" (Bool (Bool (Set (Var "f")) "is" ($#v6_transgeo :::"dilatation"::: ) )) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "f")) ($#r2_funct_2 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AFS"))))) "or" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFS")) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set (Var "x")))) ")" ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFS")) "holds" (Bool (Set (Var "x")) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r2_analoaf :::"//"::: ) (Set (Var "y")) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))))) ")" ))) ; theorem :: TRANSGEO:73 (Bool "for" (Set (Var "AFS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFS")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AFS"))) "st" (Bool (Bool (Set (Var "f")) "is" ($#v6_transgeo :::"dilatation"::: ) ) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Bool "not" ($#r1_aff_1 :::"LIN"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x"))))) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))))) ; theorem :: TRANSGEO:74 (Bool "for" (Set (Var "AFS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFS")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AFS"))) "st" (Bool (Bool (Set (Var "f")) "is" ($#v6_transgeo :::"dilatation"::: ) ) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "f")) ($#r2_funct_2 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AFS")))))))) ; theorem :: TRANSGEO:75 (Bool "for" (Set (Var "AFS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFS")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AFS"))) "st" (Bool (Bool (Set (Var "f")) "is" ($#v6_transgeo :::"dilatation"::: ) ) & (Bool (Set (Var "g")) "is" ($#v6_transgeo :::"dilatation"::: ) ) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "a")))) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "b")))) & (Bool (Bool "not" (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) "holds" (Bool (Set (Var "f")) ($#r2_funct_2 :::"="::: ) (Set (Var "g")))))) ; theorem :: TRANSGEO:76 (Bool "for" (Set (Var "AFS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFS")) "st" (Bool (Bool (Bool "not" ($#r1_aff_1 :::"LIN"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d1"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d2"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "d1"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "d2")))) "holds" (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Var "d2"))))) ; definitionlet "AFS" be ($#l1_analoaf :::"AffinSpace":::); let "f" be ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "AFS"))); attr "f" is :::"translation"::: means :: TRANSGEO:def 11 (Bool "(" (Bool "f" "is" ($#v6_transgeo :::"dilatation"::: ) ) & (Bool "(" (Bool "f" ($#r2_funct_2 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "AFS"))) "or" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "AFS" "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set "f" ($#k3_funct_2 :::"."::: ) (Set (Var "a"))))) ")" ) ")" ); end; :: deftheorem defines :::"translation"::: TRANSGEO:def 11 : (Bool "for" (Set (Var "AFS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AFS"))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v7_transgeo :::"translation"::: ) ) "iff" (Bool "(" (Bool (Set (Var "f")) "is" ($#v6_transgeo :::"dilatation"::: ) ) & (Bool "(" (Bool (Set (Var "f")) ($#r2_funct_2 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AFS"))))) "or" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFS")) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))))) ")" ) ")" ) ")" ))); theorem :: TRANSGEO:77 (Bool "for" (Set (Var "AFS")) "being" ($#l1_analoaf :::"AffinSpace":::) "holds" (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AFS")))) "is" ($#v7_transgeo :::"translation"::: ) )) ; theorem :: TRANSGEO:78 (Bool "for" (Set (Var "AFS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AFS"))) "st" (Bool (Bool (Set (Var "f")) "is" ($#v6_transgeo :::"dilatation"::: ) )) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v7_transgeo :::"translation"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFS")) "holds" (Bool (Set (Var "x")) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r2_analoaf :::"//"::: ) (Set (Var "y")) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))))) ")" ))) ; theorem :: TRANSGEO:79 (Bool "for" (Set (Var "AFS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFS")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AFS"))) "st" (Bool (Bool (Set (Var "f")) "is" ($#v7_transgeo :::"translation"::: ) ) & (Bool (Set (Var "g")) "is" ($#v7_transgeo :::"translation"::: ) ) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "a")))) & (Bool (Bool "not" ($#r1_aff_1 :::"LIN"::: ) (Set (Var "a")) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) "," (Set (Var "x"))))) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))))))) ; theorem :: TRANSGEO:80 (Bool "for" (Set (Var "AFS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFS")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AFS"))) "st" (Bool (Bool (Set (Var "f")) "is" ($#v7_transgeo :::"translation"::: ) ) & (Bool (Set (Var "g")) "is" ($#v7_transgeo :::"translation"::: ) ) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))))) "holds" (Bool (Set (Var "f")) ($#r2_funct_2 :::"="::: ) (Set (Var "g")))))) ; theorem :: TRANSGEO:81 (Bool "for" (Set (Var "AFS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AFS"))) "st" (Bool (Bool (Set (Var "f")) "is" ($#v7_transgeo :::"translation"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k2_funct_2 :::"""::: ) ) "is" ($#v7_transgeo :::"translation"::: ) ))) ; theorem :: TRANSGEO:82 (Bool "for" (Set (Var "AFS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AFS"))) "st" (Bool (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"))) "is" ($#v7_transgeo :::"translation"::: ) ))) ; definitionlet "AFS" be ($#l1_analoaf :::"AffinSpace":::); let "f" be ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "AFS"))); attr "f" is :::"collineation"::: means :: TRANSGEO:def 12 (Bool "f" ($#r2_transgeo :::"is_automorphism_of"::: ) (Set "the" ($#u1_analoaf :::"CONGR"::: ) "of" "AFS")); end; :: deftheorem defines :::"collineation"::: TRANSGEO:def 12 : (Bool "for" (Set (Var "AFS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AFS"))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v8_transgeo :::"collineation"::: ) ) "iff" (Bool (Set (Var "f")) ($#r2_transgeo :::"is_automorphism_of"::: ) (Set "the" ($#u1_analoaf :::"CONGR"::: ) "of" (Set (Var "AFS")))) ")" ))); theorem :: TRANSGEO:83 (Bool "for" (Set (Var "AFS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AFS"))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v8_transgeo :::"collineation"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFS")) "holds" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "z")) "," (Set (Var "t"))) "iff" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) ($#r2_analoaf :::"//"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "z"))) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "t")))) ")" )) ")" ))) ; theorem :: TRANSGEO:84 (Bool "for" (Set (Var "AFS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFS")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AFS"))) "st" (Bool (Bool (Set (Var "f")) "is" ($#v8_transgeo :::"collineation"::: ) )) "holds" (Bool "(" (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z"))) "iff" (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "z")))) ")" )))) ; theorem :: TRANSGEO:85 (Bool "for" (Set (Var "AFS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AFS"))) "st" (Bool (Bool (Set (Var "f")) "is" ($#v8_transgeo :::"collineation"::: ) ) & (Bool (Set (Var "g")) "is" ($#v8_transgeo :::"collineation"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k2_funct_2 :::"""::: ) ) "is" ($#v8_transgeo :::"collineation"::: ) ) & (Bool (Set (Set (Var "f")) ($#k1_transgeo :::"*"::: ) (Set (Var "g"))) "is" ($#v8_transgeo :::"collineation"::: ) ) & (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AFS")))) "is" ($#v8_transgeo :::"collineation"::: ) ) ")" ))) ; theorem :: TRANSGEO:86 (Bool "for" (Set (Var "AFS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFS")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AFS"))) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AFS")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "A")))))))) ; theorem :: TRANSGEO:87 (Bool "for" (Set (Var "AFS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFS")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AFS"))) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AFS")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "A")))) "iff" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFS")) "st" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" )) ")" ))))) ; theorem :: TRANSGEO:88 (Bool "for" (Set (Var "AFS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AFS"))) (Bool "for" (Set (Var "A")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AFS")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "C"))))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "C")))))) ; theorem :: TRANSGEO:89 (Bool "for" (Set (Var "AFS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFS")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AFS"))) "st" (Bool (Bool (Set (Var "f")) "is" ($#v8_transgeo :::"collineation"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k2_aff_1 :::"Line"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_aff_1 :::"Line"::: ) "(" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a")) ")" ) "," (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "b")) ")" ) ")" ))))) ; theorem :: TRANSGEO:90 (Bool "for" (Set (Var "AFS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AFS"))) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AFS")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v8_transgeo :::"collineation"::: ) ) & (Bool (Set (Var "K")) "is" ($#v1_aff_1 :::"being_line"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "K"))) "is" ($#v1_aff_1 :::"being_line"::: ) )))) ; theorem :: TRANSGEO:91 (Bool "for" (Set (Var "AFS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AFS"))) (Bool "for" (Set (Var "A")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AFS")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v8_transgeo :::"collineation"::: ) ) & (Bool (Set (Var "A")) ($#r5_aff_1 :::"//"::: ) (Set (Var "C")))) "holds" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "A"))) ($#r5_aff_1 :::"//"::: ) (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "C"))))))) ; theorem :: TRANSGEO:92 (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 "(" "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AFP")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_aff_1 :::"being_line"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "A"))) "is" ($#v1_aff_1 :::"being_line"::: ) ) ")" )) "holds" (Bool (Set (Var "f")) "is" ($#v8_transgeo :::"collineation"::: ) ))) ; theorem :: TRANSGEO:93 (Bool "for" (Set (Var "AFP")) "being" ($#l1_analoaf :::"AffinPlane":::) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AFP")) (Bool "for" (Set (Var "p")) "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" ($#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 (Bool "not" (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "K")))) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "p")))) "holds" (Bool (Set (Var "f")) ($#r2_funct_2 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AFP"))))))))) ;