:: BROUWER  semantic presentation begin  









definitionlet "S", "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); func  :::"DiffElems":::  "(" "S" "," "T" ")"  ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) "S" "," "T" ($#k2_borsuk_1 :::":]"::: ) ) equals :: BROUWER:def 1  "{"  (Set  ($#k4_borsuk_1 :::"["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k4_borsuk_1 :::"]"::: ) ) where s "is"   ($#m1_subset_1 :::"Point":::) "of" "S", t "is"   ($#m1_subset_1 :::"Point":::) "of" "T" : (Bool (Set (Var "s"))  ($#r1_hidden :::"<>"::: )  (Set (Var "t")))  "}"  ; end; 






:: deftheorem    defines :::"DiffElems"::: BROUWER:def 1 :  (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#k1_brouwer :::"DiffElems"::: )   "(" (Set (Var "S")) "," (Set (Var "T")) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k4_borsuk_1 :::"["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k4_borsuk_1 :::"]"::: ) ) where s "is"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")), t "is"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) : (Bool (Set (Var "s"))  ($#r1_hidden :::"<>"::: )  (Set (Var "t")))  "}"  )); 
 
theorem :: BROUWER:1 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_brouwer :::"DiffElems"::: )   "(" (Set (Var "S")) "," (Set (Var "T")) ")" )) "iff" (Bool  "ex" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S"))(Bool  "ex" (Set (Var "t")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_borsuk_1 :::"["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k4_borsuk_1 :::"]"::: ) )) & (Bool (Set (Var "s"))  ($#r1_hidden :::"<>"::: )  (Set (Var "t")))  ")" )))  ")" ))) ; 
 registrationlet "S" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_pre_topc :::"TopSpace":::); let "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); 
cluster (Set   ($#k1_brouwer :::"DiffElems"::: )   "(" "S" "," "T" ")" ) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; registrationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); let "T" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_pre_topc :::"TopSpace":::); 
cluster (Set   ($#k1_brouwer :::"DiffElems"::: )   "(" "S" "," "T" ")" ) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; 
theorem :: BROUWER:2 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "holds"  (Bool (Set   ($#k2_topreal9 :::"cl_Ball"::: )   "(" (Set (Var "x")) "," (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )))) ; 
 definitionlet "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "x" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); let "r" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; func  :::"Tdisk":::  "(" "x" "," "r" ")"  ->    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set   ($#k15_euclid :::"TOP-REAL"::: )  "n") equals :: BROUWER:def 2 (Set (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" )  ($#k1_pre_topc :::"|"::: )  (Set  "("  ($#k2_topreal9 :::"cl_Ball"::: )   "(" "x" "," "r" ")"  ")" )); end; 







:: deftheorem    defines :::"Tdisk"::: BROUWER:def 2 :  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k2_brouwer :::"Tdisk"::: )   "(" (Set (Var "x")) "," (Set (Var "r")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  ($#k1_pre_topc :::"|"::: )  (Set  "("  ($#k2_topreal9 :::"cl_Ball"::: )   "(" (Set (Var "x")) "," (Set (Var "r")) ")"  ")" )))))); 
 registrationlet "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "x" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); let "r" be  ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k2_brouwer :::"Tdisk"::: )   "(" "x" "," "r" ")" ) ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )  ; 
end; 
theorem :: BROUWER:3 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "holds"  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k2_brouwer :::"Tdisk"::: )   "(" (Set (Var "x")) "," (Set (Var "r")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_topreal9 :::"cl_Ball"::: )   "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))))) ; 
 registrationlet "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "x" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); let "r" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k2_brouwer :::"Tdisk"::: )   "(" "x" "," "r" ")" ) ->   ($#v1_topalg_2 :::"convex"::: )   ; 
end; 











theorem :: BROUWER:4 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "r")) "being"  ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "s"))  ($#r1_hidden :::"<>"::: )  (Set (Var "t"))) & (Bool (Set (Var "s")) "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k2_brouwer :::"Tdisk"::: )   "(" (Set (Var "x")) "," (Set (Var "r")) ")"  ")" )) & (Bool (Set (Var "s")) "is" (Bool  "not"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k7_toprealb :::"Tcircle"::: )   "(" (Set (Var "x")) "," (Set (Var "r")) ")"  ")" )))) "holds"  (Bool  "ex" (Set (Var "e")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k7_toprealb :::"Tcircle"::: )   "(" (Set (Var "x")) "," (Set (Var "r")) ")"  ")" ) "st" (Bool (Set  ($#k1_tarski :::"{"::: ) (Set (Var "e")) ($#k1_tarski :::"}"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_topreal9 :::"halfline"::: )   "(" (Set (Var "s")) "," (Set (Var "t")) ")"  ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k3_topreal9 :::"Sphere"::: )   "(" (Set (Var "x")) "," (Set (Var "r")) ")"  ")" ))))))) ; 
 
theorem :: BROUWER:5 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "r")) "being"  ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "s"))  ($#r1_hidden :::"<>"::: )  (Set (Var "t"))) & (Bool (Set (Var "s"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k7_toprealb :::"Tcircle"::: )   "(" (Set (Var "x")) "," (Set (Var "r")) ")"  ")" ))) & (Bool (Set (Var "t")) "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k2_brouwer :::"Tdisk"::: )   "(" (Set (Var "x")) "," (Set (Var "r")) ")"  ")" ))) "holds"  (Bool  "ex" (Set (Var "e")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k7_toprealb :::"Tcircle"::: )   "(" (Set (Var "x")) "," (Set (Var "r")) ")"  ")" ) "st"  (Bool  "("  (Bool (Set (Var "e"))  ($#r1_hidden :::"<>"::: )  (Set (Var "s"))) & (Bool (Set  ($#k2_tarski :::"{"::: ) (Set (Var "s")) "," (Set (Var "e")) ($#k2_tarski :::"}"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_topreal9 :::"halfline"::: )   "(" (Set (Var "s")) "," (Set (Var "t")) ")"  ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k3_topreal9 :::"Sphere"::: )   "(" (Set (Var "x")) "," (Set (Var "r")) ")"  ")" )))  ")" ))))) ; 
 definitionlet "n" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "o" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); let "s", "t" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); let "r" be  ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; assume that  
(Bool (Set (Const "s")) "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k2_brouwer :::"Tdisk"::: )   "(" (Set (Const "o")) "," (Set (Const "r")) ")"  ")" ))
 and  
(Bool (Set (Const "t")) "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k2_brouwer :::"Tdisk"::: )   "(" (Set (Const "o")) "," (Set (Const "r")) ")"  ")" ))
 and  
(Bool (Set (Const "s"))  ($#r1_hidden :::"<>"::: )  (Set (Const "t")))
 ; func  :::"HC":::  "(" "s" "," "t" "," "o" "," "r" ")"  ->   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" ) means :: BROUWER:def 3 (Bool  "("  (Bool it  ($#r2_hidden :::"in"::: )  (Set (Set  "("  ($#k4_topreal9 :::"halfline"::: )   "(" "s" "," "t" ")"  ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k3_topreal9 :::"Sphere"::: )   "(" "o" "," "r" ")"  ")" ))) & (Bool it  ($#r1_hidden :::"<>"::: )  "s")  ")" ); end; 










:: deftheorem    defines :::"HC"::: BROUWER:def 3 :  (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "o")) "," (Set (Var "s")) "," (Set (Var "t")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "r")) "being"  ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "s")) "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k2_brouwer :::"Tdisk"::: )   "(" (Set (Var "o")) "," (Set (Var "r")) ")"  ")" )) & (Bool (Set (Var "t")) "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k2_brouwer :::"Tdisk"::: )   "(" (Set (Var "o")) "," (Set (Var "r")) ")"  ")" )) & (Bool (Set (Var "s"))  ($#r1_hidden :::"<>"::: )  (Set (Var "t")))) "holds"  (Bool  "for" (Set (Var "b6")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b6"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_brouwer :::"HC"::: )   "(" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "o")) "," (Set (Var "r")) ")" )) "iff" (Bool  "("  (Bool (Set (Var "b6"))  ($#r2_hidden :::"in"::: )  (Set (Set  "("  ($#k4_topreal9 :::"halfline"::: )   "(" (Set (Var "s")) "," (Set (Var "t")) ")"  ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k3_topreal9 :::"Sphere"::: )   "(" (Set (Var "o")) "," (Set (Var "r")) ")"  ")" ))) & (Bool (Set (Var "b6"))  ($#r1_hidden :::"<>"::: )  (Set (Var "s")))  ")" )  ")" ))))); 
 








theorem :: BROUWER:6 (Bool  "for" (Set (Var "r")) "being"  ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "s")) "," (Set (Var "o")) "," (Set (Var "t")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "s")) "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k2_brouwer :::"Tdisk"::: )   "(" (Set (Var "o")) "," (Set (Var "r")) ")"  ")" )) & (Bool (Set (Var "t")) "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k2_brouwer :::"Tdisk"::: )   "(" (Set (Var "o")) "," (Set (Var "r")) ")"  ")" )) & (Bool (Set (Var "s"))  ($#r1_hidden :::"<>"::: )  (Set (Var "t")))) "holds"  (Bool (Set   ($#k3_brouwer :::"HC"::: )   "(" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "o")) "," (Set (Var "r")) ")" ) "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k7_toprealb :::"Tcircle"::: )   "(" (Set (Var "o")) "," (Set (Var "r")) ")"  ")" ))))) ; 
 
theorem :: BROUWER:7 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "r")) "being"  ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "o")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "," (Set (Var "O")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "n")))  "st" (Bool (Bool (Set (Var "S"))  ($#r1_hidden :::"="::: )  (Set (Var "s"))) & (Bool (Set (Var "T"))  ($#r1_hidden :::"="::: )  (Set (Var "t"))) & (Bool (Set (Var "O"))  ($#r1_hidden :::"="::: )  (Set (Var "o"))) & (Bool (Set (Var "s")) "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k2_brouwer :::"Tdisk"::: )   "(" (Set (Var "o")) "," (Set (Var "r")) ")"  ")" )) & (Bool (Set (Var "t")) "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k2_brouwer :::"Tdisk"::: )   "(" (Set (Var "o")) "," (Set (Var "r")) ")"  ")" )) & (Bool (Set (Var "s"))  ($#r1_hidden :::"<>"::: )  (Set (Var "t"))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  ($#k23_rvsum_1 :::"|("::: ) (Set  "(" (Set (Var "t"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "s")) ")" ) "," (Set  "(" (Set (Var "s"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "o")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Set  "(" (Set  ($#k23_rvsum_1 :::"|("::: ) (Set  "(" (Set (Var "t"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "s")) ")" ) "," (Set  "(" (Set (Var "s"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "o")) ")" ) ($#k23_rvsum_1 :::")|"::: ) )  ($#k5_square_1 :::"^2"::: )  ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k18_rvsum_1 :::"Sum"::: )  (Set  "("  ($#k11_euclid :::"sqr"::: )  (Set  "(" (Set (Var "T"))  ($#k8_euclid :::"-"::: )  (Set (Var "S")) ")" ) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k18_rvsum_1 :::"Sum"::: )  (Set  "("  ($#k11_euclid :::"sqr"::: )  (Set  "(" (Set (Var "S"))  ($#k8_euclid :::"-"::: )  (Set (Var "O")) ")" ) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "r"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" ) ")" ) ")" ) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "("  ($#k18_rvsum_1 :::"Sum"::: )  (Set  "("  ($#k11_euclid :::"sqr"::: )  (Set  "(" (Set (Var "T"))  ($#k8_euclid :::"-"::: )  (Set (Var "S")) ")" ) ")" ) ")" )))) "holds"  (Bool (Set   ($#k3_brouwer :::"HC"::: )   "(" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "o")) "," (Set (Var "r")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 1)  ($#k9_real_1 :::"-"::: )  (Set (Var "a")) ")" )  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "s")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "a"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "t")) ")" )))))))) ; 
 
theorem :: BROUWER:8 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "r")) "being"  ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "o")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "s")) "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k2_brouwer :::"Tdisk"::: )   "(" (Set (Var "o")) "," (Set (Var "r")) ")"  ")" )) & (Bool (Set (Var "t")) "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k2_brouwer :::"Tdisk"::: )   "(" (Set (Var "o")) "," (Set (Var "r")) ")"  ")" )) & (Bool (Set (Var "s"))  ($#r1_hidden :::"<>"::: )  (Set (Var "t"))) & (Bool (Set (Var "r1"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "t"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "s"))  ($#k17_euclid :::"`1"::: )  ")" ))) & (Bool (Set (Var "r2"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "t"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "s"))  ($#k18_euclid :::"`2"::: )  ")" ))) & (Bool (Set (Var "s1"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "s"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "o"))  ($#k17_euclid :::"`1"::: )  ")" ))) & (Bool (Set (Var "s2"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "s"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "o"))  ($#k18_euclid :::"`2"::: )  ")" ))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Set (Var "s1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "r1")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "s2"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "r2")) ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set (Var "s1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "r1")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "s2"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "r2")) ")" ) ")" )  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "r1"))  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "r2"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "s1"))  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "s2"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "r"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" ) ")" ) ")" ) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set  "(" (Set (Var "r1"))  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "r2"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" )))) "holds"  (Bool (Set   ($#k3_brouwer :::"HC"::: )   "(" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "o")) "," (Set (Var "r")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set  "(" (Set  "(" (Set (Var "s"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "r1")) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "s"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "r2")) ")" ) ")" ) ($#k19_euclid :::"]|"::: ) )))))) ; 
 definitionlet "n" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "o" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); let "r" be  ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; let "x" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k2_brouwer :::"Tdisk"::: )   "(" (Set (Const "o")) "," (Set (Const "r")) ")"  ")" ); let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k2_brouwer :::"Tdisk"::: )   "(" (Set (Const "o")) "," (Set (Const "r")) ")"  ")" ) "," (Set  "("  ($#k2_brouwer :::"Tdisk"::: )   "(" (Set (Const "o")) "," (Set (Const "r")) ")"  ")" ); assume 
(Bool (Bool  "not" (Set (Const "x"))  ($#r2_abian :::"is_a_fixpoint_of"::: )  (Set (Const "f"))))
 ; func  :::"HC":::  "(" "x" "," "f" ")"  ->   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k7_toprealb :::"Tcircle"::: )   "(" "o" "," "r" ")"  ")" ) means :: BROUWER:def 4 (Bool  "ex" (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" ) "st"  (Bool  "("  (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  "x") & (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set "f"  ($#k3_funct_2 :::"."::: )  "x")) & (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k3_brouwer :::"HC"::: )   "(" (Set (Var "z")) "," (Set (Var "y")) "," "o" "," "r" ")" ))  ")" )); end; 










:: deftheorem    defines :::"HC"::: BROUWER:def 4 :  (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "r")) "being"  ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k2_brouwer :::"Tdisk"::: )   "(" (Set (Var "o")) "," (Set (Var "r")) ")"  ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k2_brouwer :::"Tdisk"::: )   "(" (Set (Var "o")) "," (Set (Var "r")) ")"  ")" ) "," (Set  "("  ($#k2_brouwer :::"Tdisk"::: )   "(" (Set (Var "o")) "," (Set (Var "r")) ")"  ")" )  "st" (Bool (Bool (Bool  "not" (Set (Var "x"))  ($#r2_abian :::"is_a_fixpoint_of"::: )  (Set (Var "f"))))) "holds"  (Bool  "for" (Set (Var "b6")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k7_toprealb :::"Tcircle"::: )   "(" (Set (Var "o")) "," (Set (Var "r")) ")"  ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b6"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_brouwer :::"HC"::: )   "(" (Set (Var "x")) "," (Set (Var "f")) ")" )) "iff" (Bool  "ex" (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "st"  (Bool  "("  (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Var "x"))) & (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))) & (Bool (Set (Var "b6"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_brouwer :::"HC"::: )   "(" (Set (Var "z")) "," (Set (Var "y")) "," (Set (Var "o")) "," (Set (Var "r")) ")" ))  ")" ))  ")" ))))))); 
 
theorem :: BROUWER:9 (Bool  "for" (Set (Var "r")) "being"  ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k2_brouwer :::"Tdisk"::: )   "(" (Set (Var "o")) "," (Set (Var "r")) ")"  ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k2_brouwer :::"Tdisk"::: )   "(" (Set (Var "o")) "," (Set (Var "r")) ")"  ")" ) "," (Set  "("  ($#k2_brouwer :::"Tdisk"::: )   "(" (Set (Var "o")) "," (Set (Var "r")) ")"  ")" )  "st" (Bool (Bool (Bool  "not" (Set (Var "x"))  ($#r2_abian :::"is_a_fixpoint_of"::: )  (Set (Var "f")))) & (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k7_toprealb :::"Tcircle"::: )   "(" (Set (Var "o")) "," (Set (Var "r")) ")"  ")" ))) "holds"  (Bool (Set   ($#k4_brouwer :::"HC"::: )   "(" (Set (Var "x")) "," (Set (Var "f")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "x")))))))) ; 
 
theorem :: BROUWER:10 (Bool  "for" (Set (Var "r")) "being"   ($#v2_xxreal_0 :::"positive"::: )     ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "Y")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set   ($#k2_brouwer :::"Tdisk"::: )   "(" (Set (Var "o")) "," (Set (Var "r")) ")" )  "st" (Bool (Bool (Set (Var "Y"))  ($#r1_hidden :::"="::: )  (Set   ($#k7_toprealb :::"Tcircle"::: )   "(" (Set (Var "o")) "," (Set (Var "r")) ")" ))) "holds"  (Bool  "not" (Bool (Set (Var "Y"))  ($#r1_borsuk_1 :::"is_a_retract_of"::: )  (Set   ($#k2_brouwer :::"Tdisk"::: )   "(" (Set (Var "o")) "," (Set (Var "r")) ")" )))))) ; 
 definitionlet "n" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "r" be  ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; let "o" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k2_brouwer :::"Tdisk"::: )   "(" (Set (Const "o")) "," (Set (Const "r")) ")"  ")" ) "," (Set  "("  ($#k2_brouwer :::"Tdisk"::: )   "(" (Set (Const "o")) "," (Set (Const "r")) ")"  ")" ); func  :::"BR-map"::: "f" ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k2_brouwer :::"Tdisk"::: )   "(" "o" "," "r" ")"  ")" ) "," (Set  "("  ($#k7_toprealb :::"Tcircle"::: )   "(" "o" "," "r" ")"  ")" ) means :: BROUWER:def 5 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k2_brouwer :::"Tdisk"::: )   "(" "o" "," "r" ")"  ")" ) "holds"  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_brouwer :::"HC"::: )   "(" (Set (Var "x")) "," "f" ")" ))); end; 








:: deftheorem    defines :::"BR-map"::: BROUWER:def 5 :  (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "r")) "being"  ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k2_brouwer :::"Tdisk"::: )   "(" (Set (Var "o")) "," (Set (Var "r")) ")"  ")" ) "," (Set  "("  ($#k2_brouwer :::"Tdisk"::: )   "(" (Set (Var "o")) "," (Set (Var "r")) ")"  ")" )  (Bool  "for" (Set (Var "b5")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k2_brouwer :::"Tdisk"::: )   "(" (Set (Var "o")) "," (Set (Var "r")) ")"  ")" ) "," (Set  "("  ($#k7_toprealb :::"Tcircle"::: )   "(" (Set (Var "o")) "," (Set (Var "r")) ")"  ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_brouwer :::"BR-map"::: )  (Set (Var "f")))) "iff" (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k2_brouwer :::"Tdisk"::: )   "(" (Set (Var "o")) "," (Set (Var "r")) ")"  ")" ) "holds"  (Bool (Set (Set (Var "b5"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_brouwer :::"HC"::: )   "(" (Set (Var "x")) "," (Set (Var "f")) ")" )))  ")" )))))); 
 
theorem :: BROUWER:11 (Bool  "for" (Set (Var "r")) "being"  ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k2_brouwer :::"Tdisk"::: )   "(" (Set (Var "o")) "," (Set (Var "r")) ")"  ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k2_brouwer :::"Tdisk"::: )   "(" (Set (Var "o")) "," (Set (Var "r")) ")"  ")" ) "," (Set  "("  ($#k2_brouwer :::"Tdisk"::: )   "(" (Set (Var "o")) "," (Set (Var "r")) ")"  ")" )  "st" (Bool (Bool (Bool  "not" (Set (Var "x"))  ($#r2_abian :::"is_a_fixpoint_of"::: )  (Set (Var "f")))) & (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k7_toprealb :::"Tcircle"::: )   "(" (Set (Var "o")) "," (Set (Var "r")) ")"  ")" ))) "holds"  (Bool (Set (Set  "("  ($#k5_brouwer :::"BR-map"::: )  (Set (Var "f")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "x")))))))) ; 
 
theorem :: BROUWER:12 (Bool  "for" (Set (Var "r")) "being"  ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k2_brouwer :::"Tdisk"::: )   "(" (Set (Var "o")) "," (Set (Var "r")) ")"  ")" ) "," (Set  "("  ($#k2_brouwer :::"Tdisk"::: )   "(" (Set (Var "o")) "," (Set (Var "r")) ")"  ")" )  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v2_abian :::"without_fixpoints"::: )  )) "holds"  (Bool (Set (Set  "("  ($#k5_brouwer :::"BR-map"::: )  (Set (Var "f")) ")" )  ($#k2_partfun1 :::"|"::: )  (Set  "("  ($#k3_topreal9 :::"Sphere"::: )   "(" (Set (Var "o")) "," (Set (Var "r")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_struct_0 :::"id"::: )  (Set  "("  ($#k7_toprealb :::"Tcircle"::: )   "(" (Set (Var "o")) "," (Set (Var "r")) ")"  ")" ))))))) ; 
 
theorem :: BROUWER:13 (Bool  "for" (Set (Var "r")) "being"   ($#v2_xxreal_0 :::"positive"::: )     ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k2_brouwer :::"Tdisk"::: )   "(" (Set (Var "o")) "," (Set (Var "r")) ")"  ")" ) "," (Set  "("  ($#k2_brouwer :::"Tdisk"::: )   "(" (Set (Var "o")) "," (Set (Var "r")) ")"  ")" )  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v2_abian :::"without_fixpoints"::: )  )) "holds"  (Bool (Set   ($#k5_brouwer :::"BR-map"::: )  (Set (Var "f"))) "is"   ($#v5_pre_topc :::"continuous"::: )  )))) ; 
 
theorem :: BROUWER:14 (Bool  "for" (Set (Var "r")) "being"  ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k2_brouwer :::"Tdisk"::: )   "(" (Set (Var "o")) "," (Set (Var "r")) ")"  ")" ) "," (Set  "("  ($#k2_brouwer :::"Tdisk"::: )   "(" (Set (Var "o")) "," (Set (Var "r")) ")"  ")" ) "holds"  (Bool (Set (Var "f")) "is"   ($#v2_abian :::"with_fixpoint"::: )  )))) ; 
 
theorem :: BROUWER:15 (Bool  "for" (Set (Var "r")) "being"  ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k2_brouwer :::"Tdisk"::: )   "(" (Set (Var "o")) "," (Set (Var "r")) ")"  ")" ) "," (Set  "("  ($#k2_brouwer :::"Tdisk"::: )   "(" (Set (Var "o")) "," (Set (Var "r")) ")"  ")" ) (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k2_brouwer :::"Tdisk"::: )   "(" (Set (Var "o")) "," (Set (Var "r")) ")"  ")" ) "st" (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "x"))))))) ;