:: ANALMETR semantic presentation begin definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "w", "y" be ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Const "V")); pred :::"Gen"::: "w" "," "y" means :: ANALMETR:def 1 (Bool "(" (Bool "(" "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" "V" (Bool "ex" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a1")) ($#k1_rlvect_1 :::"*"::: ) "w" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a2")) ($#k1_rlvect_1 :::"*"::: ) "y" ")" )))) ")" ) & (Bool "(" "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set "(" (Set (Var "a1")) ($#k1_rlvect_1 :::"*"::: ) "w" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a2")) ($#k1_rlvect_1 :::"*"::: ) "y" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "V"))) "holds" (Bool "(" (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ) ")" ); end; :: deftheorem defines :::"Gen"::: ANALMETR:def 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")) "holds" (Bool "(" (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "w")) "," (Set (Var "y"))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "ex" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a1")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a2")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "y")) ")" )))) ")" ) & (Bool "(" "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set "(" (Set (Var "a1")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a2")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))))) "holds" (Bool "(" (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ) ")" ) ")" ))); definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "u", "v", "w", "y" be ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Const "V")); pred "u" "," "v" :::"are_Ort_wrt"::: "w" "," "y" means :: ANALMETR:def 2 (Bool "ex" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool "u" ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a1")) ($#k1_rlvect_1 :::"*"::: ) "w" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a2")) ($#k1_rlvect_1 :::"*"::: ) "y" ")" ))) & (Bool "v" ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b1")) ($#k1_rlvect_1 :::"*"::: ) "w" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b2")) ($#k1_rlvect_1 :::"*"::: ) "y" ")" ))) & (Bool (Set (Set "(" (Set (Var "a1")) ($#k8_real_1 :::"*"::: ) (Set (Var "b1")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "a2")) ($#k8_real_1 :::"*"::: ) (Set (Var "b2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )); end; :: deftheorem defines :::"are_Ort_wrt"::: ANALMETR:def 2 : (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")) "holds" (Bool "(" (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analmetr :::"are_Ort_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) "iff" (Bool "ex" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a1")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a2")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "y")) ")" ))) & (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b1")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b2")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "y")) ")" ))) & (Bool (Set (Set "(" (Set (Var "a1")) ($#k8_real_1 :::"*"::: ) (Set (Var "b1")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "a2")) ($#k8_real_1 :::"*"::: ) (Set (Var "b2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ")" ))); theorem :: ANALMETR:1 (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 ($#r1_analmetr :::"Gen"::: ) (Set (Var "w")) "," (Set (Var "y")))) "holds" (Bool "(" (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analmetr :::"are_Ort_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) "iff" (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a1")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a2")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "y")) ")" ))) & (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b1")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b2")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "y")) ")" )))) "holds" (Bool (Set (Set "(" (Set (Var "a1")) ($#k8_real_1 :::"*"::: ) (Set (Var "b1")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "a2")) ($#k8_real_1 :::"*"::: ) (Set (Var "b2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ")" ))) ; theorem :: ANALMETR:2 (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 (Var "w")) "," (Set (Var "y")) ($#r2_analmetr :::"are_Ort_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))))) ; theorem :: ANALMETR:3 (Bool "ex" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::)(Bool "ex" (Set (Var "w")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "w")) "," (Set (Var "y"))))) ; theorem :: ANALMETR:4 (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")) ($#r2_analmetr :::"are_Ort_wrt"::: ) (Set (Var "w")) "," (Set (Var "y")))) "holds" (Bool (Set (Var "v")) "," (Set (Var "u")) ($#r2_analmetr :::"are_Ort_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))))) ; theorem :: ANALMETR:5 (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 ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))) ($#r2_analmetr :::"are_Ort_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))) "," (Set (Var "v")) ($#r2_analmetr :::"are_Ort_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) ")" )))) ; theorem :: ANALMETR:6 (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")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analmetr :::"are_Ort_wrt"::: ) (Set (Var "w")) "," (Set (Var "y")))) "holds" (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u"))) "," (Set (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v"))) ($#r2_analmetr :::"are_Ort_wrt"::: ) (Set (Var "w")) "," (Set (Var "y")))))) ; theorem :: ANALMETR:7 (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")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analmetr :::"are_Ort_wrt"::: ) (Set (Var "w")) "," (Set (Var "y")))) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u"))) "," (Set (Var "v")) ($#r2_analmetr :::"are_Ort_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v"))) ($#r2_analmetr :::"are_Ort_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) ")" )))) ; theorem :: ANALMETR:8 (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")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analmetr :::"are_Ort_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) ")" ))))) ; theorem :: ANALMETR:9 (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")) ($#r2_analmetr :::"are_Ort_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "v")) "," (Set (Var "u2")) ($#r2_analmetr :::"are_Ort_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))))) "holds" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u2")))) & (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" )))) ; theorem :: ANALMETR:10 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "u")) "," (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 "v1")) ($#r2_analmetr :::"are_Ort_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "v2")) ($#r2_analmetr :::"are_Ort_wrt"::: ) (Set (Var "w")) "," (Set (Var "y")))) "holds" (Bool "(" (Bool (Set (Var "u")) "," (Set (Set (Var "v1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "v2"))) ($#r2_analmetr :::"are_Ort_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Set (Var "v1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "v2"))) ($#r2_analmetr :::"are_Ort_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) ")" ))) ; theorem :: ANALMETR:11 (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"))) & (Bool (Set (Var "u")) "," (Set (Var "u")) ($#r2_analmetr :::"are_Ort_wrt"::: ) (Set (Var "w")) "," (Set (Var "y")))) "holds" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))))) ; theorem :: ANALMETR:12 (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")) "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 (Set (Var "u1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "u2"))) ($#r2_analmetr :::"are_Ort_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "u1")) "," (Set (Set (Var "u2")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "u"))) ($#r2_analmetr :::"are_Ort_wrt"::: ) (Set (Var "w")) "," (Set (Var "y")))) "holds" (Bool (Set (Var "u2")) "," (Set (Set (Var "u")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "u1"))) ($#r2_analmetr :::"are_Ort_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))))) ; theorem :: ANALMETR:13 (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"))) & (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))))) "holds" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" )) "," (Set (Var "u")) ($#r2_analmetr :::"are_Ort_wrt"::: ) (Set (Var "w")) "," (Set (Var "y")))))) ; theorem :: ANALMETR: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")) "holds" (Bool "(" (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"))) ")" ) "iff" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "u")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "v1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "u1")) ")" ))) & (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" )) ")" ))) ; theorem :: ANALMETR:15 (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 ($#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 ($#k1_diraf :::"lambda"::: ) (Set "(" ($#k1_analoaf :::"DirPar"::: ) (Set (Var "V")) ")" ))) "iff" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "u")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "v1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "u1")) ")" ))) & (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" )) ")" ))) ; definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "u", "u1", "v", "v1", "w", "y" be ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Const "V")); pred "u" "," "u1" "," "v" "," "v1" :::"are_Ort_wrt"::: "w" "," "y" means :: ANALMETR:def 3 (Bool (Set "u1" ($#k5_algstr_0 :::"-"::: ) "u") "," (Set "v1" ($#k5_algstr_0 :::"-"::: ) "v") ($#r2_analmetr :::"are_Ort_wrt"::: ) "w" "," "y"); end; :: deftheorem defines :::"are_Ort_wrt"::: ANALMETR:def 3 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "w")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "v")) "," (Set (Var "v1")) ($#r3_analmetr :::"are_Ort_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) "iff" (Bool (Set (Set (Var "u1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "u"))) "," (Set (Set (Var "v1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "v"))) ($#r2_analmetr :::"are_Ort_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 :::"Orthogonality"::: "(" "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 :: ANALMETR:def 4 (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")) ($#r3_analmetr :::"are_Ort_wrt"::: ) "w" "," "y") ")" )) ")" )); end; :: deftheorem defines :::"Orthogonality"::: ANALMETR:def 4 : (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 ($#k1_analmetr :::"Orthogonality"::: ) "(" (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")) ($#r3_analmetr :::"are_Ort_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) ")" )) ")" )) ")" )))); theorem :: ANALMETR:16 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k2_diraf :::"Lambda"::: ) (Set "(" ($#k2_analoaf :::"OASpace"::: ) (Set (Var "V")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))))) ; theorem :: ANALMETR:17 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) "holds" (Bool (Set "the" ($#u1_analoaf :::"CONGR"::: ) "of" (Set "(" ($#k2_diraf :::"Lambda"::: ) (Set "(" ($#k2_analoaf :::"OASpace"::: ) (Set (Var "V")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_diraf :::"lambda"::: ) (Set "(" ($#k1_analoaf :::"DirPar"::: ) (Set (Var "V")) ")" )))) ; theorem :: ANALMETR:18 (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_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 "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "u")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "v1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "u1")) ")" ))) & (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" )) ")" )))) ; definitionattr "c1" is :::"strict"::: ; struct :::"ParOrtStr"::: -> ($#l1_analoaf :::"AffinStruct"::: ) ; aggr :::"ParOrtStr":::(# :::"carrier":::, :::"CONGR":::, :::"orthogonality"::: #) -> ($#l1_analmetr :::"ParOrtStr"::: ) ; sel :::"orthogonality"::: "c1" -> ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1") ($#k2_zfmisc_1 :::":]"::: ) ); end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) for ($#l1_analmetr :::"ParOrtStr"::: ) ; end; definitionlet "POS" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analmetr :::"ParOrtStr"::: ) ; let "a", "b", "c", "d" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "POS")); pred "a" "," "b" :::"_|_"::: "c" "," "d" means :: ANALMETR:def 5 (Bool (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) "a" "," "b" ($#k1_domain_1 :::"]"::: ) ) "," (Set ($#k1_domain_1 :::"["::: ) "c" "," "d" ($#k1_domain_1 :::"]"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_analmetr :::"orthogonality"::: ) "of" "POS")); end; :: deftheorem defines :::"_|_"::: ANALMETR:def 5 : (Bool "for" (Set (Var "POS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analmetr :::"ParOrtStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "c")) "," (Set (Var "d"))) "iff" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_domain_1 :::"]"::: ) ) "," (Set ($#k1_domain_1 :::"["::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k1_domain_1 :::"]"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_analmetr :::"orthogonality"::: ) "of" (Set (Var "POS")))) ")" ))); definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "w", "y" be ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Const "V")); func :::"AMSpace"::: "(" "V" "," "w" "," "y" ")" -> ($#v1_analmetr :::"strict"::: ) ($#l1_analmetr :::"ParOrtStr"::: ) equals :: ANALMETR:def 6 (Set ($#g1_analmetr :::"ParOrtStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "(" ($#k1_diraf :::"lambda"::: ) (Set "(" ($#k1_analoaf :::"DirPar"::: ) "V" ")" ) ")" ) "," (Set "(" ($#k1_analmetr :::"Orthogonality"::: ) "(" "V" "," "w" "," "y" ")" ")" ) "#)" ); end; :: deftheorem defines :::"AMSpace"::: ANALMETR:def 6 : (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 ($#k2_analmetr :::"AMSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "w")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#g1_analmetr :::"ParOrtStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set "(" ($#k1_diraf :::"lambda"::: ) (Set "(" ($#k1_analoaf :::"DirPar"::: ) (Set (Var "V")) ")" ) ")" ) "," (Set "(" ($#k1_analmetr :::"Orthogonality"::: ) "(" (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 ($#k2_analmetr :::"AMSpace"::: ) "(" "V" "," "w" "," "y" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_analmetr :::"strict"::: ) ; end; theorem :: ANALMETR:19 (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 "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k2_analmetr :::"AMSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "w")) "," (Set (Var "y")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V")))) & (Bool (Set "the" ($#u1_analoaf :::"CONGR"::: ) "of" (Set "(" ($#k2_analmetr :::"AMSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "w")) "," (Set (Var "y")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_diraf :::"lambda"::: ) (Set "(" ($#k1_analoaf :::"DirPar"::: ) (Set (Var "V")) ")" ))) & (Bool (Set "the" ($#u1_analmetr :::"orthogonality"::: ) "of" (Set "(" ($#k2_analmetr :::"AMSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "w")) "," (Set (Var "y")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_analmetr :::"Orthogonality"::: ) "(" (Set (Var "V")) "," (Set (Var "w")) "," (Set (Var "y")) ")" )) ")" ))) ; definitionlet "POS" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analmetr :::"ParOrtStr"::: ) ; func :::"Af"::: "POS" -> ($#v1_analoaf :::"strict"::: ) ($#l1_analoaf :::"AffinStruct"::: ) equals :: ANALMETR:def 7 (Set ($#g1_analoaf :::"AffinStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "POS") "," (Set "the" ($#u1_analoaf :::"CONGR"::: ) "of" "POS") "#)" ); end; :: deftheorem defines :::"Af"::: ANALMETR:def 7 : (Bool "for" (Set (Var "POS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analmetr :::"ParOrtStr"::: ) "holds" (Bool (Set ($#k3_analmetr :::"Af"::: ) (Set (Var "POS"))) ($#r1_hidden :::"="::: ) (Set ($#g1_analoaf :::"AffinStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "POS"))) "," (Set "the" ($#u1_analoaf :::"CONGR"::: ) "of" (Set (Var "POS"))) "#)" ))); registrationlet "POS" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analmetr :::"ParOrtStr"::: ) ; cluster (Set ($#k3_analmetr :::"Af"::: ) "POS") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_analoaf :::"strict"::: ) ; end; theorem :: ANALMETR:20 (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 ($#k3_analmetr :::"Af"::: ) (Set "(" ($#k2_analmetr :::"AMSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "w")) "," (Set (Var "y")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_diraf :::"Lambda"::: ) (Set "(" ($#k2_analoaf :::"OASpace"::: ) (Set (Var "V")) ")" ))))) ; theorem :: ANALMETR:21 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "w")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "p")) "," (Set (Var "p1")) "," (Set (Var "q")) "," (Set (Var "q1")) "being" ($#m1_subset_1 :::"Element":::) "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 "p1")) ($#r1_hidden :::"="::: ) (Set (Var "u1"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "v"))) & (Bool (Set (Var "q1")) ($#r1_hidden :::"="::: ) (Set (Var "v1")))) "holds" (Bool "(" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "p1")) "," (Set (Var "q1"))) "iff" (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "v1")) ($#r3_analmetr :::"are_Ort_wrt"::: ) (Set (Var "w")) "," (Set (Var "y"))) ")" )))) ; theorem :: ANALMETR:22 (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 "(" ($#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 "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "u")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "v1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "u1")) ")" ))) & (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" )) ")" )))) ; theorem :: ANALMETR:23 (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 "p")) "," (Set (Var "q")) "," (Set (Var "p1")) "," (Set (Var "q1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_analmetr :::"AMSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "w")) "," (Set (Var "y")) ")" ")" ) "st" (Bool (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "p1")) "," (Set (Var "q1")))) "holds" (Bool (Set (Var "p1")) "," (Set (Var "q1")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "p")) "," (Set (Var "q")))))) ; theorem :: ANALMETR:24 (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 "p")) "," (Set (Var "q")) "," (Set (Var "p1")) "," (Set (Var "q1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_analmetr :::"AMSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "w")) "," (Set (Var "y")) ")" ")" ) "st" (Bool (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "p1")) "," (Set (Var "q1")))) "holds" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "q1")) "," (Set (Var "p1")))))) ; theorem :: ANALMETR:25 (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 "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_analmetr :::"AMSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "w")) "," (Set (Var "y")) ")" ")" ) "holds" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "r")) "," (Set (Var "r")))))) ; theorem :: ANALMETR:26 (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 "p")) "," (Set (Var "p1")) "," (Set (Var "q")) "," (Set (Var "q1")) "," (Set (Var "r")) "," (Set (Var "r1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_analmetr :::"AMSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "w")) "," (Set (Var "y")) ")" ")" ) "st" (Bool (Bool (Set (Var "p")) "," (Set (Var "p1")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "q")) "," (Set (Var "q1"))) & (Bool (Set (Var "p")) "," (Set (Var "p1")) ($#r2_analoaf :::"//"::: ) (Set (Var "r")) "," (Set (Var "r1"))) & (Bool (Bool "not" (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "p1"))))) "holds" (Bool (Set (Var "q")) "," (Set (Var "q1")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "r")) "," (Set (Var "r1")))))) ; theorem :: ANALMETR:27 (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 "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_analmetr :::"AMSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "w")) "," (Set (Var "y")) ")" ")" ) (Bool "ex" (Set (Var "r1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_analmetr :::"AMSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "w")) "," (Set (Var "y")) ")" ")" ) "st" (Bool "(" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "r")) "," (Set (Var "r1"))) & (Bool (Set (Var "r")) ($#r1_hidden :::"<>"::: ) (Set (Var "r1"))) ")" ))))) ; theorem :: ANALMETR:28 (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 "p")) "," (Set (Var "p1")) "," (Set (Var "q")) "," (Set (Var "q1")) "," (Set (Var "r")) "," (Set (Var "r1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_analmetr :::"AMSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "w")) "," (Set (Var "y")) ")" ")" ) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "p")) "," (Set (Var "p1")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "q")) "," (Set (Var "q1"))) & (Bool (Set (Var "p")) "," (Set (Var "p1")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "r")) "," (Set (Var "r1"))) & (Bool (Bool "not" (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "p1"))))) "holds" (Bool (Set (Var "q")) "," (Set (Var "q1")) ($#r2_analoaf :::"//"::: ) (Set (Var "r")) "," (Set (Var "r1")))))) ; theorem :: ANALMETR:29 (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 "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_analmetr :::"AMSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "w")) "," (Set (Var "y")) ")" ")" ) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "r")) "," (Set (Var "r1"))) & (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "r")) "," (Set (Var "r2")))) "holds" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "r1")) "," (Set (Var "r2")))))) ; theorem :: ANALMETR: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")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_analmetr :::"AMSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "w")) "," (Set (Var "y")) ")" ")" ) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "p")) "," (Set (Var "q")))) "holds" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "q")))))) ; theorem :: ANALMETR: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")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_analmetr :::"AMSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "w")) "," (Set (Var "y")) ")" ")" ) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "p1")) "," (Set (Var "q")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "p2")) "," (Set (Var "p")))) "holds" (Bool (Set (Var "p2")) "," (Set (Var "q")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "p")) "," (Set (Var "p1")))))) ; theorem :: ANALMETR: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")) (Bool "for" (Set (Var "p")) "," (Set (Var "p1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_analmetr :::"AMSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "w")) "," (Set (Var "y")) ")" ")" ) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "p1")))) "holds" (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_analmetr :::"AMSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "w")) "," (Set (Var "y")) ")" ")" ) (Bool "ex" (Set (Var "q1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_analmetr :::"AMSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "w")) "," (Set (Var "y")) ")" ")" ) "st" (Bool "(" (Bool (Set (Var "p")) "," (Set (Var "p1")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "q1"))) & (Bool (Set (Var "p")) "," (Set (Var "p1")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "q1")) "," (Set (Var "q"))) ")" )))))) ; definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analmetr :::"ParOrtStr"::: ) ; attr "IT" is :::"OrtAfSp-like"::: means :: ANALMETR:def 8 (Bool "(" (Bool (Set ($#g1_analoaf :::"AffinStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "IT") "," (Set "the" ($#u1_analoaf :::"CONGR"::: ) "of" "IT") "#)" ) "is" ($#l1_analoaf :::"AffinSpace":::)) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool "(" "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "a")) "," (Set (Var "b")))) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "c")) "," (Set (Var "c"))) & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "c")) "," (Set (Var "d")))) "implies" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "d")) "," (Set (Var "c"))) & (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "a")) "," (Set (Var "b"))) ")" ) ")" & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "r")) "," (Set (Var "s"))) & (Bool (Bool "not" (Set (Var "p")) "," (Set (Var "q")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "r")) "," (Set (Var "s"))))) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "p")) "," (Set (Var "s")))) "implies" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "q")) "," (Set (Var "s"))) ")" ")" ) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "x"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "x")) "," (Set (Var "c"))) ")" )) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "c")) "," (Set (Var "x"))) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "x"))) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"OrtAfSp-like"::: ANALMETR:def 8 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analmetr :::"ParOrtStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_analmetr :::"OrtAfSp-like"::: ) ) "iff" (Bool "(" (Bool (Set ($#g1_analoaf :::"AffinStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "IT"))) "," (Set "the" ($#u1_analoaf :::"CONGR"::: ) "of" (Set (Var "IT"))) "#)" ) "is" ($#l1_analoaf :::"AffinSpace":::)) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "a")) "," (Set (Var "b")))) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "c")) "," (Set (Var "c"))) & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "c")) "," (Set (Var "d")))) "implies" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "d")) "," (Set (Var "c"))) & (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "a")) "," (Set (Var "b"))) ")" ) ")" & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "r")) "," (Set (Var "s"))) & (Bool (Bool "not" (Set (Var "p")) "," (Set (Var "q")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "r")) "," (Set (Var "s"))))) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "p")) "," (Set (Var "s")))) "implies" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "q")) "," (Set (Var "s"))) ")" ")" ) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "x"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "x")) "," (Set (Var "c"))) ")" )) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "c")) "," (Set (Var "x"))) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "x"))) ")" )) ")" ) ")" ) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_analmetr :::"strict"::: ) ($#v2_analmetr :::"OrtAfSp-like"::: ) for ($#l1_analmetr :::"ParOrtStr"::: ) ; end; definitionmode OrtAfSp is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_analmetr :::"OrtAfSp-like"::: ) ($#l1_analmetr :::"ParOrtStr"::: ) ; end; theorem :: ANALMETR: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 (Set ($#k2_analmetr :::"AMSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "w")) "," (Set (Var "y")) ")" ) "is" ($#l1_analmetr :::"OrtAfSp":::)))) ; definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analmetr :::"ParOrtStr"::: ) ; attr "IT" is :::"OrtAfPl-like"::: means :: ANALMETR:def 9 (Bool "(" (Bool (Set ($#g1_analoaf :::"AffinStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "IT") "," (Set "the" ($#u1_analoaf :::"CONGR"::: ) "of" "IT") "#)" ) "is" ($#l1_analoaf :::"AffinPlane":::)) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool "(" "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "a")) "," (Set (Var "b")))) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "c")) "," (Set (Var "c"))) & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "c")) "," (Set (Var "d")))) "implies" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "d")) "," (Set (Var "c"))) & (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "a")) "," (Set (Var "b"))) ")" ) ")" & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "r")) "," (Set (Var "s"))) & (Bool (Bool "not" (Set (Var "p")) "," (Set (Var "q")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "r")) "," (Set (Var "s"))))) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "r")) "," (Set (Var "s"))) & (Bool (Bool "not" (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "r")) "," (Set (Var "s"))))) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" ")" ) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "c")) "," (Set (Var "x"))) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "x"))) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"OrtAfPl-like"::: ANALMETR:def 9 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analmetr :::"ParOrtStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_analmetr :::"OrtAfPl-like"::: ) ) "iff" (Bool "(" (Bool (Set ($#g1_analoaf :::"AffinStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "IT"))) "," (Set "the" ($#u1_analoaf :::"CONGR"::: ) "of" (Set (Var "IT"))) "#)" ) "is" ($#l1_analoaf :::"AffinPlane":::)) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "a")) "," (Set (Var "b")))) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "c")) "," (Set (Var "c"))) & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "c")) "," (Set (Var "d")))) "implies" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "d")) "," (Set (Var "c"))) & (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "a")) "," (Set (Var "b"))) ")" ) ")" & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "r")) "," (Set (Var "s"))) & (Bool (Bool "not" (Set (Var "p")) "," (Set (Var "q")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "r")) "," (Set (Var "s"))))) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "r")) "," (Set (Var "s"))) & (Bool (Bool "not" (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "r")) "," (Set (Var "s"))))) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" ")" ) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "c")) "," (Set (Var "x"))) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "x"))) ")" )) ")" ) ")" ) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_analmetr :::"strict"::: ) ($#v3_analmetr :::"OrtAfPl-like"::: ) for ($#l1_analmetr :::"ParOrtStr"::: ) ; end; definitionmode OrtAfPl is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_analmetr :::"OrtAfPl-like"::: ) ($#l1_analmetr :::"ParOrtStr"::: ) ; end; theorem :: ANALMETR: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 (Set ($#k2_analmetr :::"AMSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "w")) "," (Set (Var "y")) ")" ) "is" ($#l1_analmetr :::"OrtAfPl":::)))) ; theorem :: ANALMETR:35 (Bool "for" (Set (Var "POS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analmetr :::"ParOrtStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS"))) "iff" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k3_analmetr :::"Af"::: ) (Set (Var "POS")) ")" )) ")" ))) ; theorem :: ANALMETR:36 (Bool "for" (Set (Var "POS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analmetr :::"ParOrtStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) (Bool "for" (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "," (Set (Var "d9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k3_analmetr :::"Af"::: ) (Set (Var "POS")) ")" ) "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 "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) "iff" (Bool (Set (Var "a9")) "," (Set (Var "b9")) ($#r2_analoaf :::"//"::: ) (Set (Var "c9")) "," (Set (Var "d9"))) ")" )))) ; registrationlet "POS" be ($#l1_analmetr :::"OrtAfSp":::); cluster (Set ($#k3_analmetr :::"Af"::: ) "POS") -> ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v1_analoaf :::"strict"::: ) ($#v1_diraf :::"AffinSpace-like"::: ) ; end; registrationlet "POS" be ($#l1_analmetr :::"OrtAfPl":::); cluster (Set ($#k3_analmetr :::"Af"::: ) "POS") -> ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v1_analoaf :::"strict"::: ) ($#v1_diraf :::"AffinSpace-like"::: ) ($#v2_diraf :::"2-dimensional"::: ) ; end; theorem :: ANALMETR:37 (Bool "for" (Set (Var "POS")) "being" ($#l1_analmetr :::"OrtAfPl":::) "holds" (Bool (Set (Var "POS")) "is" ($#l1_analmetr :::"OrtAfSp":::))) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_analmetr :::"OrtAfPl-like"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_analmetr :::"OrtAfSp-like"::: ) for ($#l1_analmetr :::"ParOrtStr"::: ) ; end; theorem :: ANALMETR:38 (Bool "for" (Set (Var "POS")) "being" ($#l1_analmetr :::"OrtAfSp":::) "st" (Bool (Bool (Set ($#k3_analmetr :::"Af"::: ) (Set (Var "POS"))) "is" ($#l1_analoaf :::"AffinPlane":::))) "holds" (Bool (Set (Var "POS")) "is" ($#l1_analmetr :::"OrtAfPl":::))) ; theorem :: ANALMETR:39 (Bool "for" (Set (Var "POS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analmetr :::"ParOrtStr"::: ) "holds" (Bool "(" (Bool (Set (Var "POS")) "is" ($#v3_analmetr :::"OrtAfPl-like"::: ) ) "iff" (Bool "(" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) "st" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "a"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "c"))) & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "r")) "," (Set (Var "s"))) & (Bool (Bool "not" (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "r")) "," (Set (Var "s"))))) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "c")))) "implies" (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "c"))) ")" & (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) "st" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "x"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "x"))) ")" )) & (Bool "not" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) "holds" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_analoaf :::"//"::: ) (Set (Var "x")) "," (Set (Var "z"))))) & (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) "st" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "x"))) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "x"))) ")" )) & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "d"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "a")))) "implies" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) "st" (Bool "(" (Bool (Set (Var "c")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "x"))) & (Bool (Set (Var "c")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "d")) "," (Set (Var "x"))) ")" )) ")" & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "a")) "," (Set (Var "b")))) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "c")) "," (Set (Var "c"))) & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "c")) "," (Set (Var "d")))) "implies" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "d")) "," (Set (Var "c"))) & (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "a")) "," (Set (Var "b"))) ")" ) ")" & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "r")) "," (Set (Var "s"))) & (Bool (Bool "not" (Set (Var "p")) "," (Set (Var "q")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "r")) "," (Set (Var "s"))))) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "r")) "," (Set (Var "s"))) & (Bool (Bool "not" (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "r")) "," (Set (Var "s"))))) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" & (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) "st" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "c")) "," (Set (Var "x"))) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "x"))) ")" )) & "(" (Bool (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))))) "implies" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) "st" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "x"))) & (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "x"))) ")" )) ")" ")" ) ")" ) ")" ) ")" )) ; definitionlet "POS" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analmetr :::"ParOrtStr"::: ) ; let "a", "b", "c" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "POS")); pred :::"LIN"::: "a" "," "b" "," "c" means :: ANALMETR:def 10 (Bool "a" "," "b" ($#r2_analoaf :::"//"::: ) "a" "," "c"); end; :: deftheorem defines :::"LIN"::: ANALMETR:def 10 : (Bool "for" (Set (Var "POS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analmetr :::"ParOrtStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) "holds" (Bool "(" (Bool ($#r5_analmetr :::"LIN"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))) "iff" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "c"))) ")" ))); definitionlet "POS" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analmetr :::"ParOrtStr"::: ) ; let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "POS")); func :::"Line"::: "(" "a" "," "b" ")" -> ($#m1_subset_1 :::"Subset":::) "of" "POS" means :: ANALMETR:def 11 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "POS" "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool ($#r5_analmetr :::"LIN"::: ) "a" "," "b" "," (Set (Var "x"))) ")" )); end; :: deftheorem defines :::"Line"::: ANALMETR:def 11 : (Bool "for" (Set (Var "POS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analmetr :::"ParOrtStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "POS")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k4_analmetr :::"Line"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) "iff" (Bool ($#r5_analmetr :::"LIN"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x"))) ")" )) ")" )))); definitionlet "POS" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analmetr :::"ParOrtStr"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "POS")); attr "A" is :::"being_line"::: means :: ANALMETR:def 12 (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "POS" "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool "A" ($#r1_hidden :::"="::: ) (Set ($#k4_analmetr :::"Line"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) ")" )); end; :: deftheorem defines :::"being_line"::: ANALMETR:def 12 : (Bool "for" (Set (Var "POS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analmetr :::"ParOrtStr"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "POS")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v4_analmetr :::"being_line"::: ) ) "iff" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k4_analmetr :::"Line"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) ")" )) ")" ))); theorem :: ANALMETR:40 (Bool "for" (Set (Var "POS")) "being" ($#l1_analmetr :::"OrtAfSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) (Bool "for" (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k3_analmetr :::"Af"::: ) (Set (Var "POS")) ")" ) "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")))) "holds" (Bool "(" (Bool ($#r5_analmetr :::"LIN"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))) "iff" (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9"))) ")" )))) ; theorem :: ANALMETR:41 (Bool "for" (Set (Var "POS")) "being" ($#l1_analmetr :::"OrtAfSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) (Bool "for" (Set (Var "a9")) "," (Set (Var "b9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k3_analmetr :::"Af"::: ) (Set (Var "POS")) ")" ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "a9"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "b9")))) "holds" (Bool (Set ($#k4_analmetr :::"Line"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_aff_1 :::"Line"::: ) "(" (Set (Var "a9")) "," (Set (Var "b9")) ")" ))))) ; theorem :: ANALMETR:42 (Bool "for" (Set (Var "POS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analmetr :::"ParOrtStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "POS"))) "iff" (Bool (Set (Var "X")) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_analmetr :::"Af"::: ) (Set (Var "POS")) ")" )) ")" ))) ; theorem :: ANALMETR:43 (Bool "for" (Set (Var "POS")) "being" ($#l1_analmetr :::"OrtAfSp":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "POS")) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_analmetr :::"Af"::: ) (Set (Var "POS")) ")" ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "Y")))) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v4_analmetr :::"being_line"::: ) ) "iff" (Bool (Set (Var "Y")) "is" ($#v1_aff_1 :::"being_line"::: ) ) ")" )))) ; definitionlet "POS" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analmetr :::"ParOrtStr"::: ) ; let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "POS")); let "K" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "POS")); pred "a" "," "b" :::"_|_"::: "K" means :: ANALMETR:def 13 (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" "POS" "st" (Bool "(" (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q"))) & (Bool "K" ($#r1_hidden :::"="::: ) (Set ($#k4_analmetr :::"Line"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" )) & (Bool "a" "," "b" ($#r4_analmetr :::"_|_"::: ) (Set (Var "p")) "," (Set (Var "q"))) ")" )); end; :: deftheorem defines :::"_|_"::: ANALMETR:def 13 : (Bool "for" (Set (Var "POS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analmetr :::"ParOrtStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "POS")) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r6_analmetr :::"_|_"::: ) (Set (Var "K"))) "iff" (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) "st" (Bool "(" (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q"))) & (Bool (Set (Var "K")) ($#r1_hidden :::"="::: ) (Set ($#k4_analmetr :::"Line"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" )) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "p")) "," (Set (Var "q"))) ")" )) ")" )))); definitionlet "POS" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analmetr :::"ParOrtStr"::: ) ; let "K", "M" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "POS")); pred "K" :::"_|_"::: "M" means :: ANALMETR:def 14 (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" "POS" "st" (Bool "(" (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q"))) & (Bool "K" ($#r1_hidden :::"="::: ) (Set ($#k4_analmetr :::"Line"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" )) & (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r6_analmetr :::"_|_"::: ) "M") ")" )); end; :: deftheorem defines :::"_|_"::: ANALMETR:def 14 : (Bool "for" (Set (Var "POS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analmetr :::"ParOrtStr"::: ) (Bool "for" (Set (Var "K")) "," (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "POS")) "holds" (Bool "(" (Bool (Set (Var "K")) ($#r7_analmetr :::"_|_"::: ) (Set (Var "M"))) "iff" (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) "st" (Bool "(" (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q"))) & (Bool (Set (Var "K")) ($#r1_hidden :::"="::: ) (Set ($#k4_analmetr :::"Line"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" )) & (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r6_analmetr :::"_|_"::: ) (Set (Var "M"))) ")" )) ")" ))); definitionlet "POS" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analmetr :::"ParOrtStr"::: ) ; let "K", "M" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "POS")); pred "K" :::"//"::: "M" means :: ANALMETR:def 15 (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" "POS" "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "d"))) & (Bool "K" ($#r1_hidden :::"="::: ) (Set ($#k4_analmetr :::"Line"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) & (Bool "M" ($#r1_hidden :::"="::: ) (Set ($#k4_analmetr :::"Line"::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" )) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) ")" )); end; :: deftheorem defines :::"//"::: ANALMETR:def 15 : (Bool "for" (Set (Var "POS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analmetr :::"ParOrtStr"::: ) (Bool "for" (Set (Var "K")) "," (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "POS")) "holds" (Bool "(" (Bool (Set (Var "K")) ($#r8_analmetr :::"//"::: ) (Set (Var "M"))) "iff" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "d"))) & (Bool (Set (Var "K")) ($#r1_hidden :::"="::: ) (Set ($#k4_analmetr :::"Line"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) & (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set ($#k4_analmetr :::"Line"::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" )) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) ")" )) ")" ))); theorem :: ANALMETR:44 (Bool "for" (Set (Var "POS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analmetr :::"ParOrtStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) (Bool "for" (Set (Var "K")) "," (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "POS")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r6_analmetr :::"_|_"::: ) (Set (Var "K")))) "implies" (Bool (Set (Var "K")) "is" ($#v4_analmetr :::"being_line"::: ) ) ")" & "(" (Bool (Bool (Set (Var "K")) ($#r7_analmetr :::"_|_"::: ) (Set (Var "M")))) "implies" (Bool "(" (Bool (Set (Var "K")) "is" ($#v4_analmetr :::"being_line"::: ) ) & (Bool (Set (Var "M")) "is" ($#v4_analmetr :::"being_line"::: ) ) ")" ) ")" ")" )))) ; theorem :: ANALMETR:45 (Bool "for" (Set (Var "POS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analmetr :::"ParOrtStr"::: ) (Bool "for" (Set (Var "K")) "," (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "POS")) "holds" (Bool "(" (Bool (Set (Var "K")) ($#r7_analmetr :::"_|_"::: ) (Set (Var "M"))) "iff" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "d"))) & (Bool (Set (Var "K")) ($#r1_hidden :::"="::: ) (Set ($#k4_analmetr :::"Line"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) & (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set ($#k4_analmetr :::"Line"::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" )) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "c")) "," (Set (Var "d"))) ")" )) ")" ))) ; theorem :: ANALMETR:46 (Bool "for" (Set (Var "POS")) "being" ($#l1_analmetr :::"OrtAfSp":::) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "POS")) (Bool "for" (Set (Var "M9")) "," (Set (Var "N9")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_analmetr :::"Af"::: ) (Set (Var "POS")) ")" ) "st" (Bool (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set (Var "M9"))) & (Bool (Set (Var "N")) ($#r1_hidden :::"="::: ) (Set (Var "N9")))) "holds" (Bool "(" (Bool (Set (Var "M")) ($#r8_analmetr :::"//"::: ) (Set (Var "N"))) "iff" (Bool (Set (Var "M9")) ($#r5_aff_1 :::"//"::: ) (Set (Var "N9"))) ")" )))) ; theorem :: ANALMETR:47 (Bool "for" (Set (Var "POS")) "being" ($#l1_analmetr :::"OrtAfSp":::) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "POS")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) "st" (Bool (Bool (Set (Var "K")) "is" ($#v4_analmetr :::"being_line"::: ) )) "holds" (Bool (Set (Var "a")) "," (Set (Var "a")) ($#r6_analmetr :::"_|_"::: ) (Set (Var "K")))))) ; theorem :: ANALMETR:48 (Bool "for" (Set (Var "POS")) "being" ($#l1_analmetr :::"OrtAfSp":::) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "POS")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r6_analmetr :::"_|_"::: ) (Set (Var "K"))) & (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) "or" (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "b"))) ")" ) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r6_analmetr :::"_|_"::: ) (Set (Var "K")))))) ; theorem :: ANALMETR:49 (Bool "for" (Set (Var "POS")) "being" ($#l1_analmetr :::"OrtAfSp":::) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "POS")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r6_analmetr :::"_|_"::: ) (Set (Var "K")))) "holds" (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r6_analmetr :::"_|_"::: ) (Set (Var "K")))))) ; definitionlet "POS" be ($#l1_analmetr :::"OrtAfSp":::); let "K", "M" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "POS")); :: original: :::"//"::: redefine pred "K" :::"//"::: "M"; symmetry (Bool "for" (Set (Var "K")) "," (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "POS")) "st" (Bool (Bool ((Set (Const "POS")) "," (Set (Var "b1")) "," (Set (Var "b2"))))) "holds" (Bool ((Set (Const "POS")) "," (Set (Var "b2")) "," (Set (Var "b1"))))) ; end; theorem :: ANALMETR:50 (Bool "for" (Set (Var "POS")) "being" ($#l1_analmetr :::"OrtAfSp":::) (Bool "for" (Set (Var "K")) "," (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "POS")) (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) "st" (Bool (Bool (Set (Var "r")) "," (Set (Var "s")) ($#r6_analmetr :::"_|_"::: ) (Set (Var "K"))) & (Bool (Set (Var "K")) ($#r9_analmetr :::"//"::: ) (Set (Var "M")))) "holds" (Bool (Set (Var "r")) "," (Set (Var "s")) ($#r6_analmetr :::"_|_"::: ) (Set (Var "M")))))) ; theorem :: ANALMETR:51 (Bool "for" (Set (Var "POS")) "being" ($#l1_analmetr :::"OrtAfSp":::) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "POS")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r6_analmetr :::"_|_"::: ) (Set (Var "K")))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b")))))) ; definitionlet "POS" be ($#l1_analmetr :::"OrtAfSp":::); let "K", "M" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "POS")); :: original: :::"_|_"::: redefine pred "K" :::"_|_"::: "M"; irreflexivity (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "POS")) "holds" (Bool ((Set (Const "POS")) "," (Set (Var "b1")) "," (Set (Var "b1"))))) ; symmetry (Bool "for" (Set (Var "K")) "," (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "POS")) "st" (Bool (Bool ((Set (Const "POS")) "," (Set (Var "b1")) "," (Set (Var "b2"))))) "holds" (Bool ((Set (Const "POS")) "," (Set (Var "b2")) "," (Set (Var "b1"))))) ; end; theorem :: ANALMETR:52 (Bool "for" (Set (Var "POS")) "being" ($#l1_analmetr :::"OrtAfSp":::) (Bool "for" (Set (Var "K")) "," (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "POS")) "st" (Bool (Bool (Set (Var "K")) ($#r10_analmetr :::"_|_"::: ) (Set (Var "M"))) & (Bool (Set (Var "K")) ($#r9_analmetr :::"//"::: ) (Set (Var "N")))) "holds" (Bool (Set (Var "N")) ($#r10_analmetr :::"_|_"::: ) (Set (Var "M"))))) ; theorem :: ANALMETR:53 (Bool "for" (Set (Var "POS")) "being" ($#l1_analmetr :::"OrtAfSp":::) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "POS")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))) & (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r6_analmetr :::"_|_"::: ) (Set (Var "K")))) "holds" (Bool "(" (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "c")) "," (Set (Var "d"))) ")" )))) ; theorem :: ANALMETR:54 (Bool "for" (Set (Var "POS")) "being" ($#l1_analmetr :::"OrtAfSp":::) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "POS")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "K")) "is" ($#v4_analmetr :::"being_line"::: ) )) "holds" (Bool (Set (Var "K")) ($#r1_hidden :::"="::: ) (Set ($#k4_analmetr :::"Line"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))))) ; theorem :: ANALMETR:55 (Bool "for" (Set (Var "POS")) "being" ($#l1_analmetr :::"OrtAfSp":::) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "POS")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "K")) "is" ($#v4_analmetr :::"being_line"::: ) ) & (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "c")) "," (Set (Var "d"))) "or" (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "a")) "," (Set (Var "b"))) ")" )) "holds" (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r6_analmetr :::"_|_"::: ) (Set (Var "K")))))) ; theorem :: ANALMETR:56 (Bool "for" (Set (Var "POS")) "being" ($#l1_analmetr :::"OrtAfSp":::) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "POS")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "M")) ($#r10_analmetr :::"_|_"::: ) (Set (Var "N")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "c")) "," (Set (Var "d")))))) ; theorem :: ANALMETR:57 (Bool "for" (Set (Var "POS")) "being" ($#l1_analmetr :::"OrtAfSp":::) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "," (Set (Var "K")) "," (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "POS")) (Bool "for" (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))) & (Bool (Set (Var "A")) ($#r10_analmetr :::"_|_"::: ) (Set (Var "M"))) & (Bool (Set (Var "A")) ($#r10_analmetr :::"_|_"::: ) (Set (Var "N"))) & (Bool (Set (Var "K")) "is" ($#v4_analmetr :::"being_line"::: ) )) "holds" (Bool (Set (Var "A")) ($#r10_analmetr :::"_|_"::: ) (Set (Var "K")))))) ; theorem :: ANALMETR:58 (Bool "for" (Set (Var "POS")) "being" ($#l1_analmetr :::"OrtAfSp":::) (Bool "for" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) "holds" (Bool "(" (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "a")) "," (Set (Var "a"))) & (Bool (Set (Var "a")) "," (Set (Var "a")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "b")) "," (Set (Var "c"))) & (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "a"))) & (Bool (Set (Var "a")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "c"))) ")" ))) ; theorem :: ANALMETR:59 (Bool "for" (Set (Var "POS")) "being" ($#l1_analmetr :::"OrtAfSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "d")) "," (Set (Var "c"))) & (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "d")) "," (Set (Var "c"))) & (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "a"))) & (Bool (Set (Var "d")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "d")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "a"))) ")" ))) ; theorem :: ANALMETR:60 (Bool "for" (Set (Var "POS")) "being" ($#l1_analmetr :::"OrtAfSp":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q"))) & (Bool "(" (Bool "(" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) ")" ) "or" (Bool "(" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "q"))) ")" ) "or" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "q"))) ")" ) "or" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) ")" ) ")" )) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))))) ; theorem :: ANALMETR:61 (Bool "for" (Set (Var "POS")) "being" ($#l1_analmetr :::"OrtAfSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "d")) "," (Set (Var "c"))) & (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "d")) "," (Set (Var "c"))) & (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "b")) "," (Set (Var "a"))) & (Bool (Set (Var "d")) "," (Set (Var "c")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "d")) "," (Set (Var "c")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "b")) "," (Set (Var "a"))) ")" ))) ; theorem :: ANALMETR:62 (Bool "for" (Set (Var "POS")) "being" ($#l1_analmetr :::"OrtAfSp":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q"))) & (Bool "(" (Bool "(" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "c")) "," (Set (Var "d"))) ")" ) "or" (Bool "(" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "a")) "," (Set (Var "b"))) ")" ) "or" (Bool "(" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "p")) "," (Set (Var "q"))) ")" ) "or" (Bool "(" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "p")) "," (Set (Var "q"))) ")" ) "or" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "p")) "," (Set (Var "q"))) ")" ) "or" (Bool "(" (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "p")) "," (Set (Var "q"))) ")" ) "or" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "c")) "," (Set (Var "d"))) ")" ) "or" (Bool "(" (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "a")) "," (Set (Var "b"))) ")" ) ")" )) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "c")) "," (Set (Var "d"))))) ; theorem :: ANALMETR:63 (Bool "for" (Set (Var "POS")) "being" ($#l1_analmetr :::"OrtAfPl":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q"))) & (Bool "(" (Bool "(" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "c")) "," (Set (Var "d"))) ")" ) "or" (Bool "(" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "p")) "," (Set (Var "q"))) ")" ) "or" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "p")) "," (Set (Var "q"))) ")" ) "or" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "c")) "," (Set (Var "d"))) ")" ) ")" )) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))))) ; theorem :: ANALMETR:64 (Bool "for" (Set (Var "POS")) "being" ($#l1_analmetr :::"OrtAfPl":::) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "POS")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "M")) "is" ($#v4_analmetr :::"being_line"::: ) ) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "d"))) & (Bool (Set (Var "N")) "is" ($#v4_analmetr :::"being_line"::: ) ) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool (Set (Var "M")) ($#r9_analmetr :::"//"::: ) (Set (Var "N")))))) ; theorem :: ANALMETR:65 (Bool "for" (Set (Var "POS")) "being" ($#l1_analmetr :::"OrtAfPl":::) (Bool "for" (Set (Var "M")) "," (Set (Var "K")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "POS")) "st" (Bool (Bool (Set (Var "M")) ($#r10_analmetr :::"_|_"::: ) (Set (Var "K"))) & (Bool (Set (Var "N")) ($#r10_analmetr :::"_|_"::: ) (Set (Var "K")))) "holds" (Bool (Set (Var "M")) ($#r9_analmetr :::"//"::: ) (Set (Var "N"))))) ; theorem :: ANALMETR:66 (Bool "for" (Set (Var "POS")) "being" ($#l1_analmetr :::"OrtAfPl":::) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "POS")) "st" (Bool (Bool (Set (Var "M")) ($#r10_analmetr :::"_|_"::: ) (Set (Var "N")))) "holds" (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) "st" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) ")" )))) ; theorem :: ANALMETR:67 (Bool "for" (Set (Var "POS")) "being" ($#l1_analmetr :::"OrtAfPl":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) "st" (Bool "(" (Bool ($#r5_analmetr :::"LIN"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p"))) & (Bool ($#r5_analmetr :::"LIN"::: ) (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "p"))) ")" )))) ; theorem :: ANALMETR:68 (Bool "for" (Set (Var "POS")) "being" ($#l1_analmetr :::"OrtAfPl":::) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "POS")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r6_analmetr :::"_|_"::: ) (Set (Var "K")))) "holds" (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) "st" (Bool "(" (Bool ($#r5_analmetr :::"LIN"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))) ")" ))))) ; theorem :: ANALMETR:69 (Bool "for" (Set (Var "POS")) "being" ($#l1_analmetr :::"OrtAfPl":::) (Bool "for" (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) "st" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "x")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool ($#r5_analmetr :::"LIN"::: ) (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "x"))) ")" )))) ; theorem :: ANALMETR:70 (Bool "for" (Set (Var "POS")) "being" ($#l1_analmetr :::"OrtAfPl":::) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "POS")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) "st" (Bool (Bool (Set (Var "K")) "is" ($#v4_analmetr :::"being_line"::: ) )) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "POS")) "st" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "x")) ($#r6_analmetr :::"_|_"::: ) (Set (Var "K"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))) ")" ))))) ;