:: ANALOAF semantic presentation begin definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "u", "v", "w", "y" be ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Const "V")); pred "u" "," "v" :::"//"::: "w" "," "y" means :: ANALOAF:def 1 (Bool "(" (Bool "u" ($#r1_hidden :::"="::: ) "v") "or" (Bool "w" ($#r1_hidden :::"="::: ) "y") "or" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "a"))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b"))) & (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" "v" ($#k5_algstr_0 :::"-"::: ) "u" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" "y" ($#k5_algstr_0 :::"-"::: ) "w" ")" ))) ")" )) ")" ); end; :: deftheorem defines :::"//"::: ANALOAF:def 1 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r1_analoaf :::"//"::: ) (Set (Var "w")) "," (Set (Var "y"))) "iff" (Bool "(" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Var "v"))) "or" (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) "or" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "a"))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b"))) & (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "u")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "w")) ")" ))) ")" )) ")" ) ")" ))); theorem :: ANALOAF:1 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "w")) "," (Set (Var "v")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" (Set (Var "w")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "v")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "u")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "w")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "u")))))) ; theorem :: ANALOAF:2 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Set (Var "y")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "u"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "w"))))) "holds" (Bool (Set (Set (Var "y")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "u")))))) ; theorem :: ANALOAF:3 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "u")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "v")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "u")) ")" ) ")" )))))) ; theorem :: ANALOAF:4 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k9_real_1 :::"-"::: ) (Set (Var "b")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "u")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "v")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b")) ($#k9_real_1 :::"-"::: ) (Set (Var "a")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "u")) ")" )))))) ; theorem :: ANALOAF:5 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u"))) ($#r1_hidden :::"="::: ) (Set (Var "v")))) "holds" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k2_real_1 :::"""::: ) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v"))))))) ; theorem :: ANALOAF:6 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u"))) ($#r1_hidden :::"="::: ) (Set (Var "v")))) "implies" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k2_real_1 :::"""::: ) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")))) ")" & "(" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k2_real_1 :::"""::: ) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v"))))) "implies" (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u"))) ($#r1_hidden :::"="::: ) (Set (Var "v"))) ")" ")" )))) ; theorem :: ANALOAF:7 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r1_analoaf :::"//"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "v"))) & (Bool (Set (Var "w")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "u")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "w")) ")" ))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "a"))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b"))) ")" )))) ; theorem :: ANALOAF:8 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r1_analoaf :::"//"::: ) (Set (Var "u")) "," (Set (Var "v"))))) ; theorem :: ANALOAF:9 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r1_analoaf :::"//"::: ) (Set (Var "w")) "," (Set (Var "w"))) & (Bool (Set (Var "u")) "," (Set (Var "u")) ($#r1_analoaf :::"//"::: ) (Set (Var "v")) "," (Set (Var "w"))) ")" ))) ; theorem :: ANALOAF:10 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r1_analoaf :::"//"::: ) (Set (Var "v")) "," (Set (Var "u")))) "holds" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Var "v"))))) ; theorem :: ANALOAF:11 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q"))) & (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r1_analoaf :::"//"::: ) (Set (Var "u")) "," (Set (Var "v"))) & (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r1_analoaf :::"//"::: ) (Set (Var "w")) "," (Set (Var "y")))) "holds" (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r1_analoaf :::"//"::: ) (Set (Var "w")) "," (Set (Var "y"))))) ; theorem :: ANALOAF:12 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r1_analoaf :::"//"::: ) (Set (Var "w")) "," (Set (Var "y")))) "holds" (Bool "(" (Bool (Set (Var "v")) "," (Set (Var "u")) ($#r1_analoaf :::"//"::: ) (Set (Var "y")) "," (Set (Var "w"))) & (Bool (Set (Var "w")) "," (Set (Var "y")) ($#r1_analoaf :::"//"::: ) (Set (Var "u")) "," (Set (Var "v"))) ")" ))) ; theorem :: ANALOAF:13 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r1_analoaf :::"//"::: ) (Set (Var "v")) "," (Set (Var "w")))) "holds" (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r1_analoaf :::"//"::: ) (Set (Var "u")) "," (Set (Var "w"))))) ; theorem :: ANALOAF:14 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool "(" "not" (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r1_analoaf :::"//"::: ) (Set (Var "u")) "," (Set (Var "w"))) "or" (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r1_analoaf :::"//"::: ) (Set (Var "v")) "," (Set (Var "w"))) "or" (Bool (Set (Var "u")) "," (Set (Var "w")) ($#r1_analoaf :::"//"::: ) (Set (Var "w")) "," (Set (Var "v"))) ")" ))) ; theorem :: ANALOAF:15 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "," (Set (Var "u")) "," (Set (Var "y")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "u"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "w"))))) "holds" (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r1_analoaf :::"//"::: ) (Set (Var "w")) "," (Set (Var "y"))))) ; theorem :: ANALOAF:16 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "y")) "," (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "w")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "u"))))) "holds" (Bool "(" (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r1_analoaf :::"//"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "w")) ($#r1_analoaf :::"//"::: ) (Set (Var "v")) "," (Set (Var "y"))) ")" ))) ; theorem :: ANALOAF:17 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) "st" (Bool (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q"))))) "holds" (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r1_analoaf :::"//"::: ) (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "w")) ($#r1_analoaf :::"//"::: ) (Set (Var "v")) "," (Set (Var "y"))) & (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) ")" )))) ; theorem :: ANALOAF:18 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "p")) "," (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "v"))) & (Bool (Set (Var "v")) "," (Set (Var "p")) ($#r1_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "w")))) "holds" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "u")) "," (Set (Var "p")) ($#r1_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "y"))) & (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r1_analoaf :::"//"::: ) (Set (Var "w")) "," (Set (Var "y"))) ")" )))) ; theorem :: ANALOAF:19 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (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 "(" (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "v"))) & (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) & (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) ")" ))) ; theorem :: ANALOAF:20 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) "st" (Bool (Bool "ex" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "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 "ex" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Bool "not" (Set (Var "u")) "," (Set (Var "v")) ($#r1_analoaf :::"//"::: ) (Set (Var "w")) "," (Set (Var "y")))) & (Bool (Bool "not" (Set (Var "u")) "," (Set (Var "v")) ($#r1_analoaf :::"//"::: ) (Set (Var "y")) "," (Set (Var "w")))) ")" ))) ; theorem :: ANALOAF:21 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) "st" (Bool (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "w"))))))) "holds" (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Bool "not" (Set (Var "u")) "," (Set (Var "v")) ($#r1_analoaf :::"//"::: ) (Set (Var "w")) "," (Set (Var "y")))) & (Bool (Bool "not" (Set (Var "u")) "," (Set (Var "v")) ($#r1_analoaf :::"//"::: ) (Set (Var "y")) "," (Set (Var "w"))))) "holds" (Bool "ex" (Set (Var "z")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool "(" (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r1_analoaf :::"//"::: ) (Set (Var "u")) "," (Set (Var "z"))) "or" (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r1_analoaf :::"//"::: ) (Set (Var "z")) "," (Set (Var "u"))) ")" ) & (Bool "(" (Bool (Set (Var "w")) "," (Set (Var "y")) ($#r1_analoaf :::"//"::: ) (Set (Var "w")) "," (Set (Var "z"))) "or" (Bool (Set (Var "w")) "," (Set (Var "y")) ($#r1_analoaf :::"//"::: ) (Set (Var "z")) "," (Set (Var "w"))) ")" ) ")" )))) ; definitionattr "c1" is :::"strict"::: ; struct :::"AffinStruct"::: -> ($#l1_struct_0 :::"1-sorted"::: ) ; aggr :::"AffinStruct":::(# :::"carrier":::, :::"CONGR"::: #) -> ($#l1_analoaf :::"AffinStruct"::: ) ; sel :::"CONGR"::: "c1" -> ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1") ($#k2_zfmisc_1 :::":]"::: ) ); end; registration cluster ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v1_analoaf :::"strict"::: ) for ($#l1_analoaf :::"AffinStruct"::: ) ; end; definitionlet "AS" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) ; let "a", "b", "c", "d" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "AS")); pred "a" "," "b" :::"//"::: "c" "," "d" means :: ANALOAF:def 2 (Bool (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) "a" "," "b" ($#k1_domain_1 :::"]"::: ) ) "," (Set ($#k1_domain_1 :::"["::: ) "c" "," "d" ($#k1_domain_1 :::"]"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_analoaf :::"CONGR"::: ) "of" "AS")); end; :: deftheorem defines :::"//"::: ANALOAF:def 2 : (Bool "for" (Set (Var "AS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) "iff" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_domain_1 :::"]"::: ) ) "," (Set ($#k1_domain_1 :::"["::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k1_domain_1 :::"]"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_analoaf :::"CONGR"::: ) "of" (Set (Var "AS")))) ")" ))); definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); func :::"DirPar"::: "V" -> ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") ($#k2_zfmisc_1 :::":]"::: ) ) means :: ANALOAF:def 3 (Bool "for" (Set (Var "x")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" "V" "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "u")) "," (Set (Var "v")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "w")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r1_analoaf :::"//"::: ) (Set (Var "w")) "," (Set (Var "y"))) ")" )) ")" )); end; :: deftheorem defines :::"DirPar"::: ANALOAF:def 3 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_analoaf :::"DirPar"::: ) (Set (Var "V")))) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "ex" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "u")) "," (Set (Var "v")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "w")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r1_analoaf :::"//"::: ) (Set (Var "w")) "," (Set (Var "y"))) ")" )) ")" )) ")" ))); theorem :: ANALOAF:22 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "u")) "," (Set (Var "v")) ($#k1_domain_1 :::"]"::: ) ) "," (Set ($#k1_domain_1 :::"["::: ) (Set (Var "w")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_analoaf :::"DirPar"::: ) (Set (Var "V")))) "iff" (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r1_analoaf :::"//"::: ) (Set (Var "w")) "," (Set (Var "y"))) ")" ))) ; definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); func :::"OASpace"::: "V" -> ($#v1_analoaf :::"strict"::: ) ($#l1_analoaf :::"AffinStruct"::: ) equals :: ANALOAF:def 4 (Set ($#g1_analoaf :::"AffinStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "(" ($#k1_analoaf :::"DirPar"::: ) "V" ")" ) "#)" ); end; :: deftheorem defines :::"OASpace"::: ANALOAF:def 4 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) "holds" (Bool (Set ($#k2_analoaf :::"OASpace"::: ) (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Set ($#g1_analoaf :::"AffinStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set "(" ($#k1_analoaf :::"DirPar"::: ) (Set (Var "V")) ")" ) "#)" ))); registrationlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); cluster (Set ($#k2_analoaf :::"OASpace"::: ) "V") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_analoaf :::"strict"::: ) ; end; theorem :: ANALOAF:23 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) "st" (Bool (Bool "ex" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "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 "(" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_analoaf :::"OASpace"::: ) (Set (Var "V")) ")" ) "st" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_analoaf :::"OASpace"::: ) (Set (Var "V")) ")" ) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "c"))) & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "a")))) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" & "(" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "r")) "," (Set (Var "s")))) "implies" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "r")) "," (Set (Var "s"))) ")" & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) "implies" (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "d")) "," (Set (Var "c"))) ")" & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "c")))) "implies" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "c"))) ")" & (Bool "(" "not" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "c"))) "or" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "c"))) "or" (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "b"))) ")" ) ")" ) ")" ) & (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_analoaf :::"OASpace"::: ) (Set (Var "V")) ")" ) "st" (Bool "(" (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) & (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "d")) "," (Set (Var "c")))) ")" )) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_analoaf :::"OASpace"::: ) (Set (Var "V")) ")" ) (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_analoaf :::"OASpace"::: ) (Set (Var "V")) ")" ) "st" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "d"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "d"))) ")" )) ")" ) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_analoaf :::"OASpace"::: ) (Set (Var "V")) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) "," (Set (Var "p")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "c")))) "holds" (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_analoaf :::"OASpace"::: ) (Set (Var "V")) ")" ) "st" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "p")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) ")" )) ")" ) ")" )) ; theorem :: ANALOAF:24 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) "st" (Bool (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "w"))))))) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_analoaf :::"OASpace"::: ) (Set (Var "V")) ")" ) "st" (Bool (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) & (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "d")) "," (Set (Var "c"))))) "holds" (Bool "ex" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_analoaf :::"OASpace"::: ) (Set (Var "V")) ")" ) "st" (Bool "(" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "t"))) "or" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "t")) "," (Set (Var "a"))) ")" ) & (Bool "(" (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "t"))) "or" (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r2_analoaf :::"//"::: ) (Set (Var "t")) "," (Set (Var "c"))) ")" ) ")" )))) ; definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) ; attr "IT" is :::"OAffinSpace-like"::: means :: ANALOAF:def 5 (Bool "(" (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "c"))) & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "a")))) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" & "(" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "r")) "," (Set (Var "s")))) "implies" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "r")) "," (Set (Var "s"))) ")" & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) "implies" (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "d")) "," (Set (Var "c"))) ")" & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "c")))) "implies" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "c"))) ")" & (Bool "(" "not" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "c"))) "or" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "c"))) "or" (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "b"))) ")" ) ")" ) ")" ) & (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool "(" (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) & (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "d")) "," (Set (Var "c")))) ")" )) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "d"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "d"))) ")" )) ")" ) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) "," (Set (Var "p")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "c")))) "holds" (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "p")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"OAffinSpace-like"::: ANALOAF:def 5 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_analoaf :::"OAffinSpace-like"::: ) ) "iff" (Bool "(" (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "c"))) & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "a")))) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" & "(" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "r")) "," (Set (Var "s")))) "implies" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "r")) "," (Set (Var "s"))) ")" & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) "implies" (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "d")) "," (Set (Var "c"))) ")" & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "c")))) "implies" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "c"))) ")" & (Bool "(" "not" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "c"))) "or" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "c"))) "or" (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "b"))) ")" ) ")" ) ")" ) & (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool "(" (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) & (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "d")) "," (Set (Var "c")))) ")" )) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "d"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "d"))) ")" )) ")" ) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) "," (Set (Var "p")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "c")))) "holds" (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "p")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) ")" )) ")" ) ")" ) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v1_analoaf :::"strict"::: ) ($#v2_analoaf :::"OAffinSpace-like"::: ) for ($#l1_analoaf :::"AffinStruct"::: ) ; end; definitionmode OAffinSpace is ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v2_analoaf :::"OAffinSpace-like"::: ) ($#l1_analoaf :::"AffinStruct"::: ) ; end; theorem :: ANALOAF:25 (Bool "for" (Set (Var "AS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) "holds" (Bool "(" (Bool "(" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "c"))) & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "a")))) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" & "(" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "r")) "," (Set (Var "s")))) "implies" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "r")) "," (Set (Var "s"))) ")" & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) "implies" (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "d")) "," (Set (Var "c"))) ")" & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "c")))) "implies" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "c"))) ")" & (Bool "(" "not" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "c"))) "or" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "c"))) "or" (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "b"))) ")" ) ")" ) ")" ) & (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) & (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "d")) "," (Set (Var "c")))) ")" )) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "d"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "d"))) ")" )) ")" ) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) "," (Set (Var "p")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "c")))) "holds" (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "p")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) ")" )) ")" ) ")" ) "iff" (Bool (Set (Var "AS")) "is" ($#l1_analoaf :::"OAffinSpace":::)) ")" )) ; theorem :: ANALOAF:26 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) "st" (Bool (Bool "ex" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "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 ($#k2_analoaf :::"OASpace"::: ) (Set (Var "V"))) "is" ($#l1_analoaf :::"OAffinSpace":::))) ; definitionlet "IT" be ($#l1_analoaf :::"OAffinSpace":::); attr "IT" is :::"2-dimensional"::: means :: ANALOAF:def 6 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) & (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "d")) "," (Set (Var "c"))))) "holds" (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool "(" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "p"))) "or" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "a"))) ")" ) & (Bool "(" (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "p"))) "or" (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "c"))) ")" ) ")" ))); end; :: deftheorem defines :::"2-dimensional"::: ANALOAF:def 6 : (Bool "for" (Set (Var "IT")) "being" ($#l1_analoaf :::"OAffinSpace":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_analoaf :::"2-dimensional"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) & (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "d")) "," (Set (Var "c"))))) "holds" (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool "(" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "p"))) "or" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "a"))) ")" ) & (Bool "(" (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "p"))) "or" (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "c"))) ")" ) ")" ))) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v1_analoaf :::"strict"::: ) ($#v2_analoaf :::"OAffinSpace-like"::: ) ($#v3_analoaf :::"2-dimensional"::: ) for ($#l1_analoaf :::"AffinStruct"::: ) ; end; definitionmode OAffinPlane is ($#v3_analoaf :::"2-dimensional"::: ) ($#l1_analoaf :::"OAffinSpace":::); end; theorem :: ANALOAF:27 (Bool "for" (Set (Var "AS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) "holds" (Bool "(" (Bool "(" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "c"))) & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "a")))) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" & "(" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "r")) "," (Set (Var "s")))) "implies" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_analoaf :::"//"::: ) (Set (Var "r")) "," (Set (Var "s"))) ")" & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) "implies" (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "d")) "," (Set (Var "c"))) ")" & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "c")))) "implies" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "c"))) ")" & (Bool "(" "not" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "c"))) "or" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "c"))) "or" (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "b"))) ")" ) ")" ) ")" ) & (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) & (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "d")) "," (Set (Var "c")))) ")" )) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "d"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "d"))) ")" )) ")" ) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) "," (Set (Var "p")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "c")))) "holds" (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "p")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) ")" )) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) & (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "d")) "," (Set (Var "c"))))) "holds" (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "p"))) "or" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "a"))) ")" ) & (Bool "(" (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "p"))) "or" (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "c"))) ")" ) ")" )) ")" ) ")" ) "iff" (Bool (Set (Var "AS")) "is" ($#l1_analoaf :::"OAffinPlane":::)) ")" )) ; theorem :: ANALOAF:28 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) "st" (Bool (Bool "ex" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "(" (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"::: ) )) ")" ) ")" ) & (Bool "(" "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" )))) ")" ) ")" ))) "holds" (Bool (Set ($#k2_analoaf :::"OASpace"::: ) (Set (Var "V"))) "is" ($#l1_analoaf :::"OAffinPlane":::))) ;