:: RUSUB_5 semantic presentation begin definitionlet "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; let "M", "N" be ($#v2_rusub_4 :::"Affine"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); pred "M" :::"is_parallel_to"::: "N" means :: RUSUB_5:def 1 (Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" "V" "st" (Bool "M" ($#r1_hidden :::"="::: ) (Set "N" ($#k6_rusub_4 :::"+"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) )))); end; :: deftheorem defines :::"is_parallel_to"::: RUSUB_5:def 1 : (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#v2_rusub_4 :::"Affine"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "M")) ($#r1_rusub_5 :::"is_parallel_to"::: ) (Set (Var "N"))) "iff" (Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set (Set (Var "N")) ($#k6_rusub_4 :::"+"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) )))) ")" ))); theorem :: RUSUB_5:1 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "M")) "being" ($#v2_rusub_4 :::"Affine"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool (Set (Var "M")) ($#r1_rusub_5 :::"is_parallel_to"::: ) (Set (Var "M"))))) ; theorem :: RUSUB_5:2 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#v2_rusub_4 :::"Affine"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "M")) ($#r1_rusub_5 :::"is_parallel_to"::: ) (Set (Var "N")))) "holds" (Bool (Set (Var "N")) ($#r1_rusub_5 :::"is_parallel_to"::: ) (Set (Var "M"))))) ; theorem :: RUSUB_5:3 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "M")) "," (Set (Var "L")) "," (Set (Var "N")) "being" ($#v2_rusub_4 :::"Affine"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "M")) ($#r1_rusub_5 :::"is_parallel_to"::: ) (Set (Var "L"))) & (Bool (Set (Var "L")) ($#r1_rusub_5 :::"is_parallel_to"::: ) (Set (Var "N")))) "holds" (Bool (Set (Var "M")) ($#r1_rusub_5 :::"is_parallel_to"::: ) (Set (Var "N"))))) ; definitionlet "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "M", "N" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); func "M" :::"-"::: "N" -> ($#m1_subset_1 :::"Subset":::) "of" "V" equals :: RUSUB_5:def 2 "{" (Set "(" (Set (Var "u")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "v")) ")" ) where u, v "is" ($#m1_subset_1 :::"Element":::) "of" "V" : (Bool "(" (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) "M") & (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) "N") ")" ) "}" ; end; :: deftheorem defines :::"-"::: RUSUB_5:def 2 : (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "M")) ($#k1_rusub_5 :::"-"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "u")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "v")) ")" ) where u, v "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) : (Bool "(" (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) ")" ) "}" ))); theorem :: RUSUB_5:4 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#v2_rusub_4 :::"Affine"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "M")) ($#k1_rusub_5 :::"-"::: ) (Set (Var "N"))) "is" ($#v2_rusub_4 :::"Affine"::: ) ))) ; theorem :: RUSUB_5:5 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool "(" (Bool (Set (Var "M")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "N")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) "holds" (Bool (Set (Set (Var "M")) ($#k6_rusub_4 :::"+"::: ) (Set (Var "N"))) "is" ($#v1_xboole_0 :::"empty"::: ) ))) ; theorem :: RUSUB_5:6 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool (Bool "not" (Set (Set (Var "M")) ($#k6_rusub_4 :::"+"::: ) (Set (Var "N"))) "is" ($#v1_xboole_0 :::"empty"::: ) )))) ; theorem :: RUSUB_5:7 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool "(" (Bool (Set (Var "M")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "N")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) "holds" (Bool (Set (Set (Var "M")) ($#k1_rusub_5 :::"-"::: ) (Set (Var "N"))) "is" ($#v1_xboole_0 :::"empty"::: ) ))) ; theorem :: RUSUB_5:8 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool (Bool "not" (Set (Set (Var "M")) ($#k1_rusub_5 :::"-"::: ) (Set (Var "N"))) "is" ($#v1_xboole_0 :::"empty"::: ) )))) ; theorem :: RUSUB_5:9 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set (Set (Var "N")) ($#k7_rusub_4 :::"+"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ))) "iff" (Bool (Set (Set (Var "M")) ($#k1_rusub_5 :::"-"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "N"))) ")" )))) ; theorem :: RUSUB_5:10 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set (Set (Var "M")) ($#k7_rusub_4 :::"+"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "M")) ($#k7_rusub_4 :::"+"::: ) (Set (Var "N"))))))) ; theorem :: RUSUB_5:11 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set (Set (Var "M")) ($#k1_rusub_5 :::"-"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "M")) ($#k1_rusub_5 :::"-"::: ) (Set (Var "N"))))))) ; theorem :: RUSUB_5:12 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "M")) ($#k1_rusub_5 :::"-"::: ) (Set (Var "M")))))) ; theorem :: RUSUB_5:13 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_rusub_4 :::"Affine"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "M")) "is" ($#v3_rusub_4 :::"Subspace-like"::: ) ) & (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) "holds" (Bool (Set (Set (Var "M")) ($#k7_rusub_4 :::"+"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_tarski :::"c="::: ) (Set (Var "M")))))) ; theorem :: RUSUB_5:14 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "M")) "," (Set (Var "N1")) "," (Set (Var "N2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_rusub_4 :::"Affine"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "N1")) "is" ($#v3_rusub_4 :::"Subspace-like"::: ) ) & (Bool (Set (Var "N2")) "is" ($#v3_rusub_4 :::"Subspace-like"::: ) ) & (Bool (Set (Var "M")) ($#r1_rusub_5 :::"is_parallel_to"::: ) (Set (Var "N1"))) & (Bool (Set (Var "M")) ($#r1_rusub_5 :::"is_parallel_to"::: ) (Set (Var "N2")))) "holds" (Bool (Set (Var "N1")) ($#r1_hidden :::"="::: ) (Set (Var "N2"))))) ; theorem :: RUSUB_5:15 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_rusub_4 :::"Affine"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) "holds" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "M")) ($#k1_rusub_5 :::"-"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) )))))) ; theorem :: RUSUB_5:16 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_rusub_4 :::"Affine"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) "holds" (Bool "ex" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_rusub_4 :::"Affine"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "N")) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k1_rusub_5 :::"-"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ))) & (Bool (Set (Var "M")) ($#r1_rusub_5 :::"is_parallel_to"::: ) (Set (Var "N"))) & (Bool (Set (Var "N")) "is" ($#v3_rusub_4 :::"Subspace-like"::: ) ) ")" ))))) ; theorem :: RUSUB_5:17 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_rusub_4 :::"Affine"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) "holds" (Bool (Set (Set (Var "M")) ($#k1_rusub_5 :::"-"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k1_rusub_5 :::"-"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "u")) ($#k6_domain_1 :::"}"::: ) )))))) ; theorem :: RUSUB_5:18 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_rusub_4 :::"Affine"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "M")) ($#k1_rusub_5 :::"-"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" (Set (Var "M")) ($#k1_rusub_5 :::"-"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" ) where v "is" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) : (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) "}" )))) ; theorem :: RUSUB_5:19 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_rusub_4 :::"Affine"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) "holds" (Bool (Set (Set (Var "M")) ($#k1_rusub_5 :::"-"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" (Set (Var "M")) ($#k1_rusub_5 :::"-"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "u")) ($#k6_domain_1 :::"}"::: ) ) ")" ) where u "is" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) : (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) "}" ))))) ; theorem :: RUSUB_5:20 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_rusub_4 :::"Affine"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "ex" (Set (Var "L")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_rusub_4 :::"Affine"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "L")) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k1_rusub_5 :::"-"::: ) (Set (Var "M")))) & (Bool (Set (Var "L")) "is" ($#v3_rusub_4 :::"Subspace-like"::: ) ) & (Bool (Set (Var "M")) ($#r1_rusub_5 :::"is_parallel_to"::: ) (Set (Var "L"))) ")" )))) ; begin definitionlet "V" be ($#l1_bhsp_1 :::"RealUnitarySpace":::); let "W" be ($#m1_rusub_1 :::"Subspace"::: ) "of" (Set (Const "V")); func :::"Ort_Comp"::: "W" -> ($#v1_bhsp_1 :::"strict"::: ) ($#m1_rusub_1 :::"Subspace"::: ) "of" "V" means :: RUSUB_5:def 3 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) "{" (Set (Var "v")) where v "is" ($#m1_subset_1 :::"VECTOR":::) "of" "V" : (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" "V" "st" (Bool (Bool (Set (Var "w")) ($#r1_struct_0 :::"in"::: ) "W")) "holds" (Bool (Set (Var "w")) "," (Set (Var "v")) ($#r1_bhsp_1 :::"are_orthogonal"::: ) )) "}" ); end; :: deftheorem defines :::"Ort_Comp"::: RUSUB_5:def 3 : (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "W")) "being" ($#m1_rusub_1 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "b3")) "being" ($#v1_bhsp_1 :::"strict"::: ) ($#m1_rusub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_rusub_5 :::"Ort_Comp"::: ) (Set (Var "W")))) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "v")) where v "is" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) : (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "w")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W")))) "holds" (Bool (Set (Var "w")) "," (Set (Var "v")) ($#r1_bhsp_1 :::"are_orthogonal"::: ) )) "}" ) ")" )))); definitionlet "V" be ($#l1_bhsp_1 :::"RealUnitarySpace":::); let "M" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); func :::"Ort_Comp"::: "M" -> ($#v1_bhsp_1 :::"strict"::: ) ($#m1_rusub_1 :::"Subspace"::: ) "of" "V" means :: RUSUB_5:def 4 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) "{" (Set (Var "v")) where v "is" ($#m1_subset_1 :::"VECTOR":::) "of" "V" : (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" "V" "st" (Bool (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) "M")) "holds" (Bool (Set (Var "w")) "," (Set (Var "v")) ($#r1_bhsp_1 :::"are_orthogonal"::: ) )) "}" ); end; :: deftheorem defines :::"Ort_Comp"::: RUSUB_5:def 4 : (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "b3")) "being" ($#v1_bhsp_1 :::"strict"::: ) ($#m1_rusub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_rusub_5 :::"Ort_Comp"::: ) (Set (Var "M")))) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "v")) where v "is" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) : (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) "holds" (Bool (Set (Var "w")) "," (Set (Var "v")) ($#r1_bhsp_1 :::"are_orthogonal"::: ) )) "}" ) ")" )))); theorem :: RUSUB_5:21 (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "W")) "being" ($#m1_rusub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))) ($#r1_struct_0 :::"in"::: ) (Set ($#k2_rusub_5 :::"Ort_Comp"::: ) (Set (Var "W")))))) ; theorem :: RUSUB_5:22 (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) "holds" (Bool (Set ($#k2_rusub_5 :::"Ort_Comp"::: ) (Set "(" ($#k1_rusub_1 :::"(0)."::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_rusub_1 :::"(Omega)."::: ) (Set (Var "V"))))) ; theorem :: RUSUB_5:23 (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) "holds" (Bool (Set ($#k2_rusub_5 :::"Ort_Comp"::: ) (Set "(" ($#k2_rusub_1 :::"(Omega)."::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_rusub_1 :::"(0)."::: ) (Set (Var "V"))))) ; theorem :: RUSUB_5:24 (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "W")) "being" ($#m1_rusub_1 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) & (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W")))) "holds" (Bool "not" (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set ($#k2_rusub_5 :::"Ort_Comp"::: ) (Set (Var "W")))))))) ; theorem :: RUSUB_5:25 (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool (Set (Var "M")) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k2_rusub_5 :::"Ort_Comp"::: ) (Set "(" ($#k3_rusub_5 :::"Ort_Comp"::: ) (Set (Var "M")) ")" ) ")" ))))) ; theorem :: RUSUB_5:26 (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "M")) ($#r1_tarski :::"c="::: ) (Set (Var "N")))) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k3_rusub_5 :::"Ort_Comp"::: ) (Set (Var "N")) ")" )) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k3_rusub_5 :::"Ort_Comp"::: ) (Set (Var "M")) ")" ))))) ; theorem :: RUSUB_5:27 (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "W")) "being" ($#m1_rusub_1 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W"))))) "holds" (Bool (Set ($#k3_rusub_5 :::"Ort_Comp"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k2_rusub_5 :::"Ort_Comp"::: ) (Set (Var "W"))))))) ; theorem :: RUSUB_5:28 (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k3_rusub_5 :::"Ort_Comp"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k2_rusub_5 :::"Ort_Comp"::: ) (Set "(" ($#k2_rusub_5 :::"Ort_Comp"::: ) (Set "(" ($#k3_rusub_5 :::"Ort_Comp"::: ) (Set (Var "M")) ")" ) ")" ))))) ; theorem :: RUSUB_5:29 (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set ($#k3_bhsp_1 :::"||."::: ) (Set "(" (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_bhsp_1 :::".||"::: ) ) ($#k5_square_1 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k3_bhsp_1 :::"||."::: ) (Set (Var "x")) ($#k3_bhsp_1 :::".||"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "y")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set ($#k3_bhsp_1 :::"||."::: ) (Set (Var "y")) ($#k3_bhsp_1 :::".||"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ))) & (Bool (Set (Set ($#k3_bhsp_1 :::"||."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k3_bhsp_1 :::".||"::: ) ) ($#k5_square_1 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k3_bhsp_1 :::"||."::: ) (Set (Var "x")) ($#k3_bhsp_1 :::".||"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "y")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set ($#k3_bhsp_1 :::"||."::: ) (Set (Var "y")) ($#k3_bhsp_1 :::".||"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ))) ")" ))) ; theorem :: RUSUB_5:30 (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r1_bhsp_1 :::"are_orthogonal"::: ) )) "holds" (Bool (Set (Set ($#k3_bhsp_1 :::"||."::: ) (Set "(" (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_bhsp_1 :::".||"::: ) ) ($#k5_square_1 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k3_bhsp_1 :::"||."::: ) (Set (Var "x")) ($#k3_bhsp_1 :::".||"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set ($#k3_bhsp_1 :::"||."::: ) (Set (Var "y")) ($#k3_bhsp_1 :::".||"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ))))) ; theorem :: RUSUB_5:31 (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" (Set ($#k3_bhsp_1 :::"||."::: ) (Set "(" (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_bhsp_1 :::".||"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set ($#k3_bhsp_1 :::"||."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k3_bhsp_1 :::".||"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k3_bhsp_1 :::"||."::: ) (Set (Var "x")) ($#k3_bhsp_1 :::".||"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k3_bhsp_1 :::"||."::: ) (Set (Var "y")) ($#k3_bhsp_1 :::".||"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ))))) ; theorem :: RUSUB_5:32 (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "ex" (Set (Var "W")) "being" ($#m1_rusub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "u")) where u "is" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) : (Bool (Set (Set (Var "u")) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "}" )))) ; begin definitionlet "V" be ($#l1_bhsp_1 :::"RealUnitarySpace":::); func :::"Family_open_set"::: "V" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "V" means :: RUSUB_5:def 5 (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" "V" "holds" (Bool "(" (Bool (Set (Var "M")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" "V" "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) "holds" (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k4_bhsp_2 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "M"))) ")" ))) ")" )); end; :: deftheorem defines :::"Family_open_set"::: RUSUB_5:def 5 : (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_rusub_5 :::"Family_open_set"::: ) (Set (Var "V")))) "iff" (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "M")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) "holds" (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k4_bhsp_2 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "M"))) ")" ))) ")" )) ")" ))); theorem :: RUSUB_5:33 (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "r")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "p")))) "holds" (Bool (Set ($#k4_bhsp_2 :::"Ball"::: ) "(" (Set (Var "v")) "," (Set (Var "r")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k4_bhsp_2 :::"Ball"::: ) "(" (Set (Var "v")) "," (Set (Var "p")) ")" ))))) ; theorem :: RUSUB_5:34 (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "V")) (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k4_bhsp_2 :::"Ball"::: ) "(" (Set (Var "v")) "," (Set (Var "r")) ")" ) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V")))) ")" )))) ; theorem :: RUSUB_5:35 (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "v")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set ($#k4_bhsp_2 :::"Ball"::: ) "(" (Set (Var "v")) "," (Set (Var "r")) ")" ))) "holds" (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "p")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k4_bhsp_2 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "p")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k4_bhsp_2 :::"Ball"::: ) "(" (Set (Var "v")) "," (Set (Var "r")) ")" )) ")" ))))) ; theorem :: RUSUB_5:36 (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "r")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k4_bhsp_2 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k4_bhsp_2 :::"Ball"::: ) "(" (Set (Var "w")) "," (Set (Var "p")) ")" ")" )))) "holds" (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set ($#k4_bhsp_2 :::"Ball"::: ) "(" (Set (Var "v")) "," (Set (Var "q")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k4_bhsp_2 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" )) & (Bool (Set ($#k4_bhsp_2 :::"Ball"::: ) "(" (Set (Var "v")) "," (Set (Var "q")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k4_bhsp_2 :::"Ball"::: ) "(" (Set (Var "w")) "," (Set (Var "p")) ")" )) ")" ))))) ; theorem :: RUSUB_5:37 (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k4_bhsp_2 :::"Ball"::: ) "(" (Set (Var "v")) "," (Set (Var "r")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k4_rusub_5 :::"Family_open_set"::: ) (Set (Var "V"))))))) ; theorem :: RUSUB_5:38 (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_rusub_5 :::"Family_open_set"::: ) (Set (Var "V"))))) ; theorem :: RUSUB_5:39 (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "M")) ($#r2_hidden :::"in"::: ) (Set ($#k4_rusub_5 :::"Family_open_set"::: ) (Set (Var "V")))) & (Bool (Set (Var "N")) ($#r2_hidden :::"in"::: ) (Set ($#k4_rusub_5 :::"Family_open_set"::: ) (Set (Var "V"))))) "holds" (Bool (Set (Set (Var "M")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "N"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_rusub_5 :::"Family_open_set"::: ) (Set (Var "V")))))) ; theorem :: RUSUB_5:40 (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k4_rusub_5 :::"Family_open_set"::: ) (Set (Var "V"))))) "holds" (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "A"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_rusub_5 :::"Family_open_set"::: ) (Set (Var "V")))))) ; theorem :: RUSUB_5:41 (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) "holds" (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set "(" ($#k4_rusub_5 :::"Family_open_set"::: ) (Set (Var "V")) ")" ) "#)" ) "is" ($#l1_pre_topc :::"TopSpace":::))) ; definitionlet "V" be ($#l1_bhsp_1 :::"RealUnitarySpace":::); func :::"TopUnitSpace"::: "V" -> ($#l1_pre_topc :::"TopStruct"::: ) equals :: RUSUB_5:def 6 (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "(" ($#k4_rusub_5 :::"Family_open_set"::: ) "V" ")" ) "#)" ); end; :: deftheorem defines :::"TopUnitSpace"::: RUSUB_5:def 6 : (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) "holds" (Bool (Set ($#k5_rusub_5 :::"TopUnitSpace"::: ) (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set "(" ($#k4_rusub_5 :::"Family_open_set"::: ) (Set (Var "V")) ")" ) "#)" ))); registrationlet "V" be ($#l1_bhsp_1 :::"RealUnitarySpace":::); cluster (Set ($#k5_rusub_5 :::"TopUnitSpace"::: ) "V") -> ($#v2_pre_topc :::"TopSpace-like"::: ) ; end; registrationlet "V" be ($#l1_bhsp_1 :::"RealUnitarySpace":::); cluster (Set ($#k5_rusub_5 :::"TopUnitSpace"::: ) "V") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; theorem :: RUSUB_5:42 (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k5_rusub_5 :::"TopUnitSpace"::: ) (Set (Var "V")) ")" ) "st" (Bool (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "V"))))) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "M")) "is" ($#v4_pre_topc :::"closed"::: ) ) ")" ))) ; theorem :: RUSUB_5:43 (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k5_rusub_5 :::"TopUnitSpace"::: ) (Set (Var "V")) ")" ) "st" (Bool (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set ($#k1_struct_0 :::"{}"::: ) (Set (Var "V"))))) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "M")) "is" ($#v4_pre_topc :::"closed"::: ) ) ")" ))) ; theorem :: RUSUB_5:44 (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) ($#k6_domain_1 :::"}"::: ) )) & (Bool (Set (Var "r")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k6_bhsp_2 :::"Sphere"::: ) "(" (Set (Var "v")) "," (Set (Var "r")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )))) ; theorem :: RUSUB_5:45 (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) ($#k6_domain_1 :::"}"::: ) )) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "not" (Bool (Set ($#k6_bhsp_2 :::"Sphere"::: ) "(" (Set (Var "v")) "," (Set (Var "r")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))))) ; theorem :: RUSUB_5:46 (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k4_bhsp_2 :::"Ball"::: ) "(" (Set (Var "v")) "," (Set (Var "r")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )))) ; theorem :: RUSUB_5:47 (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) ($#k6_domain_1 :::"}"::: ) )) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k4_bhsp_2 :::"Ball"::: ) "(" (Set (Var "v")) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) ($#k6_domain_1 :::"}"::: ) ))))) ; theorem :: RUSUB_5:48 (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) ($#k6_domain_1 :::"}"::: ) )) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "w")) ($#r1_hidden :::"<>"::: ) (Set (Var "v"))) & (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set ($#k4_bhsp_2 :::"Ball"::: ) "(" (Set (Var "v")) "," (Set (Var "r")) ")" )) ")" ))))) ; theorem :: RUSUB_5:49 (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) "holds" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_rusub_5 :::"TopUnitSpace"::: ) (Set (Var "V")) ")" ))) & (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set "(" ($#k5_rusub_5 :::"TopUnitSpace"::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_rusub_5 :::"Family_open_set"::: ) (Set (Var "V")))) ")" )) ; theorem :: RUSUB_5:50 (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k5_rusub_5 :::"TopUnitSpace"::: ) (Set (Var "V")) ")" ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set ($#k4_bhsp_2 :::"Ball"::: ) "(" (Set (Var "v")) "," (Set (Var "r")) ")" ))) "holds" (Bool (Set (Var "M")) "is" ($#v3_pre_topc :::"open"::: ) ))))) ; theorem :: RUSUB_5:51 (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k5_rusub_5 :::"TopUnitSpace"::: ) (Set (Var "V")) ")" ) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v3_pre_topc :::"open"::: ) ) "iff" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) "holds" (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k4_bhsp_2 :::"Ball"::: ) "(" (Set (Var "v")) "," (Set (Var "r")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "M"))) ")" ))) ")" ))) ; theorem :: RUSUB_5:52 (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "u")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "V"))(Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Set "(" ($#k4_bhsp_2 :::"Ball"::: ) "(" (Set (Var "v1")) "," (Set (Var "r1")) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k4_bhsp_2 :::"Ball"::: ) "(" (Set (Var "v2")) "," (Set (Var "r2")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k4_bhsp_2 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" ))))))) ; theorem :: RUSUB_5:53 (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k5_rusub_5 :::"TopUnitSpace"::: ) (Set (Var "V")) ")" ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set ($#k5_bhsp_2 :::"cl_Ball"::: ) "(" (Set (Var "v")) "," (Set (Var "r")) ")" ))) "holds" (Bool (Set (Var "M")) "is" ($#v4_pre_topc :::"closed"::: ) ))))) ; theorem :: RUSUB_5:54 (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k5_rusub_5 :::"TopUnitSpace"::: ) (Set (Var "V")) ")" ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set ($#k6_bhsp_2 :::"Sphere"::: ) "(" (Set (Var "v")) "," (Set (Var "r")) ")" ))) "holds" (Bool (Set (Var "M")) "is" ($#v4_pre_topc :::"closed"::: ) ))))) ;