:: REAL  semantic presentation begin  





theorem :: REAL:1 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y"))) & (Bool (Set (Var "x")) "is"   ($#v2_xxreal_0 :::"positive"::: )  )) "holds"  (Bool (Set (Var "y")) "is"   ($#v2_xxreal_0 :::"positive"::: )  )) ; 
 
theorem :: REAL:2 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y"))) & (Bool (Set (Var "y")) "is"   ($#v3_xxreal_0 :::"negative"::: )  )) "holds"  (Bool (Set (Var "x")) "is"   ($#v3_xxreal_0 :::"negative"::: )  )) ; 
 
theorem :: REAL:3 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y"))) & (Bool (Bool  "not" (Set (Var "x")) "is"   ($#v3_xxreal_0 :::"negative"::: )  ))) "holds"  (Bool  "not" (Bool (Set (Var "y")) "is"   ($#v3_xxreal_0 :::"negative"::: )  ))) ; 
 
theorem :: REAL:4 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y"))) & (Bool (Bool  "not" (Set (Var "y")) "is"   ($#v2_xxreal_0 :::"positive"::: )  ))) "holds"  (Bool  "not" (Bool (Set (Var "x")) "is"   ($#v2_xxreal_0 :::"positive"::: )  ))) ; 
 
theorem :: REAL:5 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y"))) & (Bool (Bool  "not" (Set (Var "y")) "is"   ($#v1_xboole_0 :::"zero"::: )  )) & (Bool (Bool  "not" (Set (Var "x")) "is"   ($#v3_xxreal_0 :::"negative"::: )  ))) "holds"  (Bool (Set (Var "y")) "is"   ($#v2_xxreal_0 :::"positive"::: )  )) ; 
 
theorem :: REAL:6 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y"))) & (Bool (Bool  "not" (Set (Var "x")) "is"   ($#v1_xboole_0 :::"zero"::: )  )) & (Bool (Bool  "not" (Set (Var "y")) "is"   ($#v2_xxreal_0 :::"positive"::: )  ))) "holds"  (Bool (Set (Var "x")) "is"   ($#v3_xxreal_0 :::"negative"::: )  )) ; 
 
theorem :: REAL:7 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Bool  "not" (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y")))) & (Bool (Bool  "not" (Set (Var "x")) "is"   ($#v2_xxreal_0 :::"positive"::: )  ))) "holds"  (Bool (Set (Var "y")) "is"   ($#v3_xxreal_0 :::"negative"::: )  )) ; 
 
theorem :: REAL:8 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Bool  "not" (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y")))) & (Bool (Bool  "not" (Set (Var "y")) "is"   ($#v3_xxreal_0 :::"negative"::: )  ))) "holds"  (Bool (Set (Var "x")) "is"   ($#v2_xxreal_0 :::"positive"::: )  )) ;