:: RAT_1  semantic presentation begin  






















definitionredefine func  :::"RAT":::  means :: RAT_1:def 1 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "ex" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "n")))))  ")" )); end; 




:: deftheorem    defines :::"RAT"::: RAT_1:def 1 :  (Bool  "for" (Set (Var "b1")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_numbers :::"RAT"::: )  )) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b1"))) "iff" (Bool  "ex" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "n")))))  ")" ))  ")" )); 
 definitionlet "r" be    ($#m1_hidden :::"number"::: )  ; attr "r" is  :::"rational":::  means :: RAT_1:def 2 (Bool "r"  ($#r2_hidden :::"in"::: )  (Set   ($#k3_numbers :::"RAT"::: )  )); end; 




:: deftheorem    defines :::"rational"::: RAT_1:def 2 :  (Bool  "for" (Set (Var "r")) "being"    ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Var "r")) "is"   ($#v1_rat_1 :::"rational"::: )  ) "iff" (Bool (Set (Var "r"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_numbers :::"RAT"::: )  ))  ")" )); 
 registration
cluster   ($#v1_xxreal_0 :::"ext-real"::: )   bbbadV1_XCMPLX_0()   ($#v1_xreal_0 :::"real"::: )     ($#v1_rat_1 :::"rational"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ); 
end; registration
cluster   ($#v1_rat_1 :::"rational"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; definitionmode Rational is   ($#v1_rat_1 :::"rational"::: )     ($#m1_hidden :::"number"::: )  ; end; 
theorem :: RAT_1:1 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_numbers :::"RAT"::: )  ))) "holds"  (Bool  "ex" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Integer":::) "st"  (Bool  "("  (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "n"))))  ")" ))) ; 
 
theorem :: RAT_1:2 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x")) "is"   ($#m1_hidden :::"Rational":::))) "holds"  (Bool  "ex" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Integer":::) "st"  (Bool  "("  (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "n"))))  ")" ))) ; 
 registration
cluster   ($#v1_rat_1 :::"rational"::: )    ->   ($#v1_xreal_0 :::"real"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; 
theorem :: RAT_1:3 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool (Set (Set (Var "m"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "n"))) "is"   ($#v1_rat_1 :::"rational"::: )  )) ; 
 registration
cluster   ($#v1_int_1 :::"integer"::: )    ->   ($#v1_rat_1 :::"rational"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; 



registrationlet "p", "q" be   ($#m1_hidden :::"Rational":::); 
cluster (Set "p"  ($#k3_xcmplx_0 :::"*"::: )  "q") ->   ($#v1_rat_1 :::"rational"::: )   ; 

cluster (Set "p"  ($#k2_xcmplx_0 :::"+"::: )  "q") ->   ($#v1_rat_1 :::"rational"::: )   ; 

cluster (Set "p"  ($#k6_xcmplx_0 :::"-"::: )  "q") ->   ($#v1_rat_1 :::"rational"::: )   ; 

cluster (Set "p"  ($#k7_xcmplx_0 :::"/"::: )  "q") ->   ($#v1_rat_1 :::"rational"::: )   ; 
end; registrationlet "p" be   ($#m1_hidden :::"Rational":::); 
cluster (Set   ($#k4_xcmplx_0 :::"-"::: )  "p") ->   ($#v1_rat_1 :::"rational"::: )   ; 

cluster (Set "p"  ($#k5_xcmplx_0 :::"""::: )  ) ->   ($#v1_rat_1 :::"rational"::: )   ; 
end; 
theorem :: RAT_1:4 canceled; 
 
theorem :: RAT_1:5 canceled; 
 
theorem :: RAT_1:6 canceled; 
 
theorem :: RAT_1:7 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b")))) "holds"  (Bool  "ex" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::) "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "p"))) & (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b")))  ")" ))) ; 
 
theorem :: RAT_1:8 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::) (Bool  "ex" (Set (Var "m")) "being"   ($#m1_hidden :::"Integer":::)(Bool  "ex" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "k"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k6_real_1 :::"/"::: )  (Set (Var "k"))))  ")" )))) ; 
 
theorem :: RAT_1:9 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::) (Bool  "ex" (Set (Var "m")) "being"   ($#m1_hidden :::"Integer":::)(Bool  "ex" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "k"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k6_real_1 :::"/"::: )  (Set (Var "k")))) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Integer":::)  (Bool  "for" (Set (Var "l")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "l"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k6_real_1 :::"/"::: )  (Set (Var "l"))))) "holds"  (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "l"))))  ")" )  ")" )))) ; 
 definitionlet "p" be   ($#m1_hidden :::"Rational":::); func  :::"denominator"::: "p" ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) means :: RAT_1:def 3 (Bool  "("  (Bool it  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool  "ex" (Set (Var "m")) "being"   ($#m1_hidden :::"Integer":::) "st" (Bool "p"  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k6_real_1 :::"/"::: )  it))) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Integer":::)  (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "k"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool "p"  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k6_real_1 :::"/"::: )  (Set (Var "k"))))) "holds"  (Bool it  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))))  ")" )  ")" ); end; 





:: deftheorem    defines :::"denominator"::: RAT_1:def 3 :  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::)  (Bool  "for" (Set (Var "b2")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_rat_1 :::"denominator"::: )  (Set (Var "p")))) "iff" (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool  "ex" (Set (Var "m")) "being"   ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k6_real_1 :::"/"::: )  (Set (Var "b2"))))) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Integer":::)  (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "k"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k6_real_1 :::"/"::: )  (Set (Var "k"))))) "holds"  (Bool (Set (Var "b2"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))))  ")" )  ")" )  ")" ))); 
 definitionlet "p" be   ($#m1_hidden :::"Rational":::); func  :::"numerator"::: "p" ->   ($#m1_hidden :::"Integer":::) equals :: RAT_1:def 4 (Set (Set  "("  ($#k1_rat_1 :::"denominator"::: )  "p" ")" )  ($#k8_real_1 :::"*"::: )  "p"); end; 





:: deftheorem    defines :::"numerator"::: RAT_1:def 4 :  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::) "holds"  (Bool (Set   ($#k2_rat_1 :::"numerator"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_rat_1 :::"denominator"::: )  (Set (Var "p")) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "p"))))); 
 
theorem :: RAT_1:10 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::)  "holds" (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_rat_1 :::"denominator"::: )  (Set (Var "p"))))) ; 
 
theorem :: RAT_1:11 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::) "holds"  (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_rat_1 :::"denominator"::: )  (Set (Var "p"))))) ; 
 
theorem :: RAT_1:12 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::)  "holds" (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "("  ($#k1_rat_1 :::"denominator"::: )  (Set (Var "p")) ")" )  ($#k2_real_1 :::"""::: )  ))) ; 
 
theorem :: RAT_1:13 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::) "holds"  (Bool (Num 1)  ($#r1_xxreal_0 :::">="::: )  (Set (Set  "("  ($#k1_rat_1 :::"denominator"::: )  (Set (Var "p")) ")" )  ($#k2_real_1 :::"""::: )  ))) ; 
 
theorem :: RAT_1:14 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::) "holds"   (Bool  "("  (Bool (Set   ($#k2_rat_1 :::"numerator"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "iff" (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) ; 
 
theorem :: RAT_1:15 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::) "holds"   (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_rat_1 :::"numerator"::: )  (Set (Var "p")) ")" )  ($#k6_real_1 :::"/"::: )  (Set  "("  ($#k1_rat_1 :::"denominator"::: )  (Set (Var "p")) ")" ))) & (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_rat_1 :::"numerator"::: )  (Set (Var "p")) ")" )  ($#k4_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k1_rat_1 :::"denominator"::: )  (Set (Var "p")) ")" )  ($#k2_real_1 :::"""::: )  ")" ))) & (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k1_rat_1 :::"denominator"::: )  (Set (Var "p")) ")" )  ($#k2_real_1 :::"""::: )  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k2_rat_1 :::"numerator"::: )  (Set (Var "p")) ")" )))  ")" )) ; 
 
theorem :: RAT_1:16 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::)  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k1_rat_1 :::"denominator"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_rat_1 :::"numerator"::: )  (Set (Var "p")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "p"))))) ; 
 
theorem :: RAT_1:17 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::)  "st" (Bool (Bool (Set (Var "p")) "is"   ($#m1_hidden :::"Integer":::))) "holds"  (Bool  "("  (Bool (Set   ($#k1_rat_1 :::"denominator"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set   ($#k2_rat_1 :::"numerator"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "p")))  ")" )) ; 
 
theorem :: RAT_1:18 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::)  "st" (Bool (Bool  "("  (Bool (Set   ($#k2_rat_1 :::"numerator"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "p"))) "or" (Bool (Set   ($#k1_rat_1 :::"denominator"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Num 1))  ")" )) "holds"  (Bool (Set (Var "p")) "is"   ($#m1_hidden :::"Integer":::))) ; 
 
theorem :: RAT_1:19 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::) "holds"   (Bool  "("  (Bool (Set   ($#k2_rat_1 :::"numerator"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "p"))) "iff" (Bool (Set   ($#k1_rat_1 :::"denominator"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Num 1))  ")" )) ; 
 
theorem :: RAT_1:20 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::)  "st" (Bool (Bool  "("  (Bool (Set   ($#k2_rat_1 :::"numerator"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "p"))) "or" (Bool (Set   ($#k1_rat_1 :::"denominator"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Num 1))  ")" ) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "p")))) "holds"  (Bool (Set (Var "p")) "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ))) ; 
 
theorem :: RAT_1:21 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::) "holds"   (Bool  "("  (Bool (Num 1)  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_rat_1 :::"denominator"::: )  (Set (Var "p")))) "iff" (Bool  "not" (Bool (Set (Var "p")) "is"   ($#v1_int_1 :::"integer"::: )  ))  ")" )) ; 
 
theorem :: RAT_1:22 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::) "holds"   (Bool  "("  (Bool (Num 1)  ($#r1_xxreal_0 :::">"::: )  (Set (Set  "("  ($#k1_rat_1 :::"denominator"::: )  (Set (Var "p")) ")" )  ($#k2_real_1 :::"""::: )  )) "iff" (Bool  "not" (Bool (Set (Var "p")) "is"   ($#v1_int_1 :::"integer"::: )  ))  ")" )) ; 
 
theorem :: RAT_1:23 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::) "holds"   (Bool  "("  (Bool (Set   ($#k2_rat_1 :::"numerator"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_rat_1 :::"denominator"::: )  (Set (Var "p")))) "iff" (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Num 1))  ")" )) ; 
 
theorem :: RAT_1:24 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::) "holds"   (Bool  "("  (Bool (Set   ($#k2_rat_1 :::"numerator"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "("  ($#k1_rat_1 :::"denominator"::: )  (Set (Var "p")) ")" ))) "iff" (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Num 1)))  ")" )) ; 
 
theorem :: RAT_1:25 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::) "holds"   (Bool  "("  (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "("  ($#k2_rat_1 :::"numerator"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_rat_1 :::"denominator"::: )  (Set (Var "p")))) "iff" (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Num 1)))  ")" )) ; 
 
theorem :: RAT_1:26 (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Integer":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k2_rat_1 :::"numerator"::: )  (Set (Var "p")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "m")) ")" )  ($#k6_real_1 :::"/"::: )  (Set  "(" (Set  "("  ($#k1_rat_1 :::"denominator"::: )  (Set (Var "p")) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "m")) ")" ))))) ; 
 
theorem :: RAT_1:27 (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Integer":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k6_real_1 :::"/"::: )  (Set (Var "k"))))) "holds"  (Bool  "ex" (Set (Var "l")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_rat_1 :::"numerator"::: )  (Set (Var "p")) ")" )  ($#k4_real_1 :::"*"::: )  (Set (Var "l")))) & (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_rat_1 :::"denominator"::: )  (Set (Var "p")) ")" )  ($#k4_nat_1 :::"*"::: )  (Set (Var "l"))))  ")" ))))) ; 
 
theorem :: RAT_1:28 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Integer":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::)  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "n")))) & (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "m1")) "being"   ($#m1_hidden :::"Integer":::) "st"  (Bool  "("  (Bool (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_rat_1 :::"numerator"::: )  (Set (Var "p")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "m1")))) & (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_rat_1 :::"denominator"::: )  (Set (Var "p")) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "m1"))))  ")" )))) ; 
 
theorem :: RAT_1:29 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::)  (Bool  "for" (Set (Var "l")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "holds"  (Bool  "("   "not" (Bool (Num 1)  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "l"))) "or" (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Integer":::)  (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "holds"  (Bool  "("   "not" (Bool (Set   ($#k2_rat_1 :::"numerator"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k4_real_1 :::"*"::: )  (Set (Var "l")))) "or"  "not" (Bool (Set   ($#k1_rat_1 :::"denominator"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k4_nat_1 :::"*"::: )  (Set (Var "l"))))  ")" )))  ")" ))) ; 
 
theorem :: RAT_1:30 (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Integer":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::)  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k6_real_1 :::"/"::: )  (Set (Var "k")))) & (Bool (Set (Var "k"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool  "("   "for" (Set (Var "l")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "holds"  (Bool  "("   "not" (Bool (Num 1)  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "l"))) "or" (Bool  "for" (Set (Var "m1")) "being"   ($#m1_hidden :::"Integer":::)  (Bool  "for" (Set (Var "k1")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "holds"  (Bool  "("   "not" (Bool (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "m1"))  ($#k4_real_1 :::"*"::: )  (Set (Var "l")))) "or"  "not" (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k1"))  ($#k4_nat_1 :::"*"::: )  (Set (Var "l"))))  ")" )))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_rat_1 :::"denominator"::: )  (Set (Var "p")))) & (Bool (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_rat_1 :::"numerator"::: )  (Set (Var "p"))))  ")" )))) ; 
 
theorem :: RAT_1:31 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::) "holds"   (Bool  "("  (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_real_1 :::"-"::: )  (Num 1))) "iff" (Bool (Set   ($#k2_rat_1 :::"numerator"::: )  (Set (Var "p")))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "("  ($#k1_rat_1 :::"denominator"::: )  (Set (Var "p")) ")" )))  ")" )) ; 
 
theorem :: RAT_1:32 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::) "holds"   (Bool  "("  (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Num 1))) "iff" (Bool (Set   ($#k2_rat_1 :::"numerator"::: )  (Set (Var "p")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "("  ($#k1_rat_1 :::"denominator"::: )  (Set (Var "p")) ")" )))  ")" )) ; 
 
theorem :: RAT_1:33 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::) "holds"   (Bool  "("  (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_real_1 :::"-"::: )  (Num 1))) "iff" (Bool (Set   ($#k1_rat_1 :::"denominator"::: )  (Set (Var "p")))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "("  ($#k2_rat_1 :::"numerator"::: )  (Set (Var "p")) ")" )))  ")" )) ; 
 
theorem :: RAT_1:34 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::) "holds"   (Bool  "("  (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Num 1))) "iff" (Bool (Set   ($#k1_rat_1 :::"denominator"::: )  (Set (Var "p")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "("  ($#k2_rat_1 :::"numerator"::: )  (Set (Var "p")) ")" )))  ")" )) ; 
 
theorem :: RAT_1:35 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::) "holds"   (Bool  "("  (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<"::: )  (Num 1)) "iff" (Bool (Set   ($#k2_rat_1 :::"numerator"::: )  (Set (Var "p")))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_rat_1 :::"denominator"::: )  (Set (Var "p"))))  ")" )) ; 
 
theorem :: RAT_1:36 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::) "holds"   (Bool  "("  (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<="::: )  (Num 1)) "iff" (Bool (Set   ($#k2_rat_1 :::"numerator"::: )  (Set (Var "p")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_rat_1 :::"denominator"::: )  (Set (Var "p"))))  ")" )) ; 
 
theorem :: RAT_1:37 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::) "holds"   (Bool  "("  (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) "iff" (Bool (Set   ($#k2_rat_1 :::"numerator"::: )  (Set (Var "p")))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) ; 
 
theorem :: RAT_1:38 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::) "holds"   (Bool  "("  (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "iff" (Bool (Set   ($#k2_rat_1 :::"numerator"::: )  (Set (Var "p")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) ; 
 
theorem :: RAT_1:39 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::) "holds"   (Bool  "("  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "p"))) "iff" (Bool (Set (Set (Var "a"))  ($#k4_real_1 :::"*"::: )  (Set  "("  ($#k1_rat_1 :::"denominator"::: )  (Set (Var "p")) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k2_rat_1 :::"numerator"::: )  (Set (Var "p"))))  ")" ))) ; 
 
theorem :: RAT_1:40 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::) "holds"   (Bool  "("  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "p"))) "iff" (Bool (Set (Set (Var "a"))  ($#k4_real_1 :::"*"::: )  (Set  "("  ($#k1_rat_1 :::"denominator"::: )  (Set (Var "p")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k2_rat_1 :::"numerator"::: )  (Set (Var "p"))))  ")" ))) ; 
 
theorem :: RAT_1:41 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"Rational":::)  "st" (Bool (Bool (Set   ($#k1_rat_1 :::"denominator"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_rat_1 :::"denominator"::: )  (Set (Var "q")))) & (Bool (Set   ($#k2_rat_1 :::"numerator"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_rat_1 :::"numerator"::: )  (Set (Var "q"))))) "holds"  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Var "q")))) ; 
 
theorem :: RAT_1:42 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"Rational":::) "holds"   (Bool  "("  (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "q"))) "iff" (Bool (Set (Set  "("  ($#k2_rat_1 :::"numerator"::: )  (Set (Var "p")) ")" )  ($#k4_real_1 :::"*"::: )  (Set  "("  ($#k1_rat_1 :::"denominator"::: )  (Set (Var "q")) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "("  ($#k2_rat_1 :::"numerator"::: )  (Set (Var "q")) ")" )  ($#k4_real_1 :::"*"::: )  (Set  "("  ($#k1_rat_1 :::"denominator"::: )  (Set (Var "p")) ")" )))  ")" )) ; 
 
theorem :: RAT_1:43 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::) "holds"   (Bool  "("  (Bool (Set   ($#k1_rat_1 :::"denominator"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_rat_1 :::"denominator"::: )  (Set (Var "p")))) & (Bool (Set   ($#k2_rat_1 :::"numerator"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "("  ($#k2_rat_1 :::"numerator"::: )  (Set (Var "p")) ")" )))  ")" )) ; 
 
theorem :: RAT_1:44 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"Rational":::) "holds"   (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "p"))) & (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Set (Var "p")))) "iff" (Bool  "("  (Bool (Set   ($#k2_rat_1 :::"numerator"::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_rat_1 :::"denominator"::: )  (Set (Var "p")))) & (Bool (Set   ($#k1_rat_1 :::"denominator"::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_rat_1 :::"numerator"::: )  (Set (Var "p"))))  ")" )  ")" )) ; 
 
theorem :: RAT_1:45 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"Rational":::) "holds"   (Bool  "("  (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Set (Var "p")))) "iff" (Bool  "("  (Bool (Set   ($#k2_rat_1 :::"numerator"::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "("  ($#k1_rat_1 :::"denominator"::: )  (Set (Var "p")) ")" ))) & (Bool (Set   ($#k1_rat_1 :::"denominator"::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "("  ($#k2_rat_1 :::"numerator"::: )  (Set (Var "p")) ")" )))  ")" )  ")" )) ;