:: REAL_1  semantic presentation begin  registration
cluster   ->   ($#v1_xreal_0 :::"real"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ); 
end; definitionmode Real is    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ); end; registration
cluster bbbadV1_XCMPLX_0()   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v2_xxreal_0 :::"positive"::: )     ($#v1_xreal_0 :::"real"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ); 
end; definitionlet "x" be   ($#m1_subset_1 :::"Real":::); :: original: :::"-"::: redefine func  :::"-"::: "x" ->   ($#m1_subset_1 :::"Real":::); :: original: :::"""::: redefine func "x" :::""":::  ->   ($#m1_subset_1 :::"Real":::); end; definitionlet "x" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; let "y" be   ($#m1_subset_1 :::"Real":::); :: original: :::"+"::: redefine func "x" :::"+"::: "y" ->   ($#m1_subset_1 :::"Real":::); :: original: :::"*"::: redefine func "x" :::"*"::: "y" ->   ($#m1_subset_1 :::"Real":::); :: original: :::"-"::: redefine func "x" :::"-"::: "y" ->   ($#m1_subset_1 :::"Real":::); :: original: :::"/"::: redefine func "x" :::"/"::: "y" ->   ($#m1_subset_1 :::"Real":::); end; definitionlet "x" be   ($#m1_subset_1 :::"Real":::); let "y" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; :: original: :::"+"::: redefine func "x" :::"+"::: "y" ->   ($#m1_subset_1 :::"Real":::); :: original: :::"*"::: redefine func "x" :::"*"::: "y" ->   ($#m1_subset_1 :::"Real":::); :: original: :::"-"::: redefine func "x" :::"-"::: "y" ->   ($#m1_subset_1 :::"Real":::); :: original: :::"/"::: redefine func "x" :::"/"::: "y" ->   ($#m1_subset_1 :::"Real":::); end; 




theorem :: REAL_1:1 (Bool (Set   ($#k2_arytm_2 :::"REAL+"::: )  )  ($#r1_hidden :::"="::: )   "{"  (Set (Var "r")) where r "is"   ($#m1_subset_1 :::"Real":::) : (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r")))  "}"  ) ;