:: ANALORT semantic presentation begin definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "x", "y", "u" be ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Const "V")); func :::"Ortm"::: "(" "x" "," "y" "," "u" ")" -> ($#m1_subset_1 :::"VECTOR":::) "of" "V" equals :: ANALORT:def 1 (Set (Set "(" (Set "(" ($#k2_geomtrap :::"pr1"::: ) "(" "x" "," "y" "," "u" ")" ")" ) ($#k1_rlvect_1 :::"*"::: ) "x" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k3_geomtrap :::"pr2"::: ) "(" "x" "," "y" "," "u" ")" ")" ) ")" ) ($#k1_rlvect_1 :::"*"::: ) "y" ")" )); end; :: deftheorem defines :::"Ortm"::: ANALORT:def 1 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k1_analort :::"Ortm"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k2_geomtrap :::"pr1"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) ")" ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k3_geomtrap :::"pr2"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) ")" ")" ) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "y")) ")" ))))); theorem :: ANALORT:1 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (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 "x")) "," (Set (Var "y")))) "holds" (Bool (Set ($#k1_analort :::"Ortm"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set "(" (Set (Var "u")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "v")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_analort :::"Ortm"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k1_analort :::"Ortm"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "v")) ")" ")" ))))) ; theorem :: ANALORT:2 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "x")) "," (Set (Var "y")))) "holds" (Bool (Set ($#k1_analort :::"Ortm"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set "(" (Set (Var "n")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" ($#k1_analort :::"Ortm"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) ")" ")" )))))) ; theorem :: ANALORT:3 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "x")) "," (Set (Var "y")))) "holds" (Bool (Set ($#k1_analort :::"Ortm"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))))) ; theorem :: ANALORT:4 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "x")) "," (Set (Var "y")))) "holds" (Bool (Set ($#k1_analort :::"Ortm"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "u")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k1_analort :::"Ortm"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) ")" ")" ))))) ; theorem :: ANALORT:5 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (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 "x")) "," (Set (Var "y")))) "holds" (Bool (Set ($#k1_analort :::"Ortm"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set "(" (Set (Var "u")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "v")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_analort :::"Ortm"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k1_analort :::"Ortm"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "v")) ")" ")" ))))) ; theorem :: ANALORT:6 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (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 "x")) "," (Set (Var "y"))) & (Bool (Set ($#k1_analort :::"Ortm"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_analort :::"Ortm"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "v")) ")" ))) "holds" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Var "v"))))) ; theorem :: ANALORT:7 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "x")) "," (Set (Var "y")))) "holds" (Bool (Set ($#k1_analort :::"Ortm"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set "(" ($#k1_analort :::"Ortm"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "u"))))) ; theorem :: ANALORT:8 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "x")) "," (Set (Var "y")))) "holds" (Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set ($#k1_analort :::"Ortm"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "v")) ")" ))))) ; definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "x", "y", "u" be ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Const "V")); func :::"Orte"::: "(" "x" "," "y" "," "u" ")" -> ($#m1_subset_1 :::"VECTOR":::) "of" "V" equals :: ANALORT:def 2 (Set (Set "(" (Set "(" ($#k3_geomtrap :::"pr2"::: ) "(" "x" "," "y" "," "u" ")" ")" ) ($#k1_rlvect_1 :::"*"::: ) "x" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k2_geomtrap :::"pr1"::: ) "(" "x" "," "y" "," "u" ")" ")" ) ")" ) ($#k1_rlvect_1 :::"*"::: ) "y" ")" )); end; :: deftheorem defines :::"Orte"::: ANALORT:def 2 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k2_analort :::"Orte"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_geomtrap :::"pr2"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) ")" ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k2_geomtrap :::"pr1"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) ")" ")" ) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "y")) ")" ))))); theorem :: ANALORT:9 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "x")) "," (Set (Var "y")))) "holds" (Bool (Set ($#k2_analort :::"Orte"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "v")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k2_analort :::"Orte"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "v")) ")" ")" ))))) ; theorem :: ANALORT:10 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (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 "x")) "," (Set (Var "y")))) "holds" (Bool (Set ($#k2_analort :::"Orte"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set "(" (Set (Var "u")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "v")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_analort :::"Orte"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k2_analort :::"Orte"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "v")) ")" ")" ))))) ; theorem :: ANALORT:11 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (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 "x")) "," (Set (Var "y")))) "holds" (Bool (Set ($#k2_analort :::"Orte"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set "(" (Set (Var "u")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "v")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_analort :::"Orte"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k2_analort :::"Orte"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "v")) ")" ")" ))))) ; theorem :: ANALORT:12 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "x")) "," (Set (Var "y")))) "holds" (Bool (Set ($#k2_analort :::"Orte"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set "(" (Set (Var "n")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" ($#k2_analort :::"Orte"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) ")" ")" )))))) ; theorem :: ANALORT:13 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (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 "x")) "," (Set (Var "y"))) & (Bool (Set ($#k2_analort :::"Orte"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_analort :::"Orte"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "v")) ")" ))) "holds" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Var "v"))))) ; theorem :: ANALORT:14 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "x")) "," (Set (Var "y")))) "holds" (Bool (Set ($#k2_analort :::"Orte"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set "(" ($#k2_analort :::"Orte"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "u")))))) ; theorem :: ANALORT:15 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "x")) "," (Set (Var "y")))) "holds" (Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Set ($#k2_analort :::"Orte"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "v")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "u")))))) ; definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "x", "y", "u", "v", "u1", "v1" be ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Const "V")); pred "u" "," "v" "," "u1" "," "v1" :::"are_COrte_wrt"::: "x" "," "y" means :: ANALORT:def 3 (Bool (Set ($#k2_analort :::"Orte"::: ) "(" "x" "," "y" "," "u" ")" ) "," (Set ($#k2_analort :::"Orte"::: ) "(" "x" "," "y" "," "v" ")" ) ($#r1_analoaf :::"//"::: ) "u1" "," "v1"); pred "u" "," "v" "," "u1" "," "v1" :::"are_COrtm_wrt"::: "x" "," "y" means :: ANALORT:def 4 (Bool (Set ($#k1_analort :::"Ortm"::: ) "(" "x" "," "y" "," "u" ")" ) "," (Set ($#k1_analort :::"Ortm"::: ) "(" "x" "," "y" "," "v" ")" ) ($#r1_analoaf :::"//"::: ) "u1" "," "v1"); end; :: deftheorem defines :::"are_COrte_wrt"::: ANALORT:def 3 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (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")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) "iff" (Bool (Set ($#k2_analort :::"Orte"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) ")" ) "," (Set ($#k2_analort :::"Orte"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "v")) ")" ) ($#r1_analoaf :::"//"::: ) (Set (Var "u1")) "," (Set (Var "v1"))) ")" ))); :: deftheorem defines :::"are_COrtm_wrt"::: ANALORT:def 4 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (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")) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) "iff" (Bool (Set ($#k1_analort :::"Ortm"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) ")" ) "," (Set ($#k1_analort :::"Ortm"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "v")) ")" ) ($#r1_analoaf :::"//"::: ) (Set (Var "u1")) "," (Set (Var "v1"))) ")" ))); theorem :: ANALORT:16 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (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 "x")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r1_analoaf :::"//"::: ) (Set (Var "u1")) "," (Set (Var "v1")))) "holds" (Bool (Set ($#k2_analort :::"Orte"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) ")" ) "," (Set ($#k2_analort :::"Orte"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "v")) ")" ) ($#r1_analoaf :::"//"::: ) (Set ($#k2_analort :::"Orte"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u1")) ")" ) "," (Set ($#k2_analort :::"Orte"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "v1")) ")" )))) ; theorem :: ANALORT:17 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (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 "x")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r1_analoaf :::"//"::: ) (Set (Var "u1")) "," (Set (Var "v1")))) "holds" (Bool (Set ($#k1_analort :::"Ortm"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) ")" ) "," (Set ($#k1_analort :::"Ortm"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "v")) ")" ) ($#r1_analoaf :::"//"::: ) (Set ($#k1_analort :::"Ortm"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u1")) ")" ) "," (Set ($#k1_analort :::"Ortm"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "v1")) ")" )))) ; theorem :: ANALORT:18 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "v")) "," (Set (Var "v1")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "v")) "," (Set (Var "v1")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y")))) "holds" (Bool (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "u1")) "," (Set (Var "u")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))))) ; theorem :: ANALORT:19 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "v")) "," (Set (Var "v1")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "v")) "," (Set (Var "v1")) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y")))) "holds" (Bool (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "u")) "," (Set (Var "u1")) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))))) ; theorem :: ANALORT:20 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Var "u")) "," (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))))) ; theorem :: ANALORT:21 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Var "u")) "," (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))))) ; theorem :: ANALORT:22 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "w")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))))) ; theorem :: ANALORT:23 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "w")) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))))) ; theorem :: ANALORT:24 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (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 "x")) "," (Set (Var "y")))) "holds" (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set ($#k2_analort :::"Orte"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) ")" ) "," (Set ($#k2_analort :::"Orte"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "v")) ")" ) ($#r3_analmetr :::"are_Ort_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))))) ; theorem :: ANALORT:25 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set ($#k2_analort :::"Orte"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) ")" ) "," (Set ($#k2_analort :::"Orte"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "v")) ")" ) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))))) ; theorem :: ANALORT:26 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set ($#k1_analort :::"Ortm"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) ")" ) "," (Set ($#k1_analort :::"Ortm"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "v")) ")" ) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))))) ; theorem :: ANALORT:27 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (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 "x")) "," (Set (Var "y")))) "holds" (Bool "(" (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r1_analoaf :::"//"::: ) (Set (Var "u1")) "," (Set (Var "v1"))) "iff" (Bool "ex" (Set (Var "u2")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "u2")) ($#r1_hidden :::"<>"::: ) (Set (Var "v2"))) & (Bool (Set (Var "u2")) "," (Set (Var "v2")) "," (Set (Var "u")) "," (Set (Var "v")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "u2")) "," (Set (Var "v2")) "," (Set (Var "u1")) "," (Set (Var "v1")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) ")" )) ")" ))) ; theorem :: ANALORT:28 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (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 "x")) "," (Set (Var "y")))) "holds" (Bool "(" (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r1_analoaf :::"//"::: ) (Set (Var "u1")) "," (Set (Var "v1"))) "iff" (Bool "ex" (Set (Var "u2")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "u2")) ($#r1_hidden :::"<>"::: ) (Set (Var "v2"))) & (Bool (Set (Var "u2")) "," (Set (Var "v2")) "," (Set (Var "u")) "," (Set (Var "v")) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "u2")) "," (Set (Var "v2")) "," (Set (Var "u1")) "," (Set (Var "v1")) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) ")" )) ")" ))) ; theorem :: ANALORT:29 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (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 "x")) "," (Set (Var "y")))) "holds" (Bool "(" (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "v1")) ($#r3_analmetr :::"are_Ort_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) "iff" (Bool "(" (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "v1")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) "or" (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "u1")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) ")" ) ")" ))) ; theorem :: ANALORT:30 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (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 "x")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "v1")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "u1")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Bool "not" (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Var "v"))))) "holds" (Bool (Set (Var "u1")) ($#r1_hidden :::"="::: ) (Set (Var "v1"))))) ; theorem :: ANALORT:31 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (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 "x")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "v1")) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "u1")) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Bool "not" (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Var "v"))))) "holds" (Bool (Set (Var "u1")) ($#r1_hidden :::"="::: ) (Set (Var "v1"))))) ; theorem :: ANALORT:32 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "v1")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "v1")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "w")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Bool "not" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "w")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))))) "holds" (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "v1")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))))) ; theorem :: ANALORT:33 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "v1")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "v1")) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "w")) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Bool "not" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "w")) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))))) "holds" (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "v1")) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))))) ; theorem :: ANALORT:34 (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 "x")) "," (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")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y")))) "holds" (Bool (Set (Var "v")) "," (Set (Var "u")) "," (Set (Var "v1")) "," (Set (Var "u1")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))))) ; theorem :: ANALORT:35 (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 "x")) "," (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_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y")))) "holds" (Bool (Set (Var "v")) "," (Set (Var "u")) "," (Set (Var "v1")) "," (Set (Var "u1")) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))))) ; theorem :: ANALORT:36 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "v1")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "v1")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "w")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y")))) "holds" (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "w")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))))) ; theorem :: ANALORT:37 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "v1")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "v1")) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "w")) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y")))) "holds" (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "w")) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))))) ; theorem :: ANALORT:38 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "x")) "," (Set (Var "y")))) "holds" (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "ex" (Set (Var "u1")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "w")) ($#r1_hidden :::"<>"::: ) (Set (Var "u1"))) & (Bool (Set (Var "w")) "," (Set (Var "u1")) "," (Set (Var "u")) "," (Set (Var "v")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) ")" ))))) ; theorem :: ANALORT:39 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "x")) "," (Set (Var "y")))) "holds" (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "ex" (Set (Var "u1")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "w")) ($#r1_hidden :::"<>"::: ) (Set (Var "u1"))) & (Bool (Set (Var "w")) "," (Set (Var "u1")) "," (Set (Var "u")) "," (Set (Var "v")) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) ")" ))))) ; theorem :: ANALORT:40 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "x")) "," (Set (Var "y")))) "holds" (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "ex" (Set (Var "u1")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "w")) ($#r1_hidden :::"<>"::: ) (Set (Var "u1"))) & (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "u1")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) ")" ))))) ; theorem :: ANALORT:41 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "x")) "," (Set (Var "y")))) "holds" (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "ex" (Set (Var "u1")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "w")) ($#r1_hidden :::"<>"::: ) (Set (Var "u1"))) & (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "u1")) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) ")" ))))) ; theorem :: ANALORT:42 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "w")) "," (Set (Var "w1")) "," (Set (Var "u2")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "v")) "," (Set (Var "v1")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "w")) "," (Set (Var "w1")) "," (Set (Var "v")) "," (Set (Var "v1")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "w")) "," (Set (Var "w1")) "," (Set (Var "u2")) "," (Set (Var "v2")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Bool "not" (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set (Var "w1")))) & (Bool (Bool "not" (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "v1"))))) "holds" (Bool (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "u2")) "," (Set (Var "v2")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))))) ; theorem :: ANALORT:43 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "w")) "," (Set (Var "w1")) "," (Set (Var "u2")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "v")) "," (Set (Var "v1")) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "w")) "," (Set (Var "w1")) "," (Set (Var "v")) "," (Set (Var "v1")) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "w")) "," (Set (Var "w1")) "," (Set (Var "u2")) "," (Set (Var "v2")) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Bool "not" (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set (Var "w1")))) & (Bool (Bool "not" (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "v1"))))) "holds" (Bool (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "u2")) "," (Set (Var "v2")) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))))) ; theorem :: ANALORT:44 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "w")) "," (Set (Var "w1")) "," (Set (Var "u2")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "v")) "," (Set (Var "v1")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "w")) "," (Set (Var "w1")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "u2")) "," (Set (Var "v2")) "," (Set (Var "w")) "," (Set (Var "w1")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Bool "not" (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "u2")) "," (Set (Var "v2")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y")))) & (Bool (Bool "not" (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "v1"))))) "holds" (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set (Var "w1"))))) ; theorem :: ANALORT:45 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "w")) "," (Set (Var "w1")) "," (Set (Var "u2")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "v")) "," (Set (Var "v1")) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "w")) "," (Set (Var "w1")) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "u2")) "," (Set (Var "v2")) "," (Set (Var "w")) "," (Set (Var "w1")) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Bool "not" (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "u2")) "," (Set (Var "v2")) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y")))) & (Bool (Bool "not" (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "v1"))))) "holds" (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set (Var "w1"))))) ; theorem :: ANALORT:46 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "w")) "," (Set (Var "w1")) "," (Set (Var "u2")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "v")) "," (Set (Var "v1")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "w")) "," (Set (Var "w1")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "u2")) "," (Set (Var "v2")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Bool "not" (Set (Var "u2")) "," (Set (Var "v2")) "," (Set (Var "w")) "," (Set (Var "w1")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y")))) & (Bool (Bool "not" (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "v1"))))) "holds" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Var "u1"))))) ; theorem :: ANALORT:47 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "w")) "," (Set (Var "w1")) "," (Set (Var "u2")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "v")) "," (Set (Var "v1")) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "w")) "," (Set (Var "w1")) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "u2")) "," (Set (Var "v2")) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Bool "not" (Set (Var "u2")) "," (Set (Var "v2")) "," (Set (Var "w")) "," (Set (Var "w1")) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y")))) & (Bool (Bool "not" (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "v1"))))) "holds" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Var "u1"))))) ; theorem :: ANALORT:48 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "x")) "," (Set (Var "y")))) "holds" (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "u1")) "," (Set (Var "v1")) "," (Set (Var "w1")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Bool "not" (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "w")) "," (Set (Var "u1")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y")))) & (Bool (Bool "not" (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "u1")) "," (Set (Var "w")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y")))) & (Bool (Set (Var "u1")) "," (Set (Var "w1")) "," (Set (Var "u1")) "," (Set (Var "w")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y")))) "holds" (Bool "ex" (Set (Var "u2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool "(" (Bool (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "v")) "," (Set (Var "u2")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) "or" (Bool (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "u2")) "," (Set (Var "v")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) ")" ) & (Bool "(" (Bool (Set (Var "u1")) "," (Set (Var "w1")) "," (Set (Var "u1")) "," (Set (Var "u2")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) "or" (Bool (Set (Var "u1")) "," (Set (Var "w1")) "," (Set (Var "u2")) "," (Set (Var "u1")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) ")" ) ")" ))))) ; theorem :: ANALORT:49 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "x")) "," (Set (Var "y")))) "holds" (Bool "ex" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u")) "," (Set (Var "w")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool "(" "for" (Set (Var "v1")) "," (Set (Var "w1")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool "(" "not" (Bool (Set (Var "v1")) "," (Set (Var "w1")) "," (Set (Var "u")) "," (Set (Var "v")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) "or" (Bool "(" (Bool (Bool "not" (Set (Var "v1")) "," (Set (Var "w1")) "," (Set (Var "u")) "," (Set (Var "w")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y")))) & (Bool (Bool "not" (Set (Var "v1")) "," (Set (Var "w1")) "," (Set (Var "w")) "," (Set (Var "u")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y")))) ")" ) "or" (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Var "w1"))) ")" ) ")" ) ")" )))) ; theorem :: ANALORT:50 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "x")) "," (Set (Var "y")))) "holds" (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "u1")) "," (Set (Var "v1")) "," (Set (Var "w1")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Bool "not" (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "w")) "," (Set (Var "u1")) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y")))) & (Bool (Bool "not" (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "u1")) "," (Set (Var "w")) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y")))) & (Bool (Set (Var "u1")) "," (Set (Var "w1")) "," (Set (Var "u1")) "," (Set (Var "w")) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y")))) "holds" (Bool "ex" (Set (Var "u2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool "(" (Bool (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "v")) "," (Set (Var "u2")) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) "or" (Bool (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "u2")) "," (Set (Var "v")) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) ")" ) & (Bool "(" (Bool (Set (Var "u1")) "," (Set (Var "w1")) "," (Set (Var "u1")) "," (Set (Var "u2")) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) "or" (Bool (Set (Var "u1")) "," (Set (Var "w1")) "," (Set (Var "u2")) "," (Set (Var "u1")) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) ")" ) ")" ))))) ; theorem :: ANALORT:51 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "x")) "," (Set (Var "y")))) "holds" (Bool "ex" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u")) "," (Set (Var "w")) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool "(" "for" (Set (Var "v1")) "," (Set (Var "w1")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool "(" "not" (Bool (Set (Var "v1")) "," (Set (Var "w1")) "," (Set (Var "u")) "," (Set (Var "v")) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) "or" (Bool "(" (Bool (Bool "not" (Set (Var "v1")) "," (Set (Var "w1")) "," (Set (Var "u")) "," (Set (Var "w")) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y")))) & (Bool (Bool "not" (Set (Var "v1")) "," (Set (Var "w1")) "," (Set (Var "w")) "," (Set (Var "u")) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y")))) ")" ) "or" (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Var "w1"))) ")" ) ")" ) ")" )))) ; definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "x", "y" be ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Const "V")); func :::"CORTE"::: "(" "V" "," "x" "," "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 :: ANALORT:def 5 (Bool "for" (Set (Var "uu")) "," (Set (Var "vv")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "uu")) "," (Set (Var "vv")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "u1")) "," (Set (Var "u2")) "," (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" "V" "st" (Bool "(" (Bool (Set (Var "uu")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "u1")) "," (Set (Var "u2")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "vv")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "v1")) "," (Set (Var "v2")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "u1")) "," (Set (Var "u2")) "," (Set (Var "v1")) "," (Set (Var "v2")) ($#r1_analort :::"are_COrte_wrt"::: ) "x" "," "y") ")" )) ")" )); end; :: deftheorem defines :::"CORTE"::: ANALORT:def 5 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (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 ($#k3_analort :::"CORTE"::: ) "(" (Set (Var "V")) "," (Set (Var "x")) "," (Set (Var "y")) ")" )) "iff" (Bool "for" (Set (Var "uu")) "," (Set (Var "vv")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "uu")) "," (Set (Var "vv")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) "iff" (Bool "ex" (Set (Var "u1")) "," (Set (Var "u2")) "," (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "uu")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "u1")) "," (Set (Var "u2")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "vv")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "v1")) "," (Set (Var "v2")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "u1")) "," (Set (Var "u2")) "," (Set (Var "v1")) "," (Set (Var "v2")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) ")" )) ")" )) ")" )))); definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "x", "y" be ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Const "V")); func :::"CORTM"::: "(" "V" "," "x" "," "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 :: ANALORT:def 6 (Bool "for" (Set (Var "uu")) "," (Set (Var "vv")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "uu")) "," (Set (Var "vv")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "u1")) "," (Set (Var "u2")) "," (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" "V" "st" (Bool "(" (Bool (Set (Var "uu")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "u1")) "," (Set (Var "u2")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "vv")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "v1")) "," (Set (Var "v2")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "u1")) "," (Set (Var "u2")) "," (Set (Var "v1")) "," (Set (Var "v2")) ($#r2_analort :::"are_COrtm_wrt"::: ) "x" "," "y") ")" )) ")" )); end; :: deftheorem defines :::"CORTM"::: ANALORT:def 6 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (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 ($#k4_analort :::"CORTM"::: ) "(" (Set (Var "V")) "," (Set (Var "x")) "," (Set (Var "y")) ")" )) "iff" (Bool "for" (Set (Var "uu")) "," (Set (Var "vv")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "uu")) "," (Set (Var "vv")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) "iff" (Bool "ex" (Set (Var "u1")) "," (Set (Var "u2")) "," (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "uu")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "u1")) "," (Set (Var "u2")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "vv")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "v1")) "," (Set (Var "v2")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "u1")) "," (Set (Var "u2")) "," (Set (Var "v1")) "," (Set (Var "v2")) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) ")" )) ")" )) ")" )))); definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "x", "y" be ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Const "V")); func :::"CESpace"::: "(" "V" "," "x" "," "y" ")" -> ($#v1_analoaf :::"strict"::: ) ($#l1_analoaf :::"AffinStruct"::: ) equals :: ANALORT:def 7 (Set ($#g1_analoaf :::"AffinStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "(" ($#k3_analort :::"CORTE"::: ) "(" "V" "," "x" "," "y" ")" ")" ) "#)" ); end; :: deftheorem defines :::"CESpace"::: ANALORT:def 7 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k5_analort :::"CESpace"::: ) "(" (Set (Var "V")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#g1_analoaf :::"AffinStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set "(" ($#k3_analort :::"CORTE"::: ) "(" (Set (Var "V")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) "#)" )))); registrationlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "x", "y" be ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Const "V")); cluster (Set ($#k5_analort :::"CESpace"::: ) "(" "V" "," "x" "," "y" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_analoaf :::"strict"::: ) ; end; definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "x", "y" be ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Const "V")); func :::"CMSpace"::: "(" "V" "," "x" "," "y" ")" -> ($#v1_analoaf :::"strict"::: ) ($#l1_analoaf :::"AffinStruct"::: ) equals :: ANALORT:def 8 (Set ($#g1_analoaf :::"AffinStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "(" ($#k4_analort :::"CORTM"::: ) "(" "V" "," "x" "," "y" ")" ")" ) "#)" ); end; :: deftheorem defines :::"CMSpace"::: ANALORT:def 8 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k6_analort :::"CMSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#g1_analoaf :::"AffinStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set "(" ($#k4_analort :::"CORTM"::: ) "(" (Set (Var "V")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) "#)" )))); registrationlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "x", "y" be ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Const "V")); cluster (Set ($#k6_analort :::"CMSpace"::: ) "(" "V" "," "x" "," "y" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_analoaf :::"strict"::: ) ; end; theorem :: ANALORT:52 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "uu")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "uu")) "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_analort :::"CESpace"::: ) "(" (Set (Var "V")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" )) "iff" (Bool (Set (Var "uu")) "is" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V"))) ")" )))) ; theorem :: ANALORT:53 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "uu")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "uu")) "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k6_analort :::"CMSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" )) "iff" (Bool (Set (Var "uu")) "is" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V"))) ")" )))) ; theorem :: ANALORT:54 (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 "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_analort :::"CESpace"::: ) "(" (Set (Var "V")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) "st" (Bool (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Var "u1")) ($#r1_hidden :::"="::: ) (Set (Var "r"))) & (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Var "s")))) "holds" (Bool "(" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "r")) "," (Set (Var "s"))) "iff" (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "v1")) ($#r1_analort :::"are_COrte_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) ")" )))) ; theorem :: ANALORT:55 (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 "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k6_analort :::"CMSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) "st" (Bool (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Var "u1")) ($#r1_hidden :::"="::: ) (Set (Var "r"))) & (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Var "s")))) "holds" (Bool "(" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "r")) "," (Set (Var "s"))) "iff" (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "v1")) ($#r2_analort :::"are_COrtm_wrt"::: ) (Set (Var "x")) "," (Set (Var "y"))) ")" )))) ;