:: ANPROJ_2 semantic presentation begin theorem :: ANPROJ_2:1 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" )) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "u")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Bool "not" (Set (Var "v")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Bool "not" (Set (Var "w")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Bool "not" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) ($#r2_anproj_1 :::"are_LinDep"::: ) )) & (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "u")) "," (Set (Var "v")))) ")" ))) ; theorem :: ANPROJ_2:2 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "v1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "a1")) "," (Set (Var "b1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a1")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u1")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b1")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v1")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" )) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "u")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Bool "not" (Set (Var "v")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "u")) "," (Set (Var "v")))) & (Bool (Bool "not" (Set (Var "u1")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Bool "not" (Set (Var "v1")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "u1")) "," (Set (Var "v1")))) & (Bool (Bool "not" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) ($#r2_anproj_1 :::"are_LinDep"::: ) )) & (Bool (Bool "not" (Set (Var "u1")) "," (Set (Var "v1")) "," (Set (Var "u")) ($#r2_anproj_1 :::"are_LinDep"::: ) )) ")" ))) ; theorem :: ANPROJ_2:3 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool "(" "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "q")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "r")) ")" )))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "q")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" )) "holds" (Bool "for" (Set (Var "u")) "," (Set (Var "u1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "y")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) & (Bool (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "y")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) & (Bool (Bool "not" (Set (Var "y")) "is" ($#v9_struct_0 :::"zero"::: ) )) ")" ))))) ; theorem :: ANPROJ_2:4 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool "(" "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "q")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "r")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "d")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "s")) ")" )))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "q")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "r")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "d")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "s")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" )) "holds" (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Bool "not" (Set (Var "u")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Bool "not" (Set (Var "v")) "is" ($#v9_struct_0 :::"zero"::: ) ))) "holds" (Bool "ex" (Set (Var "y")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) & (Bool (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "y")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) & (Bool (Set (Var "p")) "," (Set (Var "w")) "," (Set (Var "y")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) & (Bool (Bool "not" (Set (Var "y")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Bool "not" (Set (Var "w")) "is" ($#v9_struct_0 :::"zero"::: ) )) ")" ))))) ; theorem :: ANPROJ_2:5 (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 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "a1")) "," (Set (Var "b1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a1")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u1")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b1")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v1")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" )) "holds" (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "y")) "is" ($#v9_struct_0 :::"zero"::: ) ) "or" "not" (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "y")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) "or" "not" (Bool (Set (Var "u1")) "," (Set (Var "v1")) "," (Set (Var "y")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) ")" )))) ; definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "u", "v", "w" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "V")); pred "u" "," "v" "," "w" :::"are_Prop_Vect"::: means :: ANPROJ_2:def 1 (Bool "(" (Bool (Bool "not" "u" "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Bool "not" "v" "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Bool "not" "w" "is" ($#v9_struct_0 :::"zero"::: ) )) ")" ); end; :: deftheorem defines :::"are_Prop_Vect"::: ANPROJ_2:def 1 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) ($#r1_anproj_2 :::"are_Prop_Vect"::: ) ) "iff" (Bool "(" (Bool (Bool "not" (Set (Var "u")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Bool "not" (Set (Var "v")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Bool "not" (Set (Var "w")) "is" ($#v9_struct_0 :::"zero"::: ) )) ")" ) ")" ))); definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "u", "v", "w", "u1", "v1", "w1" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "V")); pred "u" "," "v" "," "w" "," "u1" "," "v1" "," "w1" :::"lie_on_a_triangle"::: means :: ANPROJ_2:def 2 (Bool "(" (Bool "u" "," "v" "," "w1" ($#r2_anproj_1 :::"are_LinDep"::: ) ) & (Bool "u" "," "w" "," "v1" ($#r2_anproj_1 :::"are_LinDep"::: ) ) & (Bool "v" "," "w" "," "u1" ($#r2_anproj_1 :::"are_LinDep"::: ) ) ")" ); end; :: deftheorem defines :::"lie_on_a_triangle"::: ANPROJ_2: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 "u1")) "," (Set (Var "v1")) "," (Set (Var "w1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "u1")) "," (Set (Var "v1")) "," (Set (Var "w1")) ($#r2_anproj_2 :::"lie_on_a_triangle"::: ) ) "iff" (Bool "(" (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w1")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) & (Bool (Set (Var "u")) "," (Set (Var "w")) "," (Set (Var "v1")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) & (Bool (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "u1")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) ")" ) ")" ))); definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "o", "u", "v", "w", "u2", "v2", "w2" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "V")); pred "o" "," "u" "," "v" "," "w" "," "u2" "," "v2" "," "w2" :::"are_perspective"::: means :: ANPROJ_2:def 3 (Bool "(" (Bool "o" "," "u" "," "u2" ($#r2_anproj_1 :::"are_LinDep"::: ) ) & (Bool "o" "," "v" "," "v2" ($#r2_anproj_1 :::"are_LinDep"::: ) ) & (Bool "o" "," "w" "," "w2" ($#r2_anproj_1 :::"are_LinDep"::: ) ) ")" ); end; :: deftheorem defines :::"are_perspective"::: ANPROJ_2:def 3 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "o")) "," (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "u2")) "," (Set (Var "v2")) "," (Set (Var "w2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "o")) "," (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "u2")) "," (Set (Var "v2")) "," (Set (Var "w2")) ($#r3_anproj_2 :::"are_perspective"::: ) ) "iff" (Bool "(" (Bool (Set (Var "o")) "," (Set (Var "u")) "," (Set (Var "u2")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) & (Bool (Set (Var "o")) "," (Set (Var "v")) "," (Set (Var "v2")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) & (Bool (Set (Var "o")) "," (Set (Var "w")) "," (Set (Var "w2")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) ")" ) ")" ))); theorem :: ANPROJ_2:6 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "o")) "," (Set (Var "u")) "," (Set (Var "u2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "o")) "," (Set (Var "u")) "," (Set (Var "u2")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) & (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "o")) "," (Set (Var "u")))) & (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "o")) "," (Set (Var "u2")))) & (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "u")) "," (Set (Var "u2")))) & (Bool (Set (Var "o")) "," (Set (Var "u")) "," (Set (Var "u2")) ($#r1_anproj_2 :::"are_Prop_Vect"::: ) )) "holds" (Bool "(" (Bool "ex" (Set (Var "a1")) "," (Set (Var "b1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Set (Var "b1")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "o")) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a1")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" ))) & (Bool (Set (Var "a1")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b1")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) & (Bool "ex" (Set (Var "a2")) "," (Set (Var "c2")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "u2")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "c2")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "o")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a2")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" ))) & (Bool (Set (Var "c2")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "a2")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ")" ))) ; theorem :: ANPROJ_2:7 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) & (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "p")) "," (Set (Var "q")))) & (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) ($#r1_anproj_2 :::"are_Prop_Vect"::: ) )) "holds" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "q")) ")" )))))) ; theorem :: ANPROJ_2:8 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "o")) "," (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "u2")) "," (Set (Var "v2")) "," (Set (Var "w2")) "," (Set (Var "u1")) "," (Set (Var "v1")) "," (Set (Var "w1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Bool "not" (Set (Var "o")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) ($#r1_anproj_2 :::"are_Prop_Vect"::: ) ) & (Bool (Set (Var "u2")) "," (Set (Var "v2")) "," (Set (Var "w2")) ($#r1_anproj_2 :::"are_Prop_Vect"::: ) ) & (Bool (Set (Var "u1")) "," (Set (Var "v1")) "," (Set (Var "w1")) ($#r1_anproj_2 :::"are_Prop_Vect"::: ) ) & (Bool (Set (Var "o")) "," (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "u2")) "," (Set (Var "v2")) "," (Set (Var "w2")) ($#r3_anproj_2 :::"are_perspective"::: ) ) & (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "o")) "," (Set (Var "u2")))) & (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "o")) "," (Set (Var "v2")))) & (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "o")) "," (Set (Var "w2")))) & (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "u")) "," (Set (Var "u2")))) & (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "v")) "," (Set (Var "v2")))) & (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "w")) "," (Set (Var "w2")))) & (Bool (Bool "not" (Set (Var "o")) "," (Set (Var "u")) "," (Set (Var "v")) ($#r2_anproj_1 :::"are_LinDep"::: ) )) & (Bool (Bool "not" (Set (Var "o")) "," (Set (Var "u")) "," (Set (Var "w")) ($#r2_anproj_1 :::"are_LinDep"::: ) )) & (Bool (Bool "not" (Set (Var "o")) "," (Set (Var "v")) "," (Set (Var "w")) ($#r2_anproj_1 :::"are_LinDep"::: ) )) & (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "u1")) "," (Set (Var "v1")) "," (Set (Var "w1")) ($#r2_anproj_2 :::"lie_on_a_triangle"::: ) ) & (Bool (Set (Var "u2")) "," (Set (Var "v2")) "," (Set (Var "w2")) "," (Set (Var "u1")) "," (Set (Var "v1")) "," (Set (Var "w1")) ($#r2_anproj_2 :::"lie_on_a_triangle"::: ) )) "holds" (Bool (Set (Var "u1")) "," (Set (Var "v1")) "," (Set (Var "w1")) ($#r2_anproj_1 :::"are_LinDep"::: ) ))) ; definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "o", "u", "v", "w", "u2", "v2", "w2" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "V")); pred "o" "," "u" "," "v" "," "w" "," "u2" "," "v2" "," "w2" :::"lie_on_an_angle"::: means :: ANPROJ_2:def 4 (Bool "(" (Bool (Bool "not" "o" "," "u" "," "u2" ($#r2_anproj_1 :::"are_LinDep"::: ) )) & (Bool "o" "," "u" "," "v" ($#r2_anproj_1 :::"are_LinDep"::: ) ) & (Bool "o" "," "u" "," "w" ($#r2_anproj_1 :::"are_LinDep"::: ) ) & (Bool "o" "," "u2" "," "v2" ($#r2_anproj_1 :::"are_LinDep"::: ) ) & (Bool "o" "," "u2" "," "w2" ($#r2_anproj_1 :::"are_LinDep"::: ) ) ")" ); end; :: deftheorem defines :::"lie_on_an_angle"::: ANPROJ_2:def 4 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "o")) "," (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "u2")) "," (Set (Var "v2")) "," (Set (Var "w2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "o")) "," (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "u2")) "," (Set (Var "v2")) "," (Set (Var "w2")) ($#r4_anproj_2 :::"lie_on_an_angle"::: ) ) "iff" (Bool "(" (Bool (Bool "not" (Set (Var "o")) "," (Set (Var "u")) "," (Set (Var "u2")) ($#r2_anproj_1 :::"are_LinDep"::: ) )) & (Bool (Set (Var "o")) "," (Set (Var "u")) "," (Set (Var "v")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) & (Bool (Set (Var "o")) "," (Set (Var "u")) "," (Set (Var "w")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) & (Bool (Set (Var "o")) "," (Set (Var "u2")) "," (Set (Var "v2")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) & (Bool (Set (Var "o")) "," (Set (Var "u2")) "," (Set (Var "w2")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) ")" ) ")" ))); definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "o", "u", "v", "w", "u2", "v2", "w2" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "V")); pred "o" "," "u" "," "v" "," "w" "," "u2" "," "v2" "," "w2" :::"are_half_mutually_not_Prop"::: means :: ANPROJ_2:def 5 (Bool "(" (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) "o" "," "v")) & (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) "o" "," "w")) & (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) "o" "," "v2")) & (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) "o" "," "w2")) & (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) "u" "," "v")) & (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) "u" "," "w")) & (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) "u2" "," "v2")) & (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) "u2" "," "w2")) & (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) "v" "," "w")) & (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) "v2" "," "w2")) ")" ); end; :: deftheorem defines :::"are_half_mutually_not_Prop"::: ANPROJ_2:def 5 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "o")) "," (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "u2")) "," (Set (Var "v2")) "," (Set (Var "w2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "o")) "," (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "u2")) "," (Set (Var "v2")) "," (Set (Var "w2")) ($#r5_anproj_2 :::"are_half_mutually_not_Prop"::: ) ) "iff" (Bool "(" (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "o")) "," (Set (Var "v")))) & (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "o")) "," (Set (Var "w")))) & (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "o")) "," (Set (Var "v2")))) & (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "o")) "," (Set (Var "w2")))) & (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "u")) "," (Set (Var "v")))) & (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "u")) "," (Set (Var "w")))) & (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "u2")) "," (Set (Var "v2")))) & (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "u2")) "," (Set (Var "w2")))) & (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "v")) "," (Set (Var "w")))) & (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "v2")) "," (Set (Var "w2")))) ")" ) ")" ))); theorem :: ANPROJ_2:9 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "o")) "," (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "u2")) "," (Set (Var "v2")) "," (Set (Var "w2")) "," (Set (Var "u1")) "," (Set (Var "v1")) "," (Set (Var "w1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Bool "not" (Set (Var "o")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) ($#r1_anproj_2 :::"are_Prop_Vect"::: ) ) & (Bool (Set (Var "u2")) "," (Set (Var "v2")) "," (Set (Var "w2")) ($#r1_anproj_2 :::"are_Prop_Vect"::: ) ) & (Bool (Set (Var "u1")) "," (Set (Var "v1")) "," (Set (Var "w1")) ($#r1_anproj_2 :::"are_Prop_Vect"::: ) ) & (Bool (Set (Var "o")) "," (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "u2")) "," (Set (Var "v2")) "," (Set (Var "w2")) ($#r4_anproj_2 :::"lie_on_an_angle"::: ) ) & (Bool (Set (Var "o")) "," (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "u2")) "," (Set (Var "v2")) "," (Set (Var "w2")) ($#r5_anproj_2 :::"are_half_mutually_not_Prop"::: ) ) & (Bool (Set (Var "u")) "," (Set (Var "v2")) "," (Set (Var "w1")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) & (Bool (Set (Var "u2")) "," (Set (Var "v")) "," (Set (Var "w1")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) & (Bool (Set (Var "u")) "," (Set (Var "w2")) "," (Set (Var "v1")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) & (Bool (Set (Var "w")) "," (Set (Var "u2")) "," (Set (Var "v1")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) & (Bool (Set (Var "v")) "," (Set (Var "w2")) "," (Set (Var "u1")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) & (Bool (Set (Var "w")) "," (Set (Var "v2")) "," (Set (Var "u1")) ($#r2_anproj_1 :::"are_LinDep"::: ) )) "holds" (Bool (Set (Var "u1")) "," (Set (Var "v1")) "," (Set (Var "w1")) ($#r2_anproj_1 :::"are_LinDep"::: ) ))) ; theorem :: ANPROJ_2:10 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) (Bool "ex" (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set (Var "x1")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" )))) ; theorem :: ANPROJ_2:11 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2"))) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x3"))) & (Bool (Set (Var "x2")) ($#r1_hidden :::"<>"::: ) (Set (Var "x3"))) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set (Var "x1")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) & (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "x2"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2")))) "holds" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) & (Bool (Set (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "x3"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set (Var "x3")))) "holds" (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) ")" ) "," (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "b")) "," (Set (Var "g")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ")" ) "," (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "c")) "," (Set (Var "h")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k8_funcsdom :::"RealFuncZero"::: ) (Set (Var "A"))))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))))) ; theorem :: ANPROJ_2:12 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2"))) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x3"))) & (Bool (Set (Var "x2")) ($#r1_hidden :::"<>"::: ) (Set (Var "x3")))) "holds" (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "st" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) ")" ) "," (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "b")) "," (Set (Var "g")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ")" ) "," (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "c")) "," (Set (Var "h")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k8_funcsdom :::"RealFuncZero"::: ) (Set (Var "A"))))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))))) ; theorem :: ANPROJ_2:13 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k8_domain_1 :::"}"::: ) )) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2"))) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x3"))) & (Bool (Set (Var "x2")) ($#r1_hidden :::"<>"::: ) (Set (Var "x3"))) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set (Var "x1")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) & (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "x2"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2")))) "holds" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) & (Bool (Set (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "x3"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set (Var "x3")))) "holds" (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) "holds" (Bool "for" (Set (Var "h9")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Var "h9")) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) ")" ) "," (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "b")) "," (Set (Var "g")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ")" ) "," (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "c")) "," (Set (Var "h")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ))))))) ; theorem :: ANPROJ_2:14 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k8_domain_1 :::"}"::: ) )) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2"))) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x3"))) & (Bool (Set (Var "x2")) ($#r1_hidden :::"<>"::: ) (Set (Var "x3")))) "holds" (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "st" (Bool "for" (Set (Var "h9")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Var "h9")) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) ")" ) "," (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "b")) "," (Set (Var "g")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ")" ) "," (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "c")) "," (Set (Var "h")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ))))))) ; theorem :: ANPROJ_2:15 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k8_domain_1 :::"}"::: ) )) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2"))) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x3"))) & (Bool (Set (Var "x2")) ($#r1_hidden :::"<>"::: ) (Set (Var "x3")))) "holds" (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "st" (Bool "(" (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) ")" ) "," (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "b")) "," (Set (Var "g")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ")" ) "," (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "c")) "," (Set (Var "h")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k8_funcsdom :::"RealFuncZero"::: ) (Set (Var "A"))))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ) & (Bool "(" "for" (Set (Var "h9")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Var "h9")) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) ")" ) "," (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "b")) "," (Set (Var "g")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ")" ) "," (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "c")) "," (Set (Var "h")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ))) ")" ) ")" )))) ; theorem :: ANPROJ_2:16 (Bool "ex" (Set (Var "V")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_rlvect_1 :::"RealLinearSpace":::)(Bool "ex" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w")) ")" )))) ")" ) ")" ))) ; theorem :: ANPROJ_2:17 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "," (Set (Var "f1")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2"))) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x3"))) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x4"))) & (Bool (Set (Var "x2")) ($#r1_hidden :::"<>"::: ) (Set (Var "x3"))) & (Bool (Set (Var "x2")) ($#r1_hidden :::"<>"::: ) (Set (Var "x4"))) & (Bool (Set (Var "x3")) ($#r1_hidden :::"<>"::: ) (Set (Var "x4"))) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set (Var "x1")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) & (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "x2"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2")))) "holds" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) & (Bool (Set (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "x3"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set (Var "x3")))) "holds" (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) & (Bool (Set (Set (Var "f1")) ($#k3_funct_2 :::"."::: ) (Set (Var "x4"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set (Var "x4")))) "holds" (Bool (Set (Set (Var "f1")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) ")" ) "," (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "b")) "," (Set (Var "g")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ")" ) "," (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "c")) "," (Set (Var "h")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ")" ) "," (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "d")) "," (Set (Var "f1")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k8_funcsdom :::"RealFuncZero"::: ) (Set (Var "A"))))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))))) ; theorem :: ANPROJ_2:18 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2"))) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x3"))) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x4"))) & (Bool (Set (Var "x2")) ($#r1_hidden :::"<>"::: ) (Set (Var "x3"))) & (Bool (Set (Var "x2")) ($#r1_hidden :::"<>"::: ) (Set (Var "x4"))) & (Bool (Set (Var "x3")) ($#r1_hidden :::"<>"::: ) (Set (Var "x4")))) "holds" (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "," (Set (Var "f1")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "st" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) ")" ) "," (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "b")) "," (Set (Var "g")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ")" ) "," (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "c")) "," (Set (Var "h")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ")" ) "," (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "d")) "," (Set (Var "f1")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k8_funcsdom :::"RealFuncZero"::: ) (Set (Var "A"))))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))))) ; theorem :: ANPROJ_2:19 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "," (Set (Var "f1")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k9_domain_1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k9_domain_1 :::"}"::: ) )) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2"))) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x3"))) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x4"))) & (Bool (Set (Var "x2")) ($#r1_hidden :::"<>"::: ) (Set (Var "x3"))) & (Bool (Set (Var "x2")) ($#r1_hidden :::"<>"::: ) (Set (Var "x4"))) & (Bool (Set (Var "x3")) ($#r1_hidden :::"<>"::: ) (Set (Var "x4"))) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set (Var "x1")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) & (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "x2"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2")))) "holds" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) & (Bool (Set (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "x3"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set (Var "x3")))) "holds" (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) & (Bool (Set (Set (Var "f1")) ($#k3_funct_2 :::"."::: ) (Set (Var "x4"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set (Var "x4")))) "holds" (Bool (Set (Set (Var "f1")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) "holds" (Bool "for" (Set (Var "h9")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Var "h9")) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) ")" ) "," (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "b")) "," (Set (Var "g")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ")" ) "," (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "c")) "," (Set (Var "h")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ")" ) "," (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "d")) "," (Set (Var "f1")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ))))))) ; theorem :: ANPROJ_2:20 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k9_domain_1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k9_domain_1 :::"}"::: ) )) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2"))) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x3"))) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x4"))) & (Bool (Set (Var "x2")) ($#r1_hidden :::"<>"::: ) (Set (Var "x3"))) & (Bool (Set (Var "x2")) ($#r1_hidden :::"<>"::: ) (Set (Var "x4"))) & (Bool (Set (Var "x3")) ($#r1_hidden :::"<>"::: ) (Set (Var "x4")))) "holds" (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "," (Set (Var "f1")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "st" (Bool "for" (Set (Var "h9")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Var "h9")) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) ")" ) "," (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "b")) "," (Set (Var "g")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ")" ) "," (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "c")) "," (Set (Var "h")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ")" ) "," (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "d")) "," (Set (Var "f1")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ))))))) ; theorem :: ANPROJ_2:21 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k9_domain_1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k9_domain_1 :::"}"::: ) )) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2"))) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x3"))) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x4"))) & (Bool (Set (Var "x2")) ($#r1_hidden :::"<>"::: ) (Set (Var "x3"))) & (Bool (Set (Var "x2")) ($#r1_hidden :::"<>"::: ) (Set (Var "x4"))) & (Bool (Set (Var "x3")) ($#r1_hidden :::"<>"::: ) (Set (Var "x4")))) "holds" (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "," (Set (Var "f1")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "st" (Bool "(" (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) ")" ) "," (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "b")) "," (Set (Var "g")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ")" ) "," (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "c")) "," (Set (Var "h")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ")" ) "," (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "d")) "," (Set (Var "f1")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k8_funcsdom :::"RealFuncZero"::: ) (Set (Var "A"))))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ) & (Bool "(" "for" (Set (Var "h9")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Var "h9")) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) ")" ) "," (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "b")) "," (Set (Var "g")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ")" ) "," (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "c")) "," (Set (Var "h")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ")" ) "," (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "d")) "," (Set (Var "f1")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ))) ")" ) ")" )))) ; theorem :: ANPROJ_2:22 (Bool "ex" (Set (Var "V")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_rlvect_1 :::"RealLinearSpace":::)(Bool "ex" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "u1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "d")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u1")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "d")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u1")) ")" )))) ")" ) ")" ))) ; definitionlet "IT" be ($#l1_rlvect_1 :::"RealLinearSpace":::); attr "IT" is :::"up-3-dimensional"::: means :: ANPROJ_2:def 6 (Bool "ex" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w1")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w1")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "IT"))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))); end; :: deftheorem defines :::"up-3-dimensional"::: ANPROJ_2:def 6 : (Bool "for" (Set (Var "IT")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_anproj_2 :::"up-3-dimensional"::: ) ) "iff" (Bool "ex" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w1")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "IT"))))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) bbbadV13_ALGSTR_0() ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) ($#v1_anproj_2 :::"up-3-dimensional"::: ) for ($#l1_rlvect_1 :::"RLSStruct"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) bbbadV13_ALGSTR_0() ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) ($#v1_anproj_2 :::"up-3-dimensional"::: ) -> ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) for ($#l1_rlvect_1 :::"RLSStruct"::: ) ; end; definitionlet "CS" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_collsp :::"CollStr"::: ) ; redefine attr "CS" is :::"reflexive"::: means :: ANPROJ_2:def 7 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" "CS" "holds" (Bool "(" (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "p")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p")) "," (Set (Var "p")) "," (Set (Var "q")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "q")) ($#r1_collsp :::"is_collinear"::: ) ) ")" )); redefine attr "CS" is :::"transitive"::: means :: ANPROJ_2:def 8 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Element":::) "of" "CS" "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q"))) & (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r1")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r2")) ($#r1_collsp :::"is_collinear"::: ) )) "holds" (Bool (Set (Var "r")) "," (Set (Var "r1")) "," (Set (Var "r2")) ($#r1_collsp :::"is_collinear"::: ) )); end; :: deftheorem defines :::"reflexive"::: ANPROJ_2:def 7 : (Bool "for" (Set (Var "CS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_collsp :::"CollStr"::: ) "holds" (Bool "(" (Bool (Set (Var "CS")) "is" ($#v2_collsp :::"reflexive"::: ) ) "iff" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "CS")) "holds" (Bool "(" (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "p")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p")) "," (Set (Var "p")) "," (Set (Var "q")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "q")) ($#r1_collsp :::"is_collinear"::: ) ) ")" )) ")" )); :: deftheorem defines :::"transitive"::: ANPROJ_2:def 8 : (Bool "for" (Set (Var "CS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_collsp :::"CollStr"::: ) "holds" (Bool "(" (Bool (Set (Var "CS")) "is" ($#v3_collsp :::"transitive"::: ) ) "iff" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "CS")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q"))) & (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r1")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r2")) ($#r1_collsp :::"is_collinear"::: ) )) "holds" (Bool (Set (Var "r")) "," (Set (Var "r1")) "," (Set (Var "r2")) ($#r1_collsp :::"is_collinear"::: ) )) ")" )); definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_collsp :::"CollStr"::: ) ; attr "IT" is :::"Vebleian"::: means :: ANPROJ_2:def 9 (Bool "for" (Set (Var "p")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "r")) "," (Set (Var "r1")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Bool (Set (Var "p")) "," (Set (Var "p1")) "," (Set (Var "r")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "r1")) ($#r1_collsp :::"is_collinear"::: ) )) "holds" (Bool "ex" (Set (Var "r2")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool "(" (Bool (Set (Var "p")) "," (Set (Var "p2")) "," (Set (Var "r2")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "r")) "," (Set (Var "r1")) "," (Set (Var "r2")) ($#r1_collsp :::"is_collinear"::: ) ) ")" ))); attr "IT" is :::"at_least_3rank"::: means :: ANPROJ_2:def 10 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool "(" (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "r"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"<>"::: ) (Set (Var "r"))) & (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) ($#r1_collsp :::"is_collinear"::: ) ) ")" ))); end; :: deftheorem defines :::"Vebleian"::: ANPROJ_2:def 9 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_collsp :::"CollStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_anproj_2 :::"Vebleian"::: ) ) "iff" (Bool "for" (Set (Var "p")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "r")) "," (Set (Var "r1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Var "p")) "," (Set (Var "p1")) "," (Set (Var "r")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "r1")) ($#r1_collsp :::"is_collinear"::: ) )) "holds" (Bool "ex" (Set (Var "r2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool "(" (Bool (Set (Var "p")) "," (Set (Var "p2")) "," (Set (Var "r2")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "r")) "," (Set (Var "r1")) "," (Set (Var "r2")) ($#r1_collsp :::"is_collinear"::: ) ) ")" ))) ")" )); :: deftheorem defines :::"at_least_3rank"::: ANPROJ_2:def 10 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_collsp :::"CollStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_anproj_2 :::"at_least_3rank"::: ) ) "iff" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool "(" (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "r"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"<>"::: ) (Set (Var "r"))) & (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) ($#r1_collsp :::"is_collinear"::: ) ) ")" ))) ")" )); theorem :: ANPROJ_2:23 (Bool "for" (Set (Var "V")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_anproj_1 :::"ProjectiveSpace"::: ) (Set (Var "V")) ")" ) "holds" (Bool "(" (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) ($#r1_collsp :::"is_collinear"::: ) ) "iff" (Bool "ex" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k2_anproj_1 :::"Dir"::: ) (Set (Var "u")))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set ($#k2_anproj_1 :::"Dir"::: ) (Set (Var "v")))) & (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k2_anproj_1 :::"Dir"::: ) (Set (Var "w")))) & (Bool (Bool "not" (Set (Var "u")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Bool "not" (Set (Var "v")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Bool "not" (Set (Var "w")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) ")" )) ")" ))) ; registrationlet "V" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_rlvect_1 :::"RealLinearSpace":::); cluster (Set ($#k5_anproj_1 :::"ProjectiveSpace"::: ) "V") -> ($#v2_collsp :::"reflexive"::: ) ($#v3_collsp :::"transitive"::: ) ; end; theorem :: ANPROJ_2:24 (Bool "for" (Set (Var "V")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_anproj_1 :::"ProjectiveSpace"::: ) (Set (Var "V")) ")" ) "st" (Bool (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) ($#r1_collsp :::"is_collinear"::: ) )) "holds" (Bool "(" (Bool (Set (Var "p")) "," (Set (Var "r")) "," (Set (Var "q")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "q")) "," (Set (Var "p")) "," (Set (Var "r")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "r")) "," (Set (Var "q")) "," (Set (Var "p")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "r")) "," (Set (Var "p")) "," (Set (Var "q")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "p")) ($#r1_collsp :::"is_collinear"::: ) ) ")" ))) ; registrationlet "V" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_rlvect_1 :::"RealLinearSpace":::); cluster (Set ($#k5_anproj_1 :::"ProjectiveSpace"::: ) "V") -> ($#v2_anproj_2 :::"Vebleian"::: ) ; end; registrationlet "V" be ($#v1_anproj_2 :::"up-3-dimensional"::: ) ($#l1_rlvect_1 :::"RealLinearSpace":::); cluster (Set ($#k5_anproj_1 :::"ProjectiveSpace"::: ) "V") -> ($#v4_collsp :::"proper"::: ) ; end; theorem :: ANPROJ_2:25 (Bool "for" (Set (Var "V")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_rlvect_1 :::"RealLinearSpace":::) "st" (Bool (Bool "ex" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )))) "holds" (Bool (Set ($#k5_anproj_1 :::"ProjectiveSpace"::: ) (Set (Var "V"))) "is" ($#v3_anproj_2 :::"at_least_3rank"::: ) )) ; registrationlet "V" be ($#v1_anproj_2 :::"up-3-dimensional"::: ) ($#l1_rlvect_1 :::"RealLinearSpace":::); cluster (Set ($#k5_anproj_1 :::"ProjectiveSpace"::: ) "V") -> ($#v3_anproj_2 :::"at_least_3rank"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_collsp :::"reflexive"::: ) ($#v3_collsp :::"transitive"::: ) ($#v4_collsp :::"proper"::: ) ($#v2_anproj_2 :::"Vebleian"::: ) ($#v3_anproj_2 :::"at_least_3rank"::: ) for ($#l1_collsp :::"CollStr"::: ) ; end; definitionmode CollProjectiveSpace is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_collsp :::"reflexive"::: ) ($#v3_collsp :::"transitive"::: ) ($#v4_collsp :::"proper"::: ) ($#v2_anproj_2 :::"Vebleian"::: ) ($#v3_anproj_2 :::"at_least_3rank"::: ) ($#l1_collsp :::"CollStr"::: ) ; end; definitionlet "IT" be ($#l1_collsp :::"CollProjectiveSpace":::); attr "IT" is :::"Fanoian"::: means :: ANPROJ_2:def 11 (Bool "for" (Set (Var "p1")) "," (Set (Var "r2")) "," (Set (Var "q")) "," (Set (Var "r1")) "," (Set (Var "q1")) "," (Set (Var "p")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Bool (Set (Var "p1")) "," (Set (Var "r2")) "," (Set (Var "q")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "r1")) "," (Set (Var "q1")) "," (Set (Var "q")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p1")) "," (Set (Var "r1")) "," (Set (Var "p")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "r2")) "," (Set (Var "q1")) "," (Set (Var "p")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p1")) "," (Set (Var "q1")) "," (Set (Var "r")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "r2")) "," (Set (Var "r1")) "," (Set (Var "r")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Bool "not" (Set (Var "p1")) "," (Set (Var "r2")) "," (Set (Var "q1")) ($#r1_collsp :::"is_collinear"::: ) )) & (Bool (Bool "not" (Set (Var "p1")) "," (Set (Var "r2")) "," (Set (Var "r1")) ($#r1_collsp :::"is_collinear"::: ) )) & (Bool (Bool "not" (Set (Var "p1")) "," (Set (Var "r1")) "," (Set (Var "q1")) ($#r1_collsp :::"is_collinear"::: ) ))) "holds" (Bool (Set (Var "r2")) "," (Set (Var "r1")) "," (Set (Var "q1")) ($#r1_collsp :::"is_collinear"::: ) )); attr "IT" is :::"Desarguesian"::: means :: ANPROJ_2:def 12 (Bool "for" (Set (Var "o")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "q3")) "," (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "r3")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "q1"))) & (Bool (Set (Var "p1")) ($#r1_hidden :::"<>"::: ) (Set (Var "q1"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "q2"))) & (Bool (Set (Var "p2")) ($#r1_hidden :::"<>"::: ) (Set (Var "q2"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "q3"))) & (Bool (Set (Var "p3")) ($#r1_hidden :::"<>"::: ) (Set (Var "q3"))) & (Bool (Bool "not" (Set (Var "o")) "," (Set (Var "p1")) "," (Set (Var "p2")) ($#r1_collsp :::"is_collinear"::: ) )) & (Bool (Bool "not" (Set (Var "o")) "," (Set (Var "p1")) "," (Set (Var "p3")) ($#r1_collsp :::"is_collinear"::: ) )) & (Bool (Bool "not" (Set (Var "o")) "," (Set (Var "p2")) "," (Set (Var "p3")) ($#r1_collsp :::"is_collinear"::: ) )) & (Bool (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "r3")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "r3")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "r1")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "q2")) "," (Set (Var "q3")) "," (Set (Var "r1")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p1")) "," (Set (Var "p3")) "," (Set (Var "r2")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "q1")) "," (Set (Var "q3")) "," (Set (Var "r2")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "o")) "," (Set (Var "p1")) "," (Set (Var "q1")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "o")) "," (Set (Var "p2")) "," (Set (Var "q2")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "o")) "," (Set (Var "p3")) "," (Set (Var "q3")) ($#r1_collsp :::"is_collinear"::: ) )) "holds" (Bool (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "r3")) ($#r1_collsp :::"is_collinear"::: ) )); attr "IT" is :::"Pappian"::: means :: ANPROJ_2:def 13 (Bool "for" (Set (Var "o")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "q3")) "," (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "r3")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "p2"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "p3"))) & (Bool (Set (Var "p2")) ($#r1_hidden :::"<>"::: ) (Set (Var "p3"))) & (Bool (Set (Var "p1")) ($#r1_hidden :::"<>"::: ) (Set (Var "p2"))) & (Bool (Set (Var "p1")) ($#r1_hidden :::"<>"::: ) (Set (Var "p3"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "q2"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "q3"))) & (Bool (Set (Var "q2")) ($#r1_hidden :::"<>"::: ) (Set (Var "q3"))) & (Bool (Set (Var "q1")) ($#r1_hidden :::"<>"::: ) (Set (Var "q2"))) & (Bool (Set (Var "q1")) ($#r1_hidden :::"<>"::: ) (Set (Var "q3"))) & (Bool (Bool "not" (Set (Var "o")) "," (Set (Var "p1")) "," (Set (Var "q1")) ($#r1_collsp :::"is_collinear"::: ) )) & (Bool (Set (Var "o")) "," (Set (Var "p1")) "," (Set (Var "p2")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "o")) "," (Set (Var "p1")) "," (Set (Var "p3")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "o")) "," (Set (Var "q1")) "," (Set (Var "q2")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "o")) "," (Set (Var "q1")) "," (Set (Var "q3")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p1")) "," (Set (Var "q2")) "," (Set (Var "r3")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "q1")) "," (Set (Var "p2")) "," (Set (Var "r3")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p1")) "," (Set (Var "q3")) "," (Set (Var "r2")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p3")) "," (Set (Var "q1")) "," (Set (Var "r2")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p2")) "," (Set (Var "q3")) "," (Set (Var "r1")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p3")) "," (Set (Var "q2")) "," (Set (Var "r1")) ($#r1_collsp :::"is_collinear"::: ) )) "holds" (Bool (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "r3")) ($#r1_collsp :::"is_collinear"::: ) )); end; :: deftheorem defines :::"Fanoian"::: ANPROJ_2:def 11 : (Bool "for" (Set (Var "IT")) "being" ($#l1_collsp :::"CollProjectiveSpace":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v4_anproj_2 :::"Fanoian"::: ) ) "iff" (Bool "for" (Set (Var "p1")) "," (Set (Var "r2")) "," (Set (Var "q")) "," (Set (Var "r1")) "," (Set (Var "q1")) "," (Set (Var "p")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Var "p1")) "," (Set (Var "r2")) "," (Set (Var "q")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "r1")) "," (Set (Var "q1")) "," (Set (Var "q")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p1")) "," (Set (Var "r1")) "," (Set (Var "p")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "r2")) "," (Set (Var "q1")) "," (Set (Var "p")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p1")) "," (Set (Var "q1")) "," (Set (Var "r")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "r2")) "," (Set (Var "r1")) "," (Set (Var "r")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Bool "not" (Set (Var "p1")) "," (Set (Var "r2")) "," (Set (Var "q1")) ($#r1_collsp :::"is_collinear"::: ) )) & (Bool (Bool "not" (Set (Var "p1")) "," (Set (Var "r2")) "," (Set (Var "r1")) ($#r1_collsp :::"is_collinear"::: ) )) & (Bool (Bool "not" (Set (Var "p1")) "," (Set (Var "r1")) "," (Set (Var "q1")) ($#r1_collsp :::"is_collinear"::: ) ))) "holds" (Bool (Set (Var "r2")) "," (Set (Var "r1")) "," (Set (Var "q1")) ($#r1_collsp :::"is_collinear"::: ) )) ")" )); :: deftheorem defines :::"Desarguesian"::: ANPROJ_2:def 12 : (Bool "for" (Set (Var "IT")) "being" ($#l1_collsp :::"CollProjectiveSpace":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v5_anproj_2 :::"Desarguesian"::: ) ) "iff" (Bool "for" (Set (Var "o")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "q3")) "," (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "r3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "q1"))) & (Bool (Set (Var "p1")) ($#r1_hidden :::"<>"::: ) (Set (Var "q1"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "q2"))) & (Bool (Set (Var "p2")) ($#r1_hidden :::"<>"::: ) (Set (Var "q2"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "q3"))) & (Bool (Set (Var "p3")) ($#r1_hidden :::"<>"::: ) (Set (Var "q3"))) & (Bool (Bool "not" (Set (Var "o")) "," (Set (Var "p1")) "," (Set (Var "p2")) ($#r1_collsp :::"is_collinear"::: ) )) & (Bool (Bool "not" (Set (Var "o")) "," (Set (Var "p1")) "," (Set (Var "p3")) ($#r1_collsp :::"is_collinear"::: ) )) & (Bool (Bool "not" (Set (Var "o")) "," (Set (Var "p2")) "," (Set (Var "p3")) ($#r1_collsp :::"is_collinear"::: ) )) & (Bool (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "r3")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "r3")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "r1")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "q2")) "," (Set (Var "q3")) "," (Set (Var "r1")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p1")) "," (Set (Var "p3")) "," (Set (Var "r2")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "q1")) "," (Set (Var "q3")) "," (Set (Var "r2")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "o")) "," (Set (Var "p1")) "," (Set (Var "q1")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "o")) "," (Set (Var "p2")) "," (Set (Var "q2")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "o")) "," (Set (Var "p3")) "," (Set (Var "q3")) ($#r1_collsp :::"is_collinear"::: ) )) "holds" (Bool (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "r3")) ($#r1_collsp :::"is_collinear"::: ) )) ")" )); :: deftheorem defines :::"Pappian"::: ANPROJ_2:def 13 : (Bool "for" (Set (Var "IT")) "being" ($#l1_collsp :::"CollProjectiveSpace":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v6_anproj_2 :::"Pappian"::: ) ) "iff" (Bool "for" (Set (Var "o")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "q3")) "," (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "r3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "p2"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "p3"))) & (Bool (Set (Var "p2")) ($#r1_hidden :::"<>"::: ) (Set (Var "p3"))) & (Bool (Set (Var "p1")) ($#r1_hidden :::"<>"::: ) (Set (Var "p2"))) & (Bool (Set (Var "p1")) ($#r1_hidden :::"<>"::: ) (Set (Var "p3"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "q2"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "q3"))) & (Bool (Set (Var "q2")) ($#r1_hidden :::"<>"::: ) (Set (Var "q3"))) & (Bool (Set (Var "q1")) ($#r1_hidden :::"<>"::: ) (Set (Var "q2"))) & (Bool (Set (Var "q1")) ($#r1_hidden :::"<>"::: ) (Set (Var "q3"))) & (Bool (Bool "not" (Set (Var "o")) "," (Set (Var "p1")) "," (Set (Var "q1")) ($#r1_collsp :::"is_collinear"::: ) )) & (Bool (Set (Var "o")) "," (Set (Var "p1")) "," (Set (Var "p2")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "o")) "," (Set (Var "p1")) "," (Set (Var "p3")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "o")) "," (Set (Var "q1")) "," (Set (Var "q2")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "o")) "," (Set (Var "q1")) "," (Set (Var "q3")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p1")) "," (Set (Var "q2")) "," (Set (Var "r3")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "q1")) "," (Set (Var "p2")) "," (Set (Var "r3")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p1")) "," (Set (Var "q3")) "," (Set (Var "r2")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p3")) "," (Set (Var "q1")) "," (Set (Var "r2")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p2")) "," (Set (Var "q3")) "," (Set (Var "r1")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p3")) "," (Set (Var "q2")) "," (Set (Var "r1")) ($#r1_collsp :::"is_collinear"::: ) )) "holds" (Bool (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "r3")) ($#r1_collsp :::"is_collinear"::: ) )) ")" )); definitionlet "IT" be ($#l1_collsp :::"CollProjectiveSpace":::); attr "IT" is :::"2-dimensional"::: means :: ANPROJ_2:def 14 (Bool "for" (Set (Var "p")) "," (Set (Var "p1")) "," (Set (Var "q")) "," (Set (Var "q1")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool "(" (Bool (Set (Var "p")) "," (Set (Var "p1")) "," (Set (Var "r")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "q")) "," (Set (Var "q1")) "," (Set (Var "r")) ($#r1_collsp :::"is_collinear"::: ) ) ")" ))); end; :: deftheorem defines :::"2-dimensional"::: ANPROJ_2:def 14 : (Bool "for" (Set (Var "IT")) "being" ($#l1_collsp :::"CollProjectiveSpace":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v7_anproj_2 :::"2-dimensional"::: ) ) "iff" (Bool "for" (Set (Var "p")) "," (Set (Var "p1")) "," (Set (Var "q")) "," (Set (Var "q1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool "(" (Bool (Set (Var "p")) "," (Set (Var "p1")) "," (Set (Var "r")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "q")) "," (Set (Var "q1")) "," (Set (Var "r")) ($#r1_collsp :::"is_collinear"::: ) ) ")" ))) ")" )); notationlet "IT" be ($#l1_collsp :::"CollProjectiveSpace":::); antonym :::"up-3-dimensional"::: "IT" for :::"2-dimensional"::: ; end; definitionlet "IT" be ($#l1_collsp :::"CollProjectiveSpace":::); attr "IT" is :::"at_most-3-dimensional"::: means :: ANPROJ_2:def 15 (Bool "for" (Set (Var "p")) "," (Set (Var "p1")) "," (Set (Var "q")) "," (Set (Var "q1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" (Bool "ex" (Set (Var "r")) "," (Set (Var "r1")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool "(" (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p1")) "," (Set (Var "q1")) "," (Set (Var "r1")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "r2")) "," (Set (Var "r")) "," (Set (Var "r1")) ($#r1_collsp :::"is_collinear"::: ) ) ")" ))); end; :: deftheorem defines :::"at_most-3-dimensional"::: ANPROJ_2:def 15 : (Bool "for" (Set (Var "IT")) "being" ($#l1_collsp :::"CollProjectiveSpace":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v8_anproj_2 :::"at_most-3-dimensional"::: ) ) "iff" (Bool "for" (Set (Var "p")) "," (Set (Var "p1")) "," (Set (Var "q")) "," (Set (Var "q1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) (Bool "ex" (Set (Var "r")) "," (Set (Var "r1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool "(" (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p1")) "," (Set (Var "q1")) "," (Set (Var "r1")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "r2")) "," (Set (Var "r")) "," (Set (Var "r1")) ($#r1_collsp :::"is_collinear"::: ) ) ")" ))) ")" )); theorem :: ANPROJ_2:26 (Bool "for" (Set (Var "V")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "r2")) "," (Set (Var "q")) "," (Set (Var "r1")) "," (Set (Var "q1")) "," (Set (Var "p")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_anproj_1 :::"ProjectiveSpace"::: ) (Set (Var "V")) ")" ) "st" (Bool (Bool (Set (Var "p1")) "," (Set (Var "r2")) "," (Set (Var "q")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "r1")) "," (Set (Var "q1")) "," (Set (Var "q")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p1")) "," (Set (Var "r1")) "," (Set (Var "p")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "r2")) "," (Set (Var "q1")) "," (Set (Var "p")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p1")) "," (Set (Var "q1")) "," (Set (Var "r")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "r2")) "," (Set (Var "r1")) "," (Set (Var "r")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Bool "not" (Set (Var "p1")) "," (Set (Var "r2")) "," (Set (Var "q1")) ($#r1_collsp :::"is_collinear"::: ) )) & (Bool (Bool "not" (Set (Var "p1")) "," (Set (Var "r2")) "," (Set (Var "r1")) ($#r1_collsp :::"is_collinear"::: ) )) & (Bool (Bool "not" (Set (Var "p1")) "," (Set (Var "r1")) "," (Set (Var "q1")) ($#r1_collsp :::"is_collinear"::: ) ))) "holds" (Bool (Set (Var "r2")) "," (Set (Var "r1")) "," (Set (Var "q1")) ($#r1_collsp :::"is_collinear"::: ) ))) ; registrationlet "V" be ($#v1_anproj_2 :::"up-3-dimensional"::: ) ($#l1_rlvect_1 :::"RealLinearSpace":::); cluster (Set ($#k5_anproj_1 :::"ProjectiveSpace"::: ) "V") -> ($#v4_anproj_2 :::"Fanoian"::: ) ($#v5_anproj_2 :::"Desarguesian"::: ) ($#v6_anproj_2 :::"Pappian"::: ) ; end; theorem :: ANPROJ_2:27 (Bool "for" (Set (Var "V")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_rlvect_1 :::"RealLinearSpace":::) "st" (Bool (Bool "ex" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w")) ")" )))) ")" ) ")" ))) "holds" (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_anproj_1 :::"ProjectiveSpace"::: ) (Set (Var "V")) ")" ) "st" (Bool "(" (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2"))) & (Bool "(" "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_anproj_1 :::"ProjectiveSpace"::: ) (Set (Var "V")) ")" ) (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_anproj_1 :::"ProjectiveSpace"::: ) (Set (Var "V")) ")" ) "st" (Bool "(" (Bool (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "q")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "q")) ($#r1_collsp :::"is_collinear"::: ) ) ")" )) ")" ) ")" ))) ; theorem :: ANPROJ_2:28 (Bool "for" (Set (Var "V")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_rlvect_1 :::"RealLinearSpace":::) "st" (Bool (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_anproj_1 :::"ProjectiveSpace"::: ) (Set (Var "V")) ")" ) "st" (Bool "(" (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2"))) & (Bool "(" "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_anproj_1 :::"ProjectiveSpace"::: ) (Set (Var "V")) ")" ) (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_anproj_1 :::"ProjectiveSpace"::: ) (Set (Var "V")) ")" ) "st" (Bool "(" (Bool (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "q")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "q")) ($#r1_collsp :::"is_collinear"::: ) ) ")" )) ")" ) ")" ))) "holds" (Bool "for" (Set (Var "p")) "," (Set (Var "p1")) "," (Set (Var "q")) "," (Set (Var "q1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_anproj_1 :::"ProjectiveSpace"::: ) (Set (Var "V")) ")" ) (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_anproj_1 :::"ProjectiveSpace"::: ) (Set (Var "V")) ")" ) "st" (Bool "(" (Bool (Set (Var "p")) "," (Set (Var "p1")) "," (Set (Var "r")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "q")) "," (Set (Var "q1")) "," (Set (Var "r")) ($#r1_collsp :::"is_collinear"::: ) ) ")" )))) ; theorem :: ANPROJ_2:29 (Bool "for" (Set (Var "V")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_rlvect_1 :::"RealLinearSpace":::) "st" (Bool (Bool "ex" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w")) ")" )))) ")" ) ")" ))) "holds" (Bool "ex" (Set (Var "CS")) "being" ($#l1_collsp :::"CollProjectiveSpace":::) "st" (Bool "(" (Bool (Set (Var "CS")) ($#r1_hidden :::"="::: ) (Set ($#k5_anproj_1 :::"ProjectiveSpace"::: ) (Set (Var "V")))) & (Bool (Set (Var "CS")) "is" ($#v7_anproj_2 :::"2-dimensional"::: ) ) ")" ))) ; theorem :: ANPROJ_2:30 (Bool "for" (Set (Var "V")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_rlvect_1 :::"RealLinearSpace":::) "st" (Bool (Bool "ex" (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool "(" "for" (Set (Var "w1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "a1")) "," (Set (Var "b1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Var "w1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "y")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a1")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b1")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w")) ")" )))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "a1")) "," (Set (Var "b1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "y")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a1")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b1")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ) ")" ))) "holds" (Bool "ex" (Set (Var "p")) "," (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_anproj_1 :::"ProjectiveSpace"::: ) (Set (Var "V")) ")" ) "st" (Bool "(" (Bool (Bool "not" (Set (Var "p")) "," (Set (Var "q1")) "," (Set (Var "q2")) ($#r1_collsp :::"is_collinear"::: ) )) & (Bool "(" "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_anproj_1 :::"ProjectiveSpace"::: ) (Set (Var "V")) ")" ) (Bool "ex" (Set (Var "q3")) "," (Set (Var "r3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_anproj_1 :::"ProjectiveSpace"::: ) (Set (Var "V")) ")" ) "st" (Bool "(" (Bool (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "r3")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "q3")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p")) "," (Set (Var "r3")) "," (Set (Var "q3")) ($#r1_collsp :::"is_collinear"::: ) ) ")" )) ")" ) ")" ))) ; theorem :: ANPROJ_2:31 (Bool "for" (Set (Var "V")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_rlvect_1 :::"RealLinearSpace":::) "st" (Bool (Bool (Set ($#k5_anproj_1 :::"ProjectiveSpace"::: ) (Set (Var "V"))) "is" ($#v4_collsp :::"proper"::: ) ) & (Bool (Set ($#k5_anproj_1 :::"ProjectiveSpace"::: ) (Set (Var "V"))) "is" ($#v3_anproj_2 :::"at_least_3rank"::: ) ) & (Bool "ex" (Set (Var "p")) "," (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_anproj_1 :::"ProjectiveSpace"::: ) (Set (Var "V")) ")" ) "st" (Bool "(" (Bool (Bool "not" (Set (Var "p")) "," (Set (Var "q1")) "," (Set (Var "q2")) ($#r1_collsp :::"is_collinear"::: ) )) & (Bool "(" "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_anproj_1 :::"ProjectiveSpace"::: ) (Set (Var "V")) ")" ) (Bool "ex" (Set (Var "q3")) "," (Set (Var "r3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_anproj_1 :::"ProjectiveSpace"::: ) (Set (Var "V")) ")" ) "st" (Bool "(" (Bool (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "r3")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "q3")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p")) "," (Set (Var "r3")) "," (Set (Var "q3")) ($#r1_collsp :::"is_collinear"::: ) ) ")" )) ")" ) ")" ))) "holds" (Bool "ex" (Set (Var "CS")) "being" ($#l1_collsp :::"CollProjectiveSpace":::) "st" (Bool "(" (Bool (Set (Var "CS")) ($#r1_hidden :::"="::: ) (Set ($#k5_anproj_1 :::"ProjectiveSpace"::: ) (Set (Var "V")))) & (Bool (Set (Var "CS")) "is" ($#v8_anproj_2 :::"at_most-3-dimensional"::: ) ) ")" ))) ; theorem :: ANPROJ_2:32 (Bool "for" (Set (Var "V")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_rlvect_1 :::"RealLinearSpace":::) "st" (Bool (Bool "ex" (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool "(" "for" (Set (Var "w1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "c1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Var "w1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "y")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "c1")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w")) ")" )))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "a1")) "," (Set (Var "b1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "y")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a1")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b1")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ) ")" ))) "holds" (Bool "ex" (Set (Var "CS")) "being" ($#l1_collsp :::"CollProjectiveSpace":::) "st" (Bool "(" (Bool (Set (Var "CS")) ($#r1_hidden :::"="::: ) (Set ($#k5_anproj_1 :::"ProjectiveSpace"::: ) (Set (Var "V")))) & (Bool (Set (Var "CS")) "is" ($#v8_anproj_2 :::"at_most-3-dimensional"::: ) ) ")" ))) ; theorem :: ANPROJ_2:33 (Bool "for" (Set (Var "V")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_rlvect_1 :::"RealLinearSpace":::) "st" (Bool (Bool "ex" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "v1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "a1")) "," (Set (Var "b1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a1")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u1")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b1")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v1")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )))) "holds" (Bool "ex" (Set (Var "CS")) "being" ($#l1_collsp :::"CollProjectiveSpace":::) "st" (Bool "(" (Bool (Set (Var "CS")) ($#r1_hidden :::"="::: ) (Set ($#k5_anproj_1 :::"ProjectiveSpace"::: ) (Set (Var "V")))) & (Bool (Bool "not" (Set (Var "CS")) "is" ($#v7_anproj_2 :::"2-dimensional"::: ) )) ")" ))) ; theorem :: ANPROJ_2:34 (Bool "for" (Set (Var "V")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_rlvect_1 :::"RealLinearSpace":::) "st" (Bool (Bool "ex" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "v1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool "(" "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "a1")) "," (Set (Var "b1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a1")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u1")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b1")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v1")) ")" )))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "a1")) "," (Set (Var "b1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a1")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u1")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b1")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v1")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ) ")" ))) "holds" (Bool "ex" (Set (Var "CS")) "being" ($#l1_collsp :::"CollProjectiveSpace":::) "st" (Bool "(" (Bool (Set (Var "CS")) ($#r1_hidden :::"="::: ) (Set ($#k5_anproj_1 :::"ProjectiveSpace"::: ) (Set (Var "V")))) & (Bool (Set (Var "CS")) "is" ($#v7_anproj_2 :::"up-3-dimensional"::: ) ) & (Bool (Set (Var "CS")) "is" ($#v8_anproj_2 :::"at_most-3-dimensional"::: ) ) ")" ))) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_collsp :::"strict"::: ) ($#v2_collsp :::"reflexive"::: ) ($#v3_collsp :::"transitive"::: ) ($#v4_collsp :::"proper"::: ) ($#v2_anproj_2 :::"Vebleian"::: ) ($#v3_anproj_2 :::"at_least_3rank"::: ) ($#v4_anproj_2 :::"Fanoian"::: ) ($#v5_anproj_2 :::"Desarguesian"::: ) ($#v6_anproj_2 :::"Pappian"::: ) ($#v7_anproj_2 :::"2-dimensional"::: ) for ($#l1_collsp :::"CollStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_collsp :::"strict"::: ) ($#v2_collsp :::"reflexive"::: ) ($#v3_collsp :::"transitive"::: ) ($#v4_collsp :::"proper"::: ) ($#v2_anproj_2 :::"Vebleian"::: ) ($#v3_anproj_2 :::"at_least_3rank"::: ) ($#v4_anproj_2 :::"Fanoian"::: ) ($#v5_anproj_2 :::"Desarguesian"::: ) ($#v6_anproj_2 :::"Pappian"::: ) ($#v7_anproj_2 :::"up-3-dimensional"::: ) ($#v8_anproj_2 :::"at_most-3-dimensional"::: ) for ($#l1_collsp :::"CollStr"::: ) ; end; definitionmode CollProjectivePlane is ($#v7_anproj_2 :::"2-dimensional"::: ) ($#l1_collsp :::"CollProjectiveSpace":::); end; theorem :: ANPROJ_2:35 (Bool "for" (Set (Var "CS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_collsp :::"CollStr"::: ) "holds" (Bool "(" (Bool (Set (Var "CS")) "is" ($#v7_anproj_2 :::"2-dimensional"::: ) ($#l1_collsp :::"CollProjectiveSpace":::)) "iff" (Bool "(" (Bool (Set (Var "CS")) "is" ($#v4_collsp :::"proper"::: ) ($#v3_anproj_2 :::"at_least_3rank"::: ) ($#l1_collsp :::"CollSp":::)) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "p1")) "," (Set (Var "q")) "," (Set (Var "q1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "CS")) (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "CS")) "st" (Bool "(" (Bool (Set (Var "p")) "," (Set (Var "p1")) "," (Set (Var "r")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "q")) "," (Set (Var "q1")) "," (Set (Var "r")) ($#r1_collsp :::"is_collinear"::: ) ) ")" )) ")" ) ")" ) ")" )) ;