:: AXIOMS  semantic presentation begin  




















theorem :: AXIOMS:1 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y")))) "holds"  (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y")))  ")" )) "holds"  (Bool  "ex" (Set (Var "z")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y")))) "holds"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "z"))) & (Bool (Set (Var "z"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y")))  ")" )))) ; 
 
theorem :: AXIOMS:2 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k5_numbers :::"NAT"::: )  )) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k5_numbers :::"NAT"::: )  ))) "holds"  (Bool (Set (Set (Var "x"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "y")))  ($#r2_hidden :::"in"::: )  (Set   ($#k5_numbers :::"NAT"::: )  ))) ; 
 
theorem :: AXIOMS:3 (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))  ")" )) "holds"  (Bool (Set   ($#k5_numbers :::"NAT"::: )  )  ($#r1_tarski :::"c="::: )  (Set (Var "A")))) ; 
 
theorem :: AXIOMS:4 (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "i")) where i "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "k")))  "}"  )) ;