:: GEOMTRAP semantic presentation begin definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "u", "v", "u1", "v1" be ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Const "V")); pred "u" "," "v" :::"'||'"::: "u1" "," "v1" means :: GEOMTRAP:def 1 (Bool "(" (Bool "u" "," "v" ($#r1_analoaf :::"//"::: ) "u1" "," "v1") "or" (Bool "u" "," "v" ($#r1_analoaf :::"//"::: ) "v1" "," "u1") ")" ); end; :: deftheorem defines :::"'||'"::: GEOMTRAP:def 1 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "v1")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r1_geomtrap :::"'||'"::: ) (Set (Var "u1")) "," (Set (Var "v1"))) "iff" (Bool "(" (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r1_analoaf :::"//"::: ) (Set (Var "u1")) "," (Set (Var "v1"))) "or" (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r1_analoaf :::"//"::: ) (Set (Var "v1")) "," (Set (Var "u1"))) ")" ) ")" ))); theorem :: GEOMTRAP:1 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "w")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "w")) "," (Set (Var "y")))) "holds" (Bool (Set ($#k2_analoaf :::"OASpace"::: ) (Set (Var "V"))) "is" ($#l1_analoaf :::"OAffinSpace":::)))) ; theorem :: GEOMTRAP:2 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "v1")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "p1")) "," (Set (Var "q1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_analoaf :::"OASpace"::: ) (Set (Var "V")) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "u"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "v"))) & (Bool (Set (Var "p1")) ($#r1_hidden :::"="::: ) (Set (Var "u1"))) & (Bool (Set (Var "q1")) ($#r1_hidden :::"="::: ) (Set (Var "v1")))) "holds" (Bool "(" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "p1")) "," (Set (Var "q1"))) "iff" (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r1_analoaf :::"//"::: ) (Set (Var "u1")) "," (Set (Var "v1"))) ")" )))) ; theorem :: GEOMTRAP:3 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "v1")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "w")) "," (Set (Var "y")))) "holds" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "p1")) "," (Set (Var "q1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k2_diraf :::"Lambda"::: ) (Set "(" ($#k2_analoaf :::"OASpace"::: ) (Set (Var "V")) ")" ) ")" )) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "u"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "v"))) & (Bool (Set (Var "p1")) ($#r1_hidden :::"="::: ) (Set (Var "u1"))) & (Bool (Set (Var "q1")) ($#r1_hidden :::"="::: ) (Set (Var "v1")))) "holds" (Bool "(" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "p1")) "," (Set (Var "q1"))) "iff" (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r1_geomtrap :::"'||'"::: ) (Set (Var "u1")) "," (Set (Var "v1"))) ")" )))) ; theorem :: GEOMTRAP:4 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "v1")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "p1")) "," (Set (Var "q1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k2_analmetr :::"AMSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "w")) "," (Set (Var "y")) ")" ")" )) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "u"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "v"))) & (Bool (Set (Var "p1")) ($#r1_hidden :::"="::: ) (Set (Var "u1"))) & (Bool (Set (Var "q1")) ($#r1_hidden :::"="::: ) (Set (Var "v1")))) "holds" (Bool "(" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "p1")) "," (Set (Var "q1"))) "iff" (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r1_geomtrap :::"'||'"::: ) (Set (Var "u1")) "," (Set (Var "v1"))) ")" )))) ; definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "u", "v" be ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Const "V")); func "u" :::"#"::: "v" -> ($#m1_subset_1 :::"VECTOR":::) "of" "V" means :: GEOMTRAP:def 2 (Bool (Set it ($#k3_rlvect_1 :::"+"::: ) it) ($#r1_hidden :::"="::: ) (Set "u" ($#k3_rlvect_1 :::"+"::: ) "v")); commutativity (Bool "for" (Set (Var "b1")) "," (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Const "V")) "st" (Bool (Bool (Set (Set (Var "b1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "v"))))) "holds" (Bool (Set (Set (Var "b1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "u"))))) ; idempotence (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Const "V")) "holds" (Bool (Set (Set (Var "u")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "u"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "u"))))) ; end; :: deftheorem defines :::"#"::: GEOMTRAP:def 2 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "b4")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k1_geomtrap :::"#"::: ) (Set (Var "v")))) "iff" (Bool (Set (Set (Var "b4")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "v")))) ")" ))); theorem :: GEOMTRAP:5 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Set (Set (Var "u")) ($#k1_geomtrap :::"#"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "w")))))) ; theorem :: GEOMTRAP:6 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "v")) "," (Set (Var "v1")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" (Set (Var "u")) ($#k1_geomtrap :::"#"::: ) (Set (Var "u1")) ")" ) ($#k1_geomtrap :::"#"::: ) (Set "(" (Set (Var "v")) ($#k1_geomtrap :::"#"::: ) (Set (Var "v1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "u")) ($#k1_geomtrap :::"#"::: ) (Set (Var "v")) ")" ) ($#k1_geomtrap :::"#"::: ) (Set "(" (Set (Var "u1")) ($#k1_geomtrap :::"#"::: ) (Set (Var "v1")) ")" ))))) ; theorem :: GEOMTRAP:7 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "y")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Set (Var "u")) ($#k1_geomtrap :::"#"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k1_geomtrap :::"#"::: ) (Set (Var "w"))))) "holds" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "w"))))) ; theorem :: GEOMTRAP:8 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r1_analoaf :::"//"::: ) (Set (Set (Var "y")) ($#k1_geomtrap :::"#"::: ) (Set (Var "u"))) "," (Set (Set (Var "y")) ($#k1_geomtrap :::"#"::: ) (Set (Var "v")))))) ; theorem :: GEOMTRAP:9 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r1_geomtrap :::"'||'"::: ) (Set (Set (Var "w")) ($#k1_geomtrap :::"#"::: ) (Set (Var "u"))) "," (Set (Set (Var "w")) ($#k1_geomtrap :::"#"::: ) (Set (Var "v")))))) ; theorem :: GEOMTRAP:10 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Num 2) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "u")) ($#k1_geomtrap :::"#"::: ) (Set (Var "v")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "u")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "u")))) & (Bool (Set (Num 2) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "u")) ($#k1_geomtrap :::"#"::: ) (Set (Var "v")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "u")))) ")" ))) ; theorem :: GEOMTRAP:11 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Var "u")) "," (Set (Set (Var "u")) ($#k1_geomtrap :::"#"::: ) (Set (Var "v"))) ($#r1_analoaf :::"//"::: ) (Set (Set (Var "u")) ($#k1_geomtrap :::"#"::: ) (Set (Var "v"))) "," (Set (Var "v"))))) ; theorem :: GEOMTRAP:12 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r1_analoaf :::"//"::: ) (Set (Var "u")) "," (Set (Set (Var "u")) ($#k1_geomtrap :::"#"::: ) (Set (Var "v")))) & (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r1_analoaf :::"//"::: ) (Set (Set (Var "u")) ($#k1_geomtrap :::"#"::: ) (Set (Var "v"))) "," (Set (Var "v"))) ")" ))) ; theorem :: GEOMTRAP:13 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "y")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "u")) "," (Set (Var "y")) ($#r1_analoaf :::"//"::: ) (Set (Var "y")) "," (Set (Var "v")))) "holds" (Bool (Set (Set (Var "u")) ($#k1_geomtrap :::"#"::: ) (Set (Var "y"))) "," (Set (Var "y")) ($#r1_analoaf :::"//"::: ) (Set (Var "y")) "," (Set (Set (Var "y")) ($#k1_geomtrap :::"#"::: ) (Set (Var "v")))))) ; theorem :: GEOMTRAP:14 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "v1")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r1_analoaf :::"//"::: ) (Set (Var "u1")) "," (Set (Var "v1")))) "holds" (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r1_analoaf :::"//"::: ) (Set (Set (Var "u")) ($#k1_geomtrap :::"#"::: ) (Set (Var "u1"))) "," (Set (Set (Var "v")) ($#k1_geomtrap :::"#"::: ) (Set (Var "v1")))))) ; definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "w", "y", "u", "u1", "v", "v1" be ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Const "V")); pred "u" "," "u1" "," "v" "," "v1" :::"are_DTr_wrt"::: "w" "," "y" means :: GEOMTRAP:def 3 (Bool "(" (Bool "u" "," "u1" ($#r1_analoaf :::"//"::: ) "v" "," "v1") & (Bool "u" "," "u1" "," (Set "u" ($#k1_geomtrap :::"#"::: ) "u1") "," (Set "v" ($#k1_geomtrap :::"#"::: ) "v1") ($#r3_analmetr :::"are_Ort_wrt"::: ) "w" "," "y") & (Bool "v" "," "v1" "," (Set "u" ($#k1_geomtrap :::"#"::: ) "u1") "," (Set "v" ($#k1_geomtrap :::"#"::: ) "v1") ($#r3_analmetr :::"are_Ort_wrt"::: ) "w" "," "y") ")" ); end; :: deftheorem defines :::"are_DTr_wrt"::: GEOMTRAP:def 3 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "v")) "," (Set (Var "v1")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "v")) "," (Set (Var "v1")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) "iff" (Bool "(" (Bool (Set (Var "u")) "," (Set (Var "u1")) ($#r1_analoaf :::"//"::: ) (Set (Var "v")) "," (Set (Var "v1"))) & (Bool (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Set (Var "u")) ($#k1_geomtrap :::"#"::: ) (Set (Var "u1"))) "," (Set (Set (Var "v")) ($#k1_geomtrap :::"#"::: ) (Set (Var "v1"))) ($#r3_analmetr :::"are_Ort_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Set (Var "u")) ($#k1_geomtrap :::"#"::: ) (Set (Var "u1"))) "," (Set (Set (Var "v")) ($#k1_geomtrap :::"#"::: ) (Set (Var "v1"))) ($#r3_analmetr :::"are_Ort_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) ")" ) ")" ))); theorem :: GEOMTRAP:15 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "w")) "," (Set (Var "y")))) "holds" (Bool (Set (Var "u")) "," (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "v")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))))) ; theorem :: GEOMTRAP:16 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "w")) "," (Set (Var "y")))) "holds" (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u")) "," (Set (Var "v")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))))) ; theorem :: GEOMTRAP:17 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "v")) "," (Set (Var "u")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y")))) "holds" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Var "v"))))) ; theorem :: GEOMTRAP:18 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "v1")) "," (Set (Var "u")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "v1")) "," (Set (Var "u")) "," (Set (Var "u")) "," (Set (Var "v2")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y")))) "holds" (Bool "(" (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Var "u"))) & (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Var "v2"))) ")" ))) ; theorem :: GEOMTRAP:19 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "v1")) "," (Set (Var "u2")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "v1")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u2")) "," (Set (Var "v2")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "v")))) "holds" (Bool (Set (Var "u1")) "," (Set (Var "v1")) "," (Set (Var "u2")) "," (Set (Var "v2")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))))) ; theorem :: GEOMTRAP:20 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "w")) "," (Set (Var "y")))) "holds" (Bool "ex" (Set (Var "t")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "t")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) "or" (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "t")) "," (Set (Var "u1")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) ")" )))) ; theorem :: GEOMTRAP:21 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "v1")) "," (Set (Var "w")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "v1")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y")))) "holds" (Bool (Set (Var "u1")) "," (Set (Var "v1")) "," (Set (Var "u")) "," (Set (Var "v")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))))) ; theorem :: GEOMTRAP:22 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "v1")) "," (Set (Var "w")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "v1")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y")))) "holds" (Bool (Set (Var "v")) "," (Set (Var "u")) "," (Set (Var "v1")) "," (Set (Var "u1")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))))) ; theorem :: GEOMTRAP:23 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "u2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "v")) "," (Set (Var "u2")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y")))) "holds" (Bool (Set (Var "u1")) ($#r1_hidden :::"="::: ) (Set (Var "u2"))))) ; theorem :: GEOMTRAP:24 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "v1")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "v2")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Bool "not" (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Var "v"))))) "holds" (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Var "v2"))))) ; theorem :: GEOMTRAP:25 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "u1"))) & (Bool (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "v")) "," (Set (Var "v1")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool "(" (Bool (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "v")) "," (Set (Var "v2")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) "or" (Bool (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "v2")) "," (Set (Var "v")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) ")" )) "holds" (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Var "v2"))))) ; theorem :: GEOMTRAP:26 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "v1")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "v1")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y")))) "holds" (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Set (Var "u")) ($#k1_geomtrap :::"#"::: ) (Set (Var "u1"))) "," (Set (Set (Var "v")) ($#k1_geomtrap :::"#"::: ) (Set (Var "v1"))) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))))) ; theorem :: GEOMTRAP:27 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "v1")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "v1")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Bool "not" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Set (Var "u")) ($#k1_geomtrap :::"#"::: ) (Set (Var "v1"))) "," (Set (Set (Var "v")) ($#k1_geomtrap :::"#"::: ) (Set (Var "u1"))) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))))) "holds" (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Set (Var "v")) ($#k1_geomtrap :::"#"::: ) (Set (Var "u1"))) "," (Set (Set (Var "u")) ($#k1_geomtrap :::"#"::: ) (Set (Var "v1"))) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))))) ; theorem :: GEOMTRAP:28 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "u2")) "," (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "t1")) "," (Set (Var "t2")) "," (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Set (Var "u1")) ($#k1_geomtrap :::"#"::: ) (Set (Var "t1")))) & (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Set (Var "u2")) ($#k1_geomtrap :::"#"::: ) (Set (Var "t2")))) & (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v1")) ($#k1_geomtrap :::"#"::: ) (Set (Var "w1")))) & (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v2")) ($#k1_geomtrap :::"#"::: ) (Set (Var "w2")))) & (Bool (Set (Var "u1")) "," (Set (Var "u2")) "," (Set (Var "v1")) "," (Set (Var "v2")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y")))) "holds" (Bool (Set (Var "t1")) "," (Set (Var "t2")) "," (Set (Var "w1")) "," (Set (Var "w2")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))))) ; definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "w", "y", "u" be ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Const "V")); assume (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Const "w")) "," (Set (Const "y"))) ; func :::"pr1"::: "(" "w" "," "y" "," "u" ")" -> ($#m1_subset_1 :::"Real":::) means :: GEOMTRAP:def 4 (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "u" ($#r1_hidden :::"="::: ) (Set (Set "(" it ($#k1_rlvect_1 :::"*"::: ) "w" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) "y" ")" )))); end; :: deftheorem defines :::"pr1"::: GEOMTRAP:def 4 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "w")) "," (Set (Var "y")))) "holds" (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k2_geomtrap :::"pr1"::: ) "(" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "u")) ")" )) "iff" (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b5")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "y")) ")" )))) ")" )))); definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "w", "y", "u" be ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Const "V")); assume (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Const "w")) "," (Set (Const "y"))) ; func :::"pr2"::: "(" "w" "," "y" "," "u" ")" -> ($#m1_subset_1 :::"Real":::) means :: GEOMTRAP:def 5 (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "u" ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) "w" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" it ($#k1_rlvect_1 :::"*"::: ) "y" ")" )))); end; :: deftheorem defines :::"pr2"::: GEOMTRAP:def 5 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "w")) "," (Set (Var "y")))) "holds" (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k3_geomtrap :::"pr2"::: ) "(" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "u")) ")" )) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b5")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "y")) ")" )))) ")" )))); definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "w", "y", "u", "v" be ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Const "V")); func :::"PProJ"::: "(" "w" "," "y" "," "u" "," "v" ")" -> ($#m1_subset_1 :::"Real":::) equals :: GEOMTRAP:def 6 (Set (Set "(" (Set "(" ($#k2_geomtrap :::"pr1"::: ) "(" "w" "," "y" "," "u" ")" ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k2_geomtrap :::"pr1"::: ) "(" "w" "," "y" "," "v" ")" ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k3_geomtrap :::"pr2"::: ) "(" "w" "," "y" "," "u" ")" ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k3_geomtrap :::"pr2"::: ) "(" "w" "," "y" "," "v" ")" ")" ) ")" )); end; :: deftheorem defines :::"PProJ"::: GEOMTRAP:def 6 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_geomtrap :::"PProJ"::: ) "(" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "v")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k2_geomtrap :::"pr1"::: ) "(" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "u")) ")" ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k2_geomtrap :::"pr1"::: ) "(" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "v")) ")" ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k3_geomtrap :::"pr2"::: ) "(" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "u")) ")" ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k3_geomtrap :::"pr2"::: ) "(" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "v")) ")" ")" ) ")" ))))); theorem :: GEOMTRAP:29 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_geomtrap :::"PProJ"::: ) "(" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "v")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_geomtrap :::"PProJ"::: ) "(" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "v")) "," (Set (Var "u")) ")" )))) ; theorem :: GEOMTRAP:30 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "w")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "w")) "," (Set (Var "y")))) "holds" (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "v1")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set ($#k4_geomtrap :::"PProJ"::: ) "(" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set "(" (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "v1")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_geomtrap :::"PProJ"::: ) "(" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "v")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k4_geomtrap :::"PProJ"::: ) "(" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "v1")) ")" ")" ))) & (Bool (Set ($#k4_geomtrap :::"PProJ"::: ) "(" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set "(" (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "v1")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_geomtrap :::"PProJ"::: ) "(" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "v")) ")" ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k4_geomtrap :::"PProJ"::: ) "(" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "v1")) ")" ")" ))) & (Bool (Set ($#k4_geomtrap :::"PProJ"::: ) "(" (Set (Var "w")) "," (Set (Var "y")) "," (Set "(" (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "v1")) ")" ) "," (Set (Var "u")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_geomtrap :::"PProJ"::: ) "(" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "v")) "," (Set (Var "u")) ")" ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k4_geomtrap :::"PProJ"::: ) "(" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "v1")) "," (Set (Var "u")) ")" ")" ))) & (Bool (Set ($#k4_geomtrap :::"PProJ"::: ) "(" (Set (Var "w")) "," (Set (Var "y")) "," (Set "(" (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "v1")) ")" ) "," (Set (Var "u")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_geomtrap :::"PProJ"::: ) "(" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "v")) "," (Set (Var "u")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k4_geomtrap :::"PProJ"::: ) "(" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "v1")) "," (Set (Var "u")) ")" ")" ))) ")" )))) ; theorem :: GEOMTRAP:31 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "w")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "w")) "," (Set (Var "y")))) "holds" (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set ($#k4_geomtrap :::"PProJ"::: ) "(" (Set (Var "w")) "," (Set (Var "y")) "," (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" ) "," (Set (Var "v")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k4_geomtrap :::"PProJ"::: ) "(" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "v")) ")" ")" ))) & (Bool (Set ($#k4_geomtrap :::"PProJ"::: ) "(" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k4_geomtrap :::"PProJ"::: ) "(" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "v")) ")" ")" ))) & (Bool (Set ($#k4_geomtrap :::"PProJ"::: ) "(" (Set (Var "w")) "," (Set (Var "y")) "," (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" ) "," (Set (Var "v")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_geomtrap :::"PProJ"::: ) "(" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "v")) ")" ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "a")))) & (Bool (Set ($#k4_geomtrap :::"PProJ"::: ) "(" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_geomtrap :::"PProJ"::: ) "(" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "v")) ")" ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "a")))) ")" ))))) ; theorem :: GEOMTRAP:32 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "w")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "w")) "," (Set (Var "y")))) "holds" (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analmetr :::"are_Ort_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) "iff" (Bool (Set ($#k4_geomtrap :::"PProJ"::: ) "(" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "v")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )))) ; theorem :: GEOMTRAP:33 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "w")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "w")) "," (Set (Var "y")))) "holds" (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "v1")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "v1")) ($#r3_analmetr :::"are_Ort_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) "iff" (Bool (Set ($#k4_geomtrap :::"PProJ"::: ) "(" (Set (Var "w")) "," (Set (Var "y")) "," (Set "(" (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "u")) ")" ) "," (Set "(" (Set (Var "v1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "u1")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )))) ; theorem :: GEOMTRAP:34 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "w")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "w")) "," (Set (Var "y")))) "holds" (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "v1")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k4_geomtrap :::"PProJ"::: ) "(" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set "(" (Set (Var "v")) ($#k1_geomtrap :::"#"::: ) (Set (Var "v1")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_geomtrap :::"PProJ"::: ) "(" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "v")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k4_geomtrap :::"PProJ"::: ) "(" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "v1")) ")" ")" )))))) ; theorem :: GEOMTRAP:35 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "w")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "w")) "," (Set (Var "y")))) "holds" (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "v")))) "holds" (Bool (Set ($#k4_geomtrap :::"PProJ"::: ) "(" (Set (Var "w")) "," (Set (Var "y")) "," (Set "(" (Set (Var "u")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "v")) ")" ) "," (Set "(" (Set (Var "u")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "v")) ")" ) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: GEOMTRAP:36 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "w")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "w")) "," (Set (Var "y")))) "holds" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "v9")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "u")) "," (Set (Var "v")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k4_geomtrap :::"PProJ"::: ) "(" (Set (Var "w")) "," (Set (Var "y")) "," (Set "(" (Set (Var "p")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "q")) ")" ) "," (Set "(" (Set (Var "p")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "q")) ")" ) ")" ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k4_geomtrap :::"PProJ"::: ) "(" (Set (Var "w")) "," (Set (Var "y")) "," (Set "(" (Set (Var "p")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "q")) ")" ) "," (Set (Var "u")) ")" ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k4_geomtrap :::"PProJ"::: ) "(" (Set (Var "w")) "," (Set (Var "y")) "," (Set "(" (Set (Var "p")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "q")) ")" ) "," (Set "(" (Set (Var "p")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "q")) ")" ) ")" ")" ) ($#k2_real_1 :::"""::: ) ")" ))) & (Bool (Set (Var "v9")) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "A")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "q")) ")" ) ")" )))) "holds" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "v9"))))))) ; theorem :: GEOMTRAP:37 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "w")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "w")) "," (Set (Var "y")))) "holds" (Bool "for" (Set (Var "u")) "," (Set (Var "u9")) "," (Set (Var "u1")) "," (Set (Var "u2")) "," (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "t1")) "," (Set (Var "t2")) "," (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "u9"))) & (Bool (Set (Var "u")) "," (Set (Var "u9")) "," (Set (Var "u1")) "," (Set (Var "t1")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "u9")) "," (Set (Var "u2")) "," (Set (Var "t2")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "u9")) "," (Set (Var "v1")) "," (Set (Var "w1")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "u9")) "," (Set (Var "v2")) "," (Set (Var "w2")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "u1")) "," (Set (Var "u2")) ($#r1_analoaf :::"//"::: ) (Set (Var "v1")) "," (Set (Var "v2")))) "holds" (Bool (Set (Var "t1")) "," (Set (Var "t2")) ($#r1_analoaf :::"//"::: ) (Set (Var "w1")) "," (Set (Var "w2")))))) ; theorem :: GEOMTRAP:38 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "w")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "w")) "," (Set (Var "y")))) "holds" (Bool "for" (Set (Var "u")) "," (Set (Var "u9")) "," (Set (Var "u1")) "," (Set (Var "u2")) "," (Set (Var "v1")) "," (Set (Var "t1")) "," (Set (Var "t2")) "," (Set (Var "w1")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "u9"))) & (Bool (Set (Var "u")) "," (Set (Var "u9")) "," (Set (Var "u1")) "," (Set (Var "t1")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "u9")) "," (Set (Var "u2")) "," (Set (Var "t2")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "u9")) "," (Set (Var "v1")) "," (Set (Var "w1")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "u1")) ($#k1_geomtrap :::"#"::: ) (Set (Var "u2"))))) "holds" (Bool (Set (Var "w1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "t1")) ($#k1_geomtrap :::"#"::: ) (Set (Var "t2"))))))) ; theorem :: GEOMTRAP:39 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "w")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "w")) "," (Set (Var "y")))) "holds" (Bool "for" (Set (Var "u")) "," (Set (Var "u9")) "," (Set (Var "u1")) "," (Set (Var "u2")) "," (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "u9"))) & (Bool (Set (Var "u")) "," (Set (Var "u9")) "," (Set (Var "u1")) "," (Set (Var "t1")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "u9")) "," (Set (Var "u2")) "," (Set (Var "t2")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y")))) "holds" (Bool (Set (Var "u")) "," (Set (Var "u9")) "," (Set (Set (Var "u1")) ($#k1_geomtrap :::"#"::: ) (Set (Var "u2"))) "," (Set (Set (Var "t1")) ($#k1_geomtrap :::"#"::: ) (Set (Var "t2"))) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y")))))) ; theorem :: GEOMTRAP:40 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "w")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "w")) "," (Set (Var "y")))) "holds" (Bool "for" (Set (Var "u")) "," (Set (Var "u9")) "," (Set (Var "u1")) "," (Set (Var "u2")) "," (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "t1")) "," (Set (Var "t2")) "," (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "u9"))) & (Bool (Set (Var "u")) "," (Set (Var "u9")) "," (Set (Var "u1")) "," (Set (Var "t1")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "u9")) "," (Set (Var "u2")) "," (Set (Var "t2")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "u9")) "," (Set (Var "v1")) "," (Set (Var "w1")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "u9")) "," (Set (Var "v2")) "," (Set (Var "w2")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "u1")) "," (Set (Var "u2")) "," (Set (Var "v1")) "," (Set (Var "v2")) ($#r3_analmetr :::"are_Ort_wrt"::: ) (Set (Var "w")) "," (Set (Var "y")))) "holds" (Bool (Set (Var "t1")) "," (Set (Var "t2")) "," (Set (Var "w1")) "," (Set (Var "w2")) ($#r3_analmetr :::"are_Ort_wrt"::: ) (Set (Var "w")) "," (Set (Var "y")))))) ; theorem :: GEOMTRAP:41 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "u9")) "," (Set (Var "u1")) "," (Set (Var "u2")) "," (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "t1")) "," (Set (Var "t2")) "," (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "u9"))) & (Bool (Set (Var "u")) "," (Set (Var "u9")) "," (Set (Var "u1")) "," (Set (Var "t1")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "u9")) "," (Set (Var "u2")) "," (Set (Var "t2")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "u9")) "," (Set (Var "v1")) "," (Set (Var "w1")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "u9")) "," (Set (Var "v2")) "," (Set (Var "w2")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "u1")) "," (Set (Var "u2")) "," (Set (Var "v1")) "," (Set (Var "v2")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y")))) "holds" (Bool (Set (Var "t1")) "," (Set (Var "t2")) "," (Set (Var "w1")) "," (Set (Var "w2")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))))) ; definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "w", "y" be ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Const "V")); func :::"DTrapezium"::: "(" "V" "," "w" "," "y" ")" -> ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") ($#k2_zfmisc_1 :::":]"::: ) ) means :: GEOMTRAP:def 7 (Bool "for" (Set (Var "x")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "v")) "," (Set (Var "v1")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" "V" "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "u")) "," (Set (Var "u1")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "v")) "," (Set (Var "v1")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "v")) "," (Set (Var "v1")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) "w" "," "y") ")" )) ")" )); end; :: deftheorem defines :::"DTrapezium"::: GEOMTRAP:def 7 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "w")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k5_geomtrap :::"DTrapezium"::: ) "(" (Set (Var "V")) "," (Set (Var "w")) "," (Set (Var "y")) ")" )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) "iff" (Bool "ex" (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "v")) "," (Set (Var "v1")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "u")) "," (Set (Var "u1")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "v")) "," (Set (Var "v1")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "v")) "," (Set (Var "v1")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) ")" )) ")" )) ")" )))); theorem :: GEOMTRAP:42 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "v1")) "," (Set (Var "w")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "u")) "," (Set (Var "v")) ($#k1_domain_1 :::"]"::: ) ) "," (Set ($#k1_domain_1 :::"["::: ) (Set (Var "u1")) "," (Set (Var "v1")) ($#k1_domain_1 :::"]"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k5_geomtrap :::"DTrapezium"::: ) "(" (Set (Var "V")) "," (Set (Var "w")) "," (Set (Var "y")) ")" )) "iff" (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "v1")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) ")" ))) ; definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); func :::"MidPoint"::: "V" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") means :: GEOMTRAP:def 8 (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" "V" "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "u")) "," (Set (Var "v")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k1_geomtrap :::"#"::: ) (Set (Var "v"))))); end; :: deftheorem defines :::"MidPoint"::: GEOMTRAP:def 8 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k6_geomtrap :::"MidPoint"::: ) (Set (Var "V")))) "iff" (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "b2")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "u")) "," (Set (Var "v")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k1_geomtrap :::"#"::: ) (Set (Var "v"))))) ")" ))); definitionattr "c1" is :::"strict"::: ; struct :::"AfMidStruct"::: -> ($#l1_analoaf :::"AffinStruct"::: ) "," ($#l1_midsp_1 :::"MidStr"::: ) ; aggr :::"AfMidStruct":::(# :::"carrier":::, :::"MIDPOINT":::, :::"CONGR"::: #) -> ($#l1_geomtrap :::"AfMidStruct"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_geomtrap :::"strict"::: ) for ($#l1_geomtrap :::"AfMidStruct"::: ) ; end; definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "w", "y" be ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Const "V")); func :::"DTrSpace"::: "(" "V" "," "w" "," "y" ")" -> ($#v1_geomtrap :::"strict"::: ) ($#l1_geomtrap :::"AfMidStruct"::: ) equals :: GEOMTRAP:def 9 (Set ($#g1_geomtrap :::"AfMidStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "(" ($#k6_geomtrap :::"MidPoint"::: ) "V" ")" ) "," (Set "(" ($#k5_geomtrap :::"DTrapezium"::: ) "(" "V" "," "w" "," "y" ")" ")" ) "#)" ); end; :: deftheorem defines :::"DTrSpace"::: GEOMTRAP:def 9 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "w")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k7_geomtrap :::"DTrSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "w")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#g1_geomtrap :::"AfMidStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set "(" ($#k6_geomtrap :::"MidPoint"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k5_geomtrap :::"DTrapezium"::: ) "(" (Set (Var "V")) "," (Set (Var "w")) "," (Set (Var "y")) ")" ")" ) "#)" )))); registrationlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "w", "y" be ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Const "V")); cluster (Set ($#k7_geomtrap :::"DTrSpace"::: ) "(" "V" "," "w" "," "y" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_geomtrap :::"strict"::: ) ; end; definitionlet "AMS" be ($#l1_geomtrap :::"AfMidStruct"::: ) ; func :::"Af"::: "AMS" -> ($#v1_analoaf :::"strict"::: ) ($#l1_analoaf :::"AffinStruct"::: ) equals :: GEOMTRAP:def 10 (Set ($#g1_analoaf :::"AffinStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "AMS") "," (Set "the" ($#u1_analoaf :::"CONGR"::: ) "of" "AMS") "#)" ); end; :: deftheorem defines :::"Af"::: GEOMTRAP:def 10 : (Bool "for" (Set (Var "AMS")) "being" ($#l1_geomtrap :::"AfMidStruct"::: ) "holds" (Bool (Set ($#k8_geomtrap :::"Af"::: ) (Set (Var "AMS"))) ($#r1_hidden :::"="::: ) (Set ($#g1_analoaf :::"AffinStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AMS"))) "," (Set "the" ($#u1_analoaf :::"CONGR"::: ) "of" (Set (Var "AMS"))) "#)" ))); registrationlet "AMS" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_geomtrap :::"AfMidStruct"::: ) ; cluster (Set ($#k8_geomtrap :::"Af"::: ) "AMS") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_analoaf :::"strict"::: ) ; end; definitionlet "AMS" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_geomtrap :::"AfMidStruct"::: ) ; let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "AMS")); func "a" :::"#"::: "b" -> ($#m1_subset_1 :::"Element":::) "of" "AMS" equals :: GEOMTRAP:def 11 (Set (Set "the" ($#u1_midsp_1 :::"MIDPOINT"::: ) "of" "AMS") ($#k5_binop_1 :::"."::: ) "(" "a" "," "b" ")" ); end; :: deftheorem defines :::"#"::: GEOMTRAP:def 11 : (Bool "for" (Set (Var "AMS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_geomtrap :::"AfMidStruct"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AMS")) "holds" (Bool (Set (Set (Var "a")) ($#k9_geomtrap :::"#"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_midsp_1 :::"MIDPOINT"::: ) "of" (Set (Var "AMS"))) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )))); theorem :: GEOMTRAP:43 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "w")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k7_geomtrap :::"DTrSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "w")) "," (Set (Var "y")) ")" ")" ))) "iff" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V"))) ")" )))) ; theorem :: GEOMTRAP:44 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "v1")) "," (Set (Var "w")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "a1")) "," (Set (Var "b1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k7_geomtrap :::"DTrSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "w")) "," (Set (Var "y")) ")" ")" ) "st" (Bool (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Var "u1")) ($#r1_hidden :::"="::: ) (Set (Var "a1"))) & (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Var "b1")))) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a1")) "," (Set (Var "b1"))) "iff" (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "v1")) ($#r2_geomtrap :::"are_DTr_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) ")" )))) ; theorem :: GEOMTRAP:45 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k7_geomtrap :::"DTrSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "w")) "," (Set (Var "y")) ")" ")" ) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "b")))) "holds" (Bool (Set (Set (Var "u")) ($#k1_geomtrap :::"#"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k9_geomtrap :::"#"::: ) (Set (Var "b"))))))) ; definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_geomtrap :::"AfMidStruct"::: ) ; attr "IT" is :::"MidOrdTrapSpace-like"::: means :: GEOMTRAP:def 12 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "c1")) "," (Set (Var "d1")) "," (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k9_geomtrap :::"#"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k9_geomtrap :::"#"::: ) (Set (Var "a")))) & (Bool (Set (Set (Var "a")) ($#k9_geomtrap :::"#"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set "(" (Set (Var "a")) ($#k9_geomtrap :::"#"::: ) (Set (Var "b")) ")" ) ($#k9_geomtrap :::"#"::: ) (Set "(" (Set (Var "c")) ($#k9_geomtrap :::"#"::: ) (Set (Var "d")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k9_geomtrap :::"#"::: ) (Set (Var "c")) ")" ) ($#k9_geomtrap :::"#"::: ) (Set "(" (Set (Var "b")) ($#k9_geomtrap :::"#"::: ) (Set (Var "d")) ")" ))) & (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Set (Set (Var "p")) ($#k9_geomtrap :::"#"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "b")))) & "(" (Bool (Bool (Set (Set (Var "a")) ($#k9_geomtrap :::"#"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k9_geomtrap :::"#"::: ) (Set (Var "c"))))) "implies" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "c"))) ")" & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) "implies" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Set (Var "a")) ($#k9_geomtrap :::"#"::: ) (Set (Var "c"))) "," (Set (Set (Var "b")) ($#k9_geomtrap :::"#"::: ) (Set (Var "d")))) ")" & (Bool "(" "not" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) "or" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Set (Var "a")) ($#k9_geomtrap :::"#"::: ) (Set (Var "d"))) "," (Set (Set (Var "b")) ($#k9_geomtrap :::"#"::: ) (Set (Var "c")))) "or" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Set (Var "b")) ($#k9_geomtrap :::"#"::: ) (Set (Var "c"))) "," (Set (Set (Var "a")) ($#k9_geomtrap :::"#"::: ) (Set (Var "d")))) ")" ) & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Set (Var "a")) ($#k9_geomtrap :::"#"::: ) (Set (Var "a1"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Set (Var "b")) ($#k9_geomtrap :::"#"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Set (Var "c")) ($#k9_geomtrap :::"#"::: ) (Set (Var "c1"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Set (Var "d")) ($#k9_geomtrap :::"#"::: ) (Set (Var "d1"))) ($#r1_hidden :::"="::: ) (Set (Var "p")))) "implies" (Bool (Set (Var "a1")) "," (Set (Var "b1")) ($#r2_analoaf :::"//"::: ) (Set (Var "c1")) "," (Set (Var "d1"))) ")" & "(" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q"))) & (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "a1"))) & (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "b1"))) & (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "c1"))) & (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "d")) "," (Set (Var "d1"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) "implies" (Bool (Set (Var "a1")) "," (Set (Var "b1")) ($#r2_analoaf :::"//"::: ) (Set (Var "c1")) "," (Set (Var "d1"))) ")" & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "c")))) "implies" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "c"))) ")" ) ")" & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a1")) "," (Set (Var "b1"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c1")) "," (Set (Var "d1"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "implies" (Bool (Set (Var "a1")) "," (Set (Var "b1")) ($#r2_analoaf :::"//"::: ) (Set (Var "c1")) "," (Set (Var "d1"))) ")" & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) "implies" (Bool "(" (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "d")) "," (Set (Var "c"))) ")" ) ")" & (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) "or" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "d")) "," (Set (Var "c"))) ")" )) & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "p"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "q"))) & (Bool (Bool "not" (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) "implies" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "q"))) ")" ")" )); end; :: deftheorem defines :::"MidOrdTrapSpace-like"::: GEOMTRAP:def 12 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_geomtrap :::"AfMidStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_geomtrap :::"MidOrdTrapSpace-like"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "c1")) "," (Set (Var "d1")) "," (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k9_geomtrap :::"#"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k9_geomtrap :::"#"::: ) (Set (Var "a")))) & (Bool (Set (Set (Var "a")) ($#k9_geomtrap :::"#"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set "(" (Set (Var "a")) ($#k9_geomtrap :::"#"::: ) (Set (Var "b")) ")" ) ($#k9_geomtrap :::"#"::: ) (Set "(" (Set (Var "c")) ($#k9_geomtrap :::"#"::: ) (Set (Var "d")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k9_geomtrap :::"#"::: ) (Set (Var "c")) ")" ) ($#k9_geomtrap :::"#"::: ) (Set "(" (Set (Var "b")) ($#k9_geomtrap :::"#"::: ) (Set (Var "d")) ")" ))) & (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Set (Set (Var "p")) ($#k9_geomtrap :::"#"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "b")))) & "(" (Bool (Bool (Set (Set (Var "a")) ($#k9_geomtrap :::"#"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k9_geomtrap :::"#"::: ) (Set (Var "c"))))) "implies" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "c"))) ")" & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) "implies" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Set (Var "a")) ($#k9_geomtrap :::"#"::: ) (Set (Var "c"))) "," (Set (Set (Var "b")) ($#k9_geomtrap :::"#"::: ) (Set (Var "d")))) ")" & (Bool "(" "not" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) "or" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Set (Var "a")) ($#k9_geomtrap :::"#"::: ) (Set (Var "d"))) "," (Set (Set (Var "b")) ($#k9_geomtrap :::"#"::: ) (Set (Var "c")))) "or" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Set (Var "b")) ($#k9_geomtrap :::"#"::: ) (Set (Var "c"))) "," (Set (Set (Var "a")) ($#k9_geomtrap :::"#"::: ) (Set (Var "d")))) ")" ) & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Set (Var "a")) ($#k9_geomtrap :::"#"::: ) (Set (Var "a1"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Set (Var "b")) ($#k9_geomtrap :::"#"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Set (Var "c")) ($#k9_geomtrap :::"#"::: ) (Set (Var "c1"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Set (Var "d")) ($#k9_geomtrap :::"#"::: ) (Set (Var "d1"))) ($#r1_hidden :::"="::: ) (Set (Var "p")))) "implies" (Bool (Set (Var "a1")) "," (Set (Var "b1")) ($#r2_analoaf :::"//"::: ) (Set (Var "c1")) "," (Set (Var "d1"))) ")" & "(" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q"))) & (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "a1"))) & (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "b1"))) & (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "c1"))) & (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "d")) "," (Set (Var "d1"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) "implies" (Bool (Set (Var "a1")) "," (Set (Var "b1")) ($#r2_analoaf :::"//"::: ) (Set (Var "c1")) "," (Set (Var "d1"))) ")" & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "c")))) "implies" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "c"))) ")" ) ")" & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a1")) "," (Set (Var "b1"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c1")) "," (Set (Var "d1"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "implies" (Bool (Set (Var "a1")) "," (Set (Var "b1")) ($#r2_analoaf :::"//"::: ) (Set (Var "c1")) "," (Set (Var "d1"))) ")" & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) "implies" (Bool "(" (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "d")) "," (Set (Var "c"))) ")" ) ")" & (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) "or" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "d")) "," (Set (Var "c"))) ")" )) & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "p"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "q"))) & (Bool (Bool "not" (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) "implies" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "q"))) ")" ")" )) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_geomtrap :::"strict"::: ) ($#v2_geomtrap :::"MidOrdTrapSpace-like"::: ) for ($#l1_geomtrap :::"AfMidStruct"::: ) ; end; definitionmode MidOrdTrapSpace is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_geomtrap :::"MidOrdTrapSpace-like"::: ) ($#l1_geomtrap :::"AfMidStruct"::: ) ; end; theorem :: GEOMTRAP:46 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "w")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "w")) "," (Set (Var "y")))) "holds" (Bool (Set ($#k7_geomtrap :::"DTrSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "w")) "," (Set (Var "y")) ")" ) "is" ($#l1_geomtrap :::"MidOrdTrapSpace":::)))) ; definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) ; attr "IT" is :::"OrdTrapSpace-like"::: means :: GEOMTRAP:def 13 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "c1")) "," (Set (Var "d1")) "," (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool "(" "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "c")))) "implies" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "c"))) ")" ) ")" & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a1")) "," (Set (Var "b1"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c1")) "," (Set (Var "d1"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "implies" (Bool (Set (Var "a1")) "," (Set (Var "b1")) ($#r2_analoaf :::"//"::: ) (Set (Var "c1")) "," (Set (Var "d1"))) ")" & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) "implies" (Bool "(" (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "d")) "," (Set (Var "c"))) ")" ) ")" & (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) "or" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "d")) "," (Set (Var "c"))) ")" )) & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "p"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "q"))) & (Bool (Bool "not" (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) "implies" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "q"))) ")" ")" )); end; :: deftheorem defines :::"OrdTrapSpace-like"::: GEOMTRAP:def 13 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_geomtrap :::"OrdTrapSpace-like"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "c1")) "," (Set (Var "d1")) "," (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "c")))) "implies" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "c"))) ")" ) ")" & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a1")) "," (Set (Var "b1"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c1")) "," (Set (Var "d1"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "implies" (Bool (Set (Var "a1")) "," (Set (Var "b1")) ($#r2_analoaf :::"//"::: ) (Set (Var "c1")) "," (Set (Var "d1"))) ")" & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) "implies" (Bool "(" (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "d")) "," (Set (Var "c"))) ")" ) ")" & (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) "or" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "d")) "," (Set (Var "c"))) ")" )) & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "p"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "q"))) & (Bool (Bool "not" (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) "implies" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "q"))) ")" ")" )) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_analoaf :::"strict"::: ) ($#v3_geomtrap :::"OrdTrapSpace-like"::: ) for ($#l1_analoaf :::"AffinStruct"::: ) ; end; definitionmode OrdTrapSpace is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_geomtrap :::"OrdTrapSpace-like"::: ) ($#l1_analoaf :::"AffinStruct"::: ) ; end; registrationlet "MOS" be ($#l1_geomtrap :::"MidOrdTrapSpace":::); cluster (Set ($#k8_geomtrap :::"Af"::: ) "MOS") -> ($#v1_analoaf :::"strict"::: ) ($#v3_geomtrap :::"OrdTrapSpace-like"::: ) ; end; theorem :: GEOMTRAP:47 (Bool "for" (Set (Var "OTS")) "being" ($#l1_analoaf :::"OrdTrapSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OTS"))) "iff" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_diraf :::"Lambda"::: ) (Set (Var "OTS")) ")" )) ")" ))) ; theorem :: GEOMTRAP:48 (Bool "for" (Set (Var "OTS")) "being" ($#l1_analoaf :::"OrdTrapSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OTS")) (Bool "for" (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "," (Set (Var "d9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_diraf :::"Lambda"::: ) (Set (Var "OTS")) ")" ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "a9"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "b9"))) & (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Var "c9"))) & (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Var "d9")))) "holds" (Bool "(" (Bool (Set (Var "a9")) "," (Set (Var "b9")) ($#r2_analoaf :::"//"::: ) (Set (Var "c9")) "," (Set (Var "d9"))) "iff" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) "or" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "d")) "," (Set (Var "c"))) ")" ) ")" )))) ; definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) ; attr "IT" is :::"TrapSpace-like"::: means :: GEOMTRAP:def 14 (Bool "for" (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "," (Set (Var "d9")) "," (Set (Var "p9")) "," (Set (Var "q9")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool "(" (Bool (Set (Var "a9")) "," (Set (Var "b9")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "a9"))) & "(" (Bool (Bool (Set (Var "a9")) "," (Set (Var "b9")) ($#r2_analoaf :::"//"::: ) (Set (Var "c9")) "," (Set (Var "d9"))) & (Bool (Set (Var "a9")) "," (Set (Var "b9")) ($#r2_analoaf :::"//"::: ) (Set (Var "c9")) "," (Set (Var "q9"))) & (Bool (Bool "not" (Set (Var "a9")) ($#r1_hidden :::"="::: ) (Set (Var "b9"))))) "implies" (Bool (Set (Var "d9")) ($#r1_hidden :::"="::: ) (Set (Var "q9"))) ")" & "(" (Bool (Bool (Set (Var "p9")) ($#r1_hidden :::"<>"::: ) (Set (Var "q9"))) & (Bool (Set (Var "p9")) "," (Set (Var "q9")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "b9"))) & (Bool (Set (Var "p9")) "," (Set (Var "q9")) ($#r2_analoaf :::"//"::: ) (Set (Var "c9")) "," (Set (Var "d9")))) "implies" (Bool (Set (Var "a9")) "," (Set (Var "b9")) ($#r2_analoaf :::"//"::: ) (Set (Var "c9")) "," (Set (Var "d9"))) ")" & "(" (Bool (Bool (Set (Var "a9")) "," (Set (Var "b9")) ($#r2_analoaf :::"//"::: ) (Set (Var "c9")) "," (Set (Var "d9")))) "implies" (Bool (Set (Var "c9")) "," (Set (Var "d9")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "b9"))) ")" & (Bool "ex" (Set (Var "x9")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Set (Var "a9")) "," (Set (Var "b9")) ($#r2_analoaf :::"//"::: ) (Set (Var "c9")) "," (Set (Var "x9")))) ")" )); end; :: deftheorem defines :::"TrapSpace-like"::: GEOMTRAP:def 14 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v4_geomtrap :::"TrapSpace-like"::: ) ) "iff" (Bool "for" (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "," (Set (Var "d9")) "," (Set (Var "p9")) "," (Set (Var "q9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool "(" (Bool (Set (Var "a9")) "," (Set (Var "b9")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "a9"))) & "(" (Bool (Bool (Set (Var "a9")) "," (Set (Var "b9")) ($#r2_analoaf :::"//"::: ) (Set (Var "c9")) "," (Set (Var "d9"))) & (Bool (Set (Var "a9")) "," (Set (Var "b9")) ($#r2_analoaf :::"//"::: ) (Set (Var "c9")) "," (Set (Var "q9"))) & (Bool (Bool "not" (Set (Var "a9")) ($#r1_hidden :::"="::: ) (Set (Var "b9"))))) "implies" (Bool (Set (Var "d9")) ($#r1_hidden :::"="::: ) (Set (Var "q9"))) ")" & "(" (Bool (Bool (Set (Var "p9")) ($#r1_hidden :::"<>"::: ) (Set (Var "q9"))) & (Bool (Set (Var "p9")) "," (Set (Var "q9")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "b9"))) & (Bool (Set (Var "p9")) "," (Set (Var "q9")) ($#r2_analoaf :::"//"::: ) (Set (Var "c9")) "," (Set (Var "d9")))) "implies" (Bool (Set (Var "a9")) "," (Set (Var "b9")) ($#r2_analoaf :::"//"::: ) (Set (Var "c9")) "," (Set (Var "d9"))) ")" & "(" (Bool (Bool (Set (Var "a9")) "," (Set (Var "b9")) ($#r2_analoaf :::"//"::: ) (Set (Var "c9")) "," (Set (Var "d9")))) "implies" (Bool (Set (Var "c9")) "," (Set (Var "d9")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "b9"))) ")" & (Bool "ex" (Set (Var "x9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Set (Var "a9")) "," (Set (Var "b9")) ($#r2_analoaf :::"//"::: ) (Set (Var "c9")) "," (Set (Var "x9")))) ")" )) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_analoaf :::"strict"::: ) ($#v4_geomtrap :::"TrapSpace-like"::: ) for ($#l1_analoaf :::"AffinStruct"::: ) ; end; definitionmode TrapSpace is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_geomtrap :::"TrapSpace-like"::: ) ($#l1_analoaf :::"AffinStruct"::: ) ; end; registrationlet "OTS" be ($#l1_analoaf :::"OrdTrapSpace":::); cluster (Set ($#k2_diraf :::"Lambda"::: ) "OTS") -> ($#v4_geomtrap :::"TrapSpace-like"::: ) ; end; definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) ; attr "IT" is :::"Regular"::: means :: GEOMTRAP:def 15 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "a")) "," (Set (Var "a1")) "," (Set (Var "b")) "," (Set (Var "b1")) "," (Set (Var "c")) "," (Set (Var "c1")) "," (Set (Var "d")) "," (Set (Var "d1")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q"))) & (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "a1"))) & (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "b1"))) & (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "c1"))) & (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "d")) "," (Set (Var "d1"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool (Set (Var "a1")) "," (Set (Var "b1")) ($#r2_analoaf :::"//"::: ) (Set (Var "c1")) "," (Set (Var "d1")))); end; :: deftheorem defines :::"Regular"::: GEOMTRAP:def 15 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v5_geomtrap :::"Regular"::: ) ) "iff" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "a")) "," (Set (Var "a1")) "," (Set (Var "b")) "," (Set (Var "b1")) "," (Set (Var "c")) "," (Set (Var "c1")) "," (Set (Var "d")) "," (Set (Var "d1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q"))) & (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "a1"))) & (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "b1"))) & (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "c1"))) & (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "d")) "," (Set (Var "d1"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool (Set (Var "a1")) "," (Set (Var "b1")) ($#r2_analoaf :::"//"::: ) (Set (Var "c1")) "," (Set (Var "d1")))) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_analoaf :::"strict"::: ) ($#v3_geomtrap :::"OrdTrapSpace-like"::: ) ($#v5_geomtrap :::"Regular"::: ) for ($#l1_analoaf :::"AffinStruct"::: ) ; end; registrationlet "MOS" be ($#l1_geomtrap :::"MidOrdTrapSpace":::); cluster (Set ($#k8_geomtrap :::"Af"::: ) "MOS") -> ($#v1_analoaf :::"strict"::: ) ($#v5_geomtrap :::"Regular"::: ) ; end;