:: ARYTM_3  semantic presentation begin  




definitionfunc  :::"one":::  ->    ($#m1_hidden :::"set"::: )   equals :: ARYTM_3:def 1 (Num 1); end; 




:: deftheorem    defines :::"one"::: ARYTM_3:def 1 :  (Bool (Set   ($#k1_arytm_3 :::"one"::: )  )  ($#r1_hidden :::"="::: )  (Num 1)); 
 begin  definitionlet "a", "b" be   ($#m1_hidden :::"Ordinal":::); pred "a" "," "b" :::"are_relative_prime":::  means :: ARYTM_3:def 2 (Bool  "for" (Set (Var "c")) "," (Set (Var "d1")) "," (Set (Var "d2")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool "a"  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k11_ordinal2 :::"*^"::: )  (Set (Var "d1")))) & (Bool "b"  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k11_ordinal2 :::"*^"::: )  (Set (Var "d2"))))) "holds"  (Bool (Set (Var "c"))  ($#r1_hidden :::"="::: )  (Num 1))); symmetry  
(Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool  "("   "for" (Set (Var "c")) "," (Set (Var "d1")) "," (Set (Var "d2")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k11_ordinal2 :::"*^"::: )  (Set (Var "d1")))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k11_ordinal2 :::"*^"::: )  (Set (Var "d2"))))) "holds"  (Bool (Set (Var "c"))  ($#r1_hidden :::"="::: )  (Num 1))  ")" )) "holds"  (Bool  "for" (Set (Var "c")) "," (Set (Var "d1")) "," (Set (Var "d2")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k11_ordinal2 :::"*^"::: )  (Set (Var "d1")))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k11_ordinal2 :::"*^"::: )  (Set (Var "d2"))))) "holds"  (Bool (Set (Var "c"))  ($#r1_hidden :::"="::: )  (Num 1))))
 ; end; 





:: deftheorem    defines :::"are_relative_prime"::: ARYTM_3:def 2 :  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"   (Bool  "("  (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r1_arytm_3 :::"are_relative_prime"::: )  ) "iff" (Bool  "for" (Set (Var "c")) "," (Set (Var "d1")) "," (Set (Var "d2")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k11_ordinal2 :::"*^"::: )  (Set (Var "d1")))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k11_ordinal2 :::"*^"::: )  (Set (Var "d2"))))) "holds"  (Bool (Set (Var "c"))  ($#r1_hidden :::"="::: )  (Num 1)))  ")" )); 
 
theorem :: ARYTM_3:1 (Bool (Bool  "not" (Set   ($#k1_xboole_0 :::"{}"::: )  ) "," (Set   ($#k1_xboole_0 :::"{}"::: )  )  ($#r1_arytm_3 :::"are_relative_prime"::: )  )) ; 
 
theorem :: ARYTM_3:2 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"  (Bool (Num 1) "," (Set (Var "A"))  ($#r1_arytm_3 :::"are_relative_prime"::: )  )) ; 
 
theorem :: ARYTM_3:3 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set   ($#k1_xboole_0 :::"{}"::: )  ) "," (Set (Var "A"))  ($#r1_arytm_3 :::"are_relative_prime"::: )  )) "holds"  (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 






theorem :: ARYTM_3:4 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) "or" (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" )) "holds"  (Bool  "ex" (Set (Var "c")) "," (Set (Var "d1")) "," (Set (Var "d2")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::) "st"  (Bool  "("  (Bool (Set (Var "d1")) "," (Set (Var "d2"))  ($#r1_arytm_3 :::"are_relative_prime"::: )  ) & (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k9_ordinal3 :::"*^"::: )  (Set (Var "d1")))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k9_ordinal3 :::"*^"::: )  (Set (Var "d2"))))  ")" ))) ; 
 




registrationlet "m", "n" be   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::); 
cluster (Set "m"  ($#k6_ordinal3 :::"div^"::: )  "n") ->   ($#v7_ordinal1 :::"natural"::: )   ; 

cluster (Set "m"  ($#k7_ordinal3 :::"mod^"::: )  "n") ->   ($#v7_ordinal1 :::"natural"::: )   ; 
end; definitionlet "k", "n" be   ($#m1_hidden :::"Ordinal":::); pred "k" :::"divides"::: "n" means :: ARYTM_3:def 3 (Bool  "ex" (Set (Var "a")) "being"   ($#m1_hidden :::"Ordinal":::) "st" (Bool "n"  ($#r1_hidden :::"="::: )  (Set "k"  ($#k11_ordinal2 :::"*^"::: )  (Set (Var "a"))))); reflexivity  
(Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Ordinal":::) (Bool  "ex" (Set (Var "a")) "being"   ($#m1_hidden :::"Ordinal":::) "st" (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k11_ordinal2 :::"*^"::: )  (Set (Var "a"))))))
 ; end; 





:: deftheorem    defines :::"divides"::: ARYTM_3:def 3 :  (Bool  "for" (Set (Var "k")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"   (Bool  "("  (Bool (Set (Var "k"))  ($#r2_arytm_3 :::"divides"::: )  (Set (Var "n"))) "iff" (Bool  "ex" (Set (Var "a")) "being"   ($#m1_hidden :::"Ordinal":::) "st" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k11_ordinal2 :::"*^"::: )  (Set (Var "a")))))  ")" )); 
 
theorem :: ARYTM_3:5 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::) "holds"   (Bool  "("  (Bool (Set (Var "a"))  ($#r2_arytm_3 :::"divides"::: )  (Set (Var "b"))) "iff" (Bool  "ex" (Set (Var "c")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::) "st" (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k9_ordinal3 :::"*^"::: )  (Set (Var "c")))))  ")" )) ; 
 
theorem :: ARYTM_3:6 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set   ($#k1_xboole_0 :::"{}"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Var "m")))) "holds"  (Bool (Set (Set (Var "n"))  ($#k7_ordinal3 :::"mod^"::: )  (Set (Var "m")))  ($#r2_hidden :::"in"::: )  (Set (Var "m")))) ; 
 
theorem :: ARYTM_3:7 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::) "holds"   (Bool  "("  (Bool (Set (Var "m"))  ($#r2_arytm_3 :::"divides"::: )  (Set (Var "n"))) "iff" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k9_ordinal3 :::"*^"::: )  (Set  "(" (Set (Var "n"))  ($#k6_ordinal3 :::"div^"::: )  (Set (Var "m")) ")" )))  ")" )) ; 
 
theorem :: ARYTM_3:8 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r2_arytm_3 :::"divides"::: )  (Set (Var "m"))) & (Bool (Set (Var "m"))  ($#r2_arytm_3 :::"divides"::: )  (Set (Var "n")))) "holds"  (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set (Var "m")))) ; 
 
theorem :: ARYTM_3:9 (Bool  "for" (Set (Var "n")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::) "holds"   (Bool  "("  (Bool (Set (Var "n"))  ($#r2_arytm_3 :::"divides"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Num 1)  ($#r2_arytm_3 :::"divides"::: )  (Set (Var "n")))  ")" )) ; 
 
theorem :: ARYTM_3:10 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set   ($#k1_xboole_0 :::"{}"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Var "m"))) & (Bool (Set (Var "n"))  ($#r2_arytm_3 :::"divides"::: )  (Set (Var "m")))) "holds"  (Bool (Set (Var "n"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "m")))) ; 
 
theorem :: ARYTM_3:11 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "l")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r2_arytm_3 :::"divides"::: )  (Set (Var "m"))) & (Bool (Set (Var "n"))  ($#r2_arytm_3 :::"divides"::: )  (Set (Set (Var "m"))  ($#k8_ordinal3 :::"+^"::: )  (Set (Var "l"))))) "holds"  (Bool (Set (Var "n"))  ($#r2_arytm_3 :::"divides"::: )  (Set (Var "l")))) ; 
 definitionlet "k", "n" be   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::); func "k" :::"lcm"::: "n" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k4_ordinal1 :::"omega"::: )  ) means :: ARYTM_3:def 4 (Bool  "("  (Bool "k"  ($#r2_arytm_3 :::"divides"::: )  it) & (Bool "n"  ($#r2_arytm_3 :::"divides"::: )  it) & (Bool  "("   "for" (Set (Var "m")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool "k"  ($#r2_arytm_3 :::"divides"::: )  (Set (Var "m"))) & (Bool "n"  ($#r2_arytm_3 :::"divides"::: )  (Set (Var "m")))) "holds"  (Bool it  ($#r2_arytm_3 :::"divides"::: )  (Set (Var "m")))  ")" )  ")" ); commutativity  
(Bool  "for" (Set (Var "b1")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k4_ordinal1 :::"omega"::: )  )  (Bool  "for" (Set (Var "k")) "," (Set (Var "n")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r2_arytm_3 :::"divides"::: )  (Set (Var "b1"))) & (Bool (Set (Var "n"))  ($#r2_arytm_3 :::"divides"::: )  (Set (Var "b1"))) & (Bool  "("   "for" (Set (Var "m")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r2_arytm_3 :::"divides"::: )  (Set (Var "m"))) & (Bool (Set (Var "n"))  ($#r2_arytm_3 :::"divides"::: )  (Set (Var "m")))) "holds"  (Bool (Set (Var "b1"))  ($#r2_arytm_3 :::"divides"::: )  (Set (Var "m")))  ")" )) "holds"  (Bool  "("  (Bool (Set (Var "n"))  ($#r2_arytm_3 :::"divides"::: )  (Set (Var "b1"))) & (Bool (Set (Var "k"))  ($#r2_arytm_3 :::"divides"::: )  (Set (Var "b1"))) & (Bool  "("   "for" (Set (Var "m")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r2_arytm_3 :::"divides"::: )  (Set (Var "m"))) & (Bool (Set (Var "k"))  ($#r2_arytm_3 :::"divides"::: )  (Set (Var "m")))) "holds"  (Bool (Set (Var "b1"))  ($#r2_arytm_3 :::"divides"::: )  (Set (Var "m")))  ")" )  ")" )))
 ; end; 






:: deftheorem    defines :::"lcm"::: ARYTM_3:def 4 :  (Bool  "for" (Set (Var "k")) "," (Set (Var "n")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "b3")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k4_ordinal1 :::"omega"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k2_arytm_3 :::"lcm"::: )  (Set (Var "n")))) "iff" (Bool  "("  (Bool (Set (Var "k"))  ($#r2_arytm_3 :::"divides"::: )  (Set (Var "b3"))) & (Bool (Set (Var "n"))  ($#r2_arytm_3 :::"divides"::: )  (Set (Var "b3"))) & (Bool  "("   "for" (Set (Var "m")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r2_arytm_3 :::"divides"::: )  (Set (Var "m"))) & (Bool (Set (Var "n"))  ($#r2_arytm_3 :::"divides"::: )  (Set (Var "m")))) "holds"  (Bool (Set (Var "b3"))  ($#r2_arytm_3 :::"divides"::: )  (Set (Var "m")))  ")" )  ")" )  ")" ))); 
 
theorem :: ARYTM_3:12 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::) "holds"  (Bool (Set (Set (Var "m"))  ($#k2_arytm_3 :::"lcm"::: )  (Set (Var "n")))  ($#r2_arytm_3 :::"divides"::: )  (Set (Set (Var "m"))  ($#k9_ordinal3 :::"*^"::: )  (Set (Var "n"))))) ; 
 
theorem :: ARYTM_3:13 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "m"))  ($#k9_ordinal3 :::"*^"::: )  (Set (Var "n")) ")" )  ($#k6_ordinal3 :::"div^"::: )  (Set  "(" (Set (Var "m"))  ($#k2_arytm_3 :::"lcm"::: )  (Set (Var "n")) ")" ))  ($#r2_arytm_3 :::"divides"::: )  (Set (Var "m")))) ; 
 definitionlet "k", "n" be   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::); func "k" :::"hcf"::: "n" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k4_ordinal1 :::"omega"::: )  ) means :: ARYTM_3:def 5 (Bool  "("  (Bool it  ($#r2_arytm_3 :::"divides"::: )  "k") & (Bool it  ($#r2_arytm_3 :::"divides"::: )  "n") & (Bool  "("   "for" (Set (Var "m")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r2_arytm_3 :::"divides"::: )  "k") & (Bool (Set (Var "m"))  ($#r2_arytm_3 :::"divides"::: )  "n")) "holds"  (Bool (Set (Var "m"))  ($#r2_arytm_3 :::"divides"::: )  it)  ")" )  ")" ); commutativity  
(Bool  "for" (Set (Var "b1")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k4_ordinal1 :::"omega"::: )  )  (Bool  "for" (Set (Var "k")) "," (Set (Var "n")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "b1"))  ($#r2_arytm_3 :::"divides"::: )  (Set (Var "k"))) & (Bool (Set (Var "b1"))  ($#r2_arytm_3 :::"divides"::: )  (Set (Var "n"))) & (Bool  "("   "for" (Set (Var "m")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r2_arytm_3 :::"divides"::: )  (Set (Var "k"))) & (Bool (Set (Var "m"))  ($#r2_arytm_3 :::"divides"::: )  (Set (Var "n")))) "holds"  (Bool (Set (Var "m"))  ($#r2_arytm_3 :::"divides"::: )  (Set (Var "b1")))  ")" )) "holds"  (Bool  "("  (Bool (Set (Var "b1"))  ($#r2_arytm_3 :::"divides"::: )  (Set (Var "n"))) & (Bool (Set (Var "b1"))  ($#r2_arytm_3 :::"divides"::: )  (Set (Var "k"))) & (Bool  "("   "for" (Set (Var "m")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r2_arytm_3 :::"divides"::: )  (Set (Var "n"))) & (Bool (Set (Var "m"))  ($#r2_arytm_3 :::"divides"::: )  (Set (Var "k")))) "holds"  (Bool (Set (Var "m"))  ($#r2_arytm_3 :::"divides"::: )  (Set (Var "b1")))  ")" )  ")" )))
 ; end; 






:: deftheorem    defines :::"hcf"::: ARYTM_3:def 5 :  (Bool  "for" (Set (Var "k")) "," (Set (Var "n")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "b3")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k4_ordinal1 :::"omega"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k3_arytm_3 :::"hcf"::: )  (Set (Var "n")))) "iff" (Bool  "("  (Bool (Set (Var "b3"))  ($#r2_arytm_3 :::"divides"::: )  (Set (Var "k"))) & (Bool (Set (Var "b3"))  ($#r2_arytm_3 :::"divides"::: )  (Set (Var "n"))) & (Bool  "("   "for" (Set (Var "m")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r2_arytm_3 :::"divides"::: )  (Set (Var "k"))) & (Bool (Set (Var "m"))  ($#r2_arytm_3 :::"divides"::: )  (Set (Var "n")))) "holds"  (Bool (Set (Var "m"))  ($#r2_arytm_3 :::"divides"::: )  (Set (Var "b3")))  ")" )  ")" )  ")" ))); 
 
theorem :: ARYTM_3:14 (Bool  "for" (Set (Var "a")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::) "holds"   (Bool  "("  (Bool (Set (Set (Var "a"))  ($#k3_arytm_3 :::"hcf"::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Set (Var "a"))  ($#k2_arytm_3 :::"lcm"::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" )) ; 
 
theorem :: ARYTM_3:15 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Set (Var "a"))  ($#k3_arytm_3 :::"hcf"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: ARYTM_3:16 (Bool  "for" (Set (Var "a")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::) "holds"   (Bool  "("  (Bool (Set (Set (Var "a"))  ($#k3_arytm_3 :::"hcf"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Set (Var "a"))  ($#k2_arytm_3 :::"lcm"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")" )) ; 
 
theorem :: ARYTM_3:17 (Bool  "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k9_ordinal3 :::"*^"::: )  (Set (Var "c")) ")" )  ($#k3_arytm_3 :::"hcf"::: )  (Set  "(" (Set (Var "b"))  ($#k9_ordinal3 :::"*^"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k3_arytm_3 :::"hcf"::: )  (Set (Var "b")) ")" )  ($#k9_ordinal3 :::"*^"::: )  (Set (Var "c"))))) ; 
 
theorem :: ARYTM_3:18 (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Set (Var "a"))  ($#k3_arytm_3 :::"hcf"::: )  (Set (Var "b")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Set (Var "b"))  ($#k6_ordinal3 :::"div^"::: )  (Set  "(" (Set (Var "a"))  ($#k3_arytm_3 :::"hcf"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" )) ; 
 
theorem :: ARYTM_3:19 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) "or" (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" )) "holds"  (Bool (Set (Set (Var "a"))  ($#k6_ordinal3 :::"div^"::: )  (Set  "(" (Set (Var "a"))  ($#k3_arytm_3 :::"hcf"::: )  (Set (Var "b")) ")" )) "," (Set (Set (Var "b"))  ($#k6_ordinal3 :::"div^"::: )  (Set  "(" (Set (Var "a"))  ($#k3_arytm_3 :::"hcf"::: )  (Set (Var "b")) ")" ))  ($#r1_arytm_3 :::"are_relative_prime"::: )  )) ; 
 
theorem :: ARYTM_3:20 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::) "holds"   (Bool  "("  (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r1_arytm_3 :::"are_relative_prime"::: )  ) "iff" (Bool (Set (Set (Var "a"))  ($#k3_arytm_3 :::"hcf"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Num 1))  ")" )) ; 
 definitionlet "a", "b" be   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::); func  :::"RED":::  "(" "a" "," "b" ")"  ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k4_ordinal1 :::"omega"::: )  ) equals :: ARYTM_3:def 6 (Set "a"  ($#k6_ordinal3 :::"div^"::: )  (Set  "(" "a"  ($#k3_arytm_3 :::"hcf"::: )  "b" ")" )); end; 






:: deftheorem    defines :::"RED"::: ARYTM_3:def 6 :  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::) "holds"  (Bool (Set   ($#k4_arytm_3 :::"RED"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k6_ordinal3 :::"div^"::: )  (Set  "(" (Set (Var "a"))  ($#k3_arytm_3 :::"hcf"::: )  (Set (Var "b")) ")" )))); 
 
theorem :: ARYTM_3:21 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::) "holds"  (Bool (Set (Set  "("  ($#k4_arytm_3 :::"RED"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" )  ($#k9_ordinal3 :::"*^"::: )  (Set  "(" (Set (Var "a"))  ($#k3_arytm_3 :::"hcf"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "a")))) ; 
 
theorem :: ARYTM_3:22 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) "or" (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" )) "holds"  (Bool (Set   ($#k4_arytm_3 :::"RED"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "," (Set   ($#k4_arytm_3 :::"RED"::: )   "(" (Set (Var "b")) "," (Set (Var "a")) ")" )  ($#r1_arytm_3 :::"are_relative_prime"::: )  )) ; 
 
theorem :: ARYTM_3:23 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r1_arytm_3 :::"are_relative_prime"::: )  )) "holds"  (Bool (Set   ($#k4_arytm_3 :::"RED"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "a")))) ; 
 
theorem :: ARYTM_3:24 (Bool  "for" (Set (Var "a")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::) "holds"   (Bool  "("  (Bool (Set   ($#k4_arytm_3 :::"RED"::: )   "(" (Set (Var "a")) "," (Num 1) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set   ($#k4_arytm_3 :::"RED"::: )   "(" (Num 1) "," (Set (Var "a")) ")" )  ($#r1_hidden :::"="::: )  (Num 1))  ")" )) ; 
 
theorem :: ARYTM_3:25 (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool (Set   ($#k4_arytm_3 :::"RED"::: )   "(" (Set (Var "b")) "," (Set (Var "a")) ")" )  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: ARYTM_3:26 (Bool  "for" (Set (Var "a")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::) "holds"   (Bool  "("  (Bool (Set   ($#k4_arytm_3 :::"RED"::: )   "(" (Set  ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "a")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) &  "("  (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "implies" (Bool (Set   ($#k4_arytm_3 :::"RED"::: )   "(" (Set (Var "a")) "," (Set  ($#k1_xboole_0 :::"{}"::: ) ) ")" )  ($#r1_hidden :::"="::: )  (Num 1))  ")"   ")" )) ; 
 
theorem :: ARYTM_3:27 (Bool  "for" (Set (Var "a")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool (Set   ($#k4_arytm_3 :::"RED"::: )   "(" (Set (Var "a")) "," (Set (Var "a")) ")" )  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: ARYTM_3:28 (Bool  "for" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool (Set   ($#k4_arytm_3 :::"RED"::: )   "(" (Set  "(" (Set (Var "a"))  ($#k9_ordinal3 :::"*^"::: )  (Set (Var "c")) ")" ) "," (Set  "(" (Set (Var "b"))  ($#k9_ordinal3 :::"*^"::: )  (Set (Var "c")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_arytm_3 :::"RED"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))) ; 
 begin  




definitionfunc  :::"RAT+":::  ->    ($#m1_hidden :::"set"::: )   equals :: ARYTM_3:def 7 (Set (Set  "("  "{"  (Set  ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) where i, j "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k4_ordinal1 :::"omega"::: )  ) : (Bool  "("  (Bool (Set (Var "i")) "," (Set (Var "j"))  ($#r1_arytm_3 :::"are_relative_prime"::: )  ) & (Bool (Set (Var "j"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" )  "}"    ($#k6_subset_1 :::"\"::: )   "{"  (Set  ($#k4_tarski :::"["::: ) (Set (Var "k")) "," (Num 1) ($#k4_tarski :::"]"::: ) ) where k "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k4_ordinal1 :::"omega"::: )  ) : (Bool verum)  "}"   ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k4_ordinal1 :::"omega"::: ) )); end; 




:: deftheorem    defines :::"RAT+"::: ARYTM_3:def 7 :  (Bool (Set   ($#k5_arytm_3 :::"RAT+"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "("  "{"  (Set  ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) where i, j "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k4_ordinal1 :::"omega"::: )  ) : (Bool  "("  (Bool (Set (Var "i")) "," (Set (Var "j"))  ($#r1_arytm_3 :::"are_relative_prime"::: )  ) & (Bool (Set (Var "j"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" )  "}"    ($#k6_subset_1 :::"\"::: )   "{"  (Set  ($#k4_tarski :::"["::: ) (Set (Var "k")) "," (Num 1) ($#k4_tarski :::"]"::: ) ) where k "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k4_ordinal1 :::"omega"::: )  ) : (Bool verum)  "}"   ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k4_ordinal1 :::"omega"::: ) ))); 
 




registration
cluster (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; registration
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v3_ordinal1 :::"ordinal"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ); 
end; 
theorem :: ARYTM_3:29 (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  )  "holds"  (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_ordinal1 :::"omega"::: )  )) "or" (Bool  "ex" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k4_ordinal1 :::"omega"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "i")) "," (Set (Var "j"))  ($#r1_arytm_3 :::"are_relative_prime"::: )  ) & (Bool (Set (Var "j"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "j"))  ($#r1_hidden :::"<>"::: )  (Num 1))  ")" ))  ")" )) ; 
 
theorem :: ARYTM_3:30 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_hidden :::"set"::: )    "holds" (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) "is" (Bool  "not"   ($#m1_hidden :::"Ordinal":::)))) ; 
 
theorem :: ARYTM_3:31 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set   ($#k5_arytm_3 :::"RAT+"::: )  ))) "holds"  (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_ordinal1 :::"omega"::: )  ))) ; 
 registration
cluster   ($#v3_ordinal1 :::"ordinal"::: )    ->   ($#v3_ordinal1 :::"ordinal"::: )     ($#v7_ordinal1 :::"natural"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ); 
end; 
theorem :: ARYTM_3:32 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_hidden :::"set"::: )    "holds" (Bool (Bool  "not" (Set  ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k4_ordinal1 :::"omega"::: )  )))) ; 
 
theorem :: ARYTM_3:33 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k4_ordinal1 :::"omega"::: )  ) "holds"   (Bool  "("  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k5_arytm_3 :::"RAT+"::: )  )) "iff" (Bool  "("  (Bool (Set (Var "i")) "," (Set (Var "j"))  ($#r1_arytm_3 :::"are_relative_prime"::: )  ) & (Bool (Set (Var "j"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "j"))  ($#r1_hidden :::"<>"::: )  (Num 1))  ")" )  ")" )) ; 
 definitionlet "x" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ); func  :::"numerator"::: "x" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k4_ordinal1 :::"omega"::: )  ) means :: ARYTM_3:def 8 (Bool it  ($#r1_hidden :::"="::: )  "x") if (Bool "x"  ($#r2_hidden :::"in"::: )  (Set   ($#k4_ordinal1 :::"omega"::: )  ))  otherwise (Bool  "ex" (Set (Var "a")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::) "st" (Bool "x"  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) it "," (Set (Var "a")) ($#k4_tarski :::"]"::: ) ))); func  :::"denominator"::: "x" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k4_ordinal1 :::"omega"::: )  ) means :: ARYTM_3:def 9 (Bool it  ($#r1_hidden :::"="::: )  (Num 1)) if (Bool "x"  ($#r2_hidden :::"in"::: )  (Set   ($#k4_ordinal1 :::"omega"::: )  ))  otherwise (Bool  "ex" (Set (Var "a")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::) "st" (Bool "x"  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," it ($#k4_tarski :::"]"::: ) ))); end; 










:: deftheorem    defines :::"numerator"::: ARYTM_3:def 8 :  (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  )  (Bool  "for" (Set (Var "b2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k4_ordinal1 :::"omega"::: )  ) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_ordinal1 :::"omega"::: )  ))) "implies" (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_arytm_3 :::"numerator"::: )  (Set (Var "x")))) "iff" (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set (Var "x")))  ")" )  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_ordinal1 :::"omega"::: )  )))) "implies" (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_arytm_3 :::"numerator"::: )  (Set (Var "x")))) "iff" (Bool  "ex" (Set (Var "a")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::) "st" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set (Var "b2")) "," (Set (Var "a")) ($#k4_tarski :::"]"::: ) )))  ")" )  ")"   ")" ))); 
 
:: deftheorem    defines :::"denominator"::: ARYTM_3:def 9 :  (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  )  (Bool  "for" (Set (Var "b2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k4_ordinal1 :::"omega"::: )  ) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_ordinal1 :::"omega"::: )  ))) "implies" (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k7_arytm_3 :::"denominator"::: )  (Set (Var "x")))) "iff" (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Num 1))  ")" )  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_ordinal1 :::"omega"::: )  )))) "implies" (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k7_arytm_3 :::"denominator"::: )  (Set (Var "x")))) "iff" (Bool  "ex" (Set (Var "a")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::) "st" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b2")) ($#k4_tarski :::"]"::: ) )))  ")" )  ")"   ")" ))); 
 
theorem :: ARYTM_3:34 (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) "holds"  (Bool (Set   ($#k6_arytm_3 :::"numerator"::: )  (Set (Var "x"))) "," (Set   ($#k7_arytm_3 :::"denominator"::: )  (Set (Var "x")))  ($#r1_arytm_3 :::"are_relative_prime"::: )  )) ; 
 
theorem :: ARYTM_3:35 (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  )  "holds" (Bool (Set   ($#k7_arytm_3 :::"denominator"::: )  (Set (Var "x")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: ARYTM_3:36 (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  )  "st" (Bool (Bool (Bool  "not" (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_ordinal1 :::"omega"::: )  )))) "holds"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set  "("  ($#k6_arytm_3 :::"numerator"::: )  (Set (Var "x")) ")" ) "," (Set  "("  ($#k7_arytm_3 :::"denominator"::: )  (Set (Var "x")) ")" ) ($#k4_tarski :::"]"::: ) )) & (Bool (Set   ($#k7_arytm_3 :::"denominator"::: )  (Set (Var "x")))  ($#r1_hidden :::"<>"::: )  (Num 1))  ")" )) ; 
 
theorem :: ARYTM_3:37 (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) "iff" (Bool (Set   ($#k6_arytm_3 :::"numerator"::: )  (Set (Var "x")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" )) ; 
 
theorem :: ARYTM_3:38 (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_ordinal1 :::"omega"::: )  )) "iff" (Bool (Set   ($#k7_arytm_3 :::"denominator"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Num 1))  ")" )) ; 
 definitionlet "i", "j" be   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::); func "i" :::"/"::: "j" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) equals :: ARYTM_3:def 10 (Set   ($#k1_xboole_0 :::"{}"::: )  ) if (Bool "j"  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) (Set   ($#k4_arytm_3 :::"RED"::: )   "(" "i" "," "j" ")" ) if (Bool (Set   ($#k4_arytm_3 :::"RED"::: )   "(" "j" "," "i" ")" )  ($#r1_hidden :::"="::: )  (Num 1))  otherwise (Set  ($#k4_tarski :::"["::: ) (Set  "("  ($#k4_arytm_3 :::"RED"::: )   "(" "i" "," "j" ")"  ")" ) "," (Set  "("  ($#k4_arytm_3 :::"RED"::: )   "(" "j" "," "i" ")"  ")" ) ($#k4_tarski :::"]"::: ) ); end; 






:: deftheorem    defines :::"/"::: ARYTM_3:def 10 :  (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "j"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "implies" (Bool (Set (Set (Var "i"))  ($#k8_arytm_3 :::"/"::: )  (Set (Var "j")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")"  &  "("  (Bool (Bool (Set   ($#k4_arytm_3 :::"RED"::: )   "(" (Set (Var "j")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Num 1))) "implies" (Bool (Set (Set (Var "i"))  ($#k8_arytm_3 :::"/"::: )  (Set (Var "j")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_arytm_3 :::"RED"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "j"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) & (Bool (Bool  "not" (Set   ($#k4_arytm_3 :::"RED"::: )   "(" (Set (Var "j")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Num 1)))) "implies" (Bool (Set (Set (Var "i"))  ($#k8_arytm_3 :::"/"::: )  (Set (Var "j")))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set  "("  ($#k4_arytm_3 :::"RED"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")"  ")" ) "," (Set  "("  ($#k4_arytm_3 :::"RED"::: )   "(" (Set (Var "j")) "," (Set (Var "i")) ")"  ")" ) ($#k4_tarski :::"]"::: ) ))  ")"   ")" )); 
 notationlet "i", "j" be   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::); synonym  :::"quotient":::  "(" "i" "," "j" ")"  for "i" :::"/"::: "j"; end; 
theorem :: ARYTM_3:39 (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) "holds"  (Bool (Set (Set  "("  ($#k6_arytm_3 :::"numerator"::: )  (Set (Var "x")) ")" )  ($#k8_arytm_3 :::"/"::: )  (Set  "("  ($#k7_arytm_3 :::"denominator"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "x")))) ; 
 
theorem :: ARYTM_3:40 (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::) "holds"   (Bool  "("  (Bool (Set (Set  ($#k1_xboole_0 :::"{}"::: ) )  ($#k8_arytm_3 :::"/"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Set (Var "a"))  ($#k8_arytm_3 :::"/"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")" )) ; 
 
theorem :: ARYTM_3:41 (Bool  "for" (Set (Var "a")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k8_arytm_3 :::"/"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: ARYTM_3:42 (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool  "("  (Bool (Set   ($#k6_arytm_3 :::"numerator"::: )  (Set  "(" (Set (Var "a"))  ($#k8_arytm_3 :::"/"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_arytm_3 :::"RED"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) & (Bool (Set   ($#k7_arytm_3 :::"denominator"::: )  (Set  "(" (Set (Var "a"))  ($#k8_arytm_3 :::"/"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_arytm_3 :::"RED"::: )   "(" (Set (Var "b")) "," (Set (Var "a")) ")" ))  ")" )) ; 
 
theorem :: ARYTM_3:43 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k4_ordinal1 :::"omega"::: )  )  "st" (Bool (Bool (Set (Var "i")) "," (Set (Var "j"))  ($#r1_arytm_3 :::"are_relative_prime"::: )  ) & (Bool (Set (Var "j"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool  "("  (Bool (Set   ($#k6_arytm_3 :::"numerator"::: )  (Set  "(" (Set (Var "i"))  ($#k8_arytm_3 :::"/"::: )  (Set (Var "j")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "i"))) & (Bool (Set   ($#k7_arytm_3 :::"denominator"::: )  (Set  "(" (Set (Var "i"))  ($#k8_arytm_3 :::"/"::: )  (Set (Var "j")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "j")))  ")" )) ; 
 
theorem :: ARYTM_3:44 (Bool  "for" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k9_ordinal3 :::"*^"::: )  (Set (Var "c")) ")" )  ($#k8_arytm_3 :::"/"::: )  (Set  "(" (Set (Var "b"))  ($#k9_ordinal3 :::"*^"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k8_arytm_3 :::"/"::: )  (Set (Var "b"))))) ; 
 





theorem :: ARYTM_3:45 (Bool  "for" (Set (Var "l")) "," (Set (Var "j")) "," (Set (Var "i")) "," (Set (Var "k")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "j"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "l"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Set (Var "i"))  ($#k8_arytm_3 :::"/"::: )  (Set (Var "j")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k8_arytm_3 :::"/"::: )  (Set (Var "l")))) "iff" (Bool (Set (Set (Var "i"))  ($#k9_ordinal3 :::"*^"::: )  (Set (Var "l")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "j"))  ($#k9_ordinal3 :::"*^"::: )  (Set (Var "k"))))  ")" )) ; 
 definitionlet "x", "y" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ); func "x" :::"+"::: "y" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) equals :: ARYTM_3:def 11 (Set (Set  "(" (Set  "(" (Set  "("  ($#k6_arytm_3 :::"numerator"::: )  "x" ")" )  ($#k9_ordinal3 :::"*^"::: )  (Set  "("  ($#k7_arytm_3 :::"denominator"::: )  "y" ")" ) ")" )  ($#k8_ordinal3 :::"+^"::: )  (Set  "(" (Set  "("  ($#k6_arytm_3 :::"numerator"::: )  "y" ")" )  ($#k9_ordinal3 :::"*^"::: )  (Set  "("  ($#k7_arytm_3 :::"denominator"::: )  "x" ")" ) ")" ) ")" )  ($#k8_arytm_3 :::"/"::: )  (Set  "(" (Set  "("  ($#k7_arytm_3 :::"denominator"::: )  "x" ")" )  ($#k9_ordinal3 :::"*^"::: )  (Set  "("  ($#k7_arytm_3 :::"denominator"::: )  "y" ")" ) ")" )); commutativity  
(Bool  "for" (Set (Var "b1")) "," (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  )  "st" (Bool (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "("  ($#k6_arytm_3 :::"numerator"::: )  (Set (Var "x")) ")" )  ($#k9_ordinal3 :::"*^"::: )  (Set  "("  ($#k7_arytm_3 :::"denominator"::: )  (Set (Var "y")) ")" ) ")" )  ($#k8_ordinal3 :::"+^"::: )  (Set  "(" (Set  "("  ($#k6_arytm_3 :::"numerator"::: )  (Set (Var "y")) ")" )  ($#k9_ordinal3 :::"*^"::: )  (Set  "("  ($#k7_arytm_3 :::"denominator"::: )  (Set (Var "x")) ")" ) ")" ) ")" )  ($#k8_arytm_3 :::"/"::: )  (Set  "(" (Set  "("  ($#k7_arytm_3 :::"denominator"::: )  (Set (Var "x")) ")" )  ($#k9_ordinal3 :::"*^"::: )  (Set  "("  ($#k7_arytm_3 :::"denominator"::: )  (Set (Var "y")) ")" ) ")" )))) "holds"  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "("  ($#k6_arytm_3 :::"numerator"::: )  (Set (Var "y")) ")" )  ($#k9_ordinal3 :::"*^"::: )  (Set  "("  ($#k7_arytm_3 :::"denominator"::: )  (Set (Var "x")) ")" ) ")" )  ($#k8_ordinal3 :::"+^"::: )  (Set  "(" (Set  "("  ($#k6_arytm_3 :::"numerator"::: )  (Set (Var "x")) ")" )  ($#k9_ordinal3 :::"*^"::: )  (Set  "("  ($#k7_arytm_3 :::"denominator"::: )  (Set (Var "y")) ")" ) ")" ) ")" )  ($#k8_arytm_3 :::"/"::: )  (Set  "(" (Set  "("  ($#k7_arytm_3 :::"denominator"::: )  (Set (Var "y")) ")" )  ($#k9_ordinal3 :::"*^"::: )  (Set  "("  ($#k7_arytm_3 :::"denominator"::: )  (Set (Var "x")) ")" ) ")" ))))
 ; func "x" :::"*'"::: "y" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) equals :: ARYTM_3:def 12 (Set (Set  "(" (Set  "("  ($#k6_arytm_3 :::"numerator"::: )  "x" ")" )  ($#k9_ordinal3 :::"*^"::: )  (Set  "("  ($#k6_arytm_3 :::"numerator"::: )  "y" ")" ) ")" )  ($#k8_arytm_3 :::"/"::: )  (Set  "(" (Set  "("  ($#k7_arytm_3 :::"denominator"::: )  "x" ")" )  ($#k9_ordinal3 :::"*^"::: )  (Set  "("  ($#k7_arytm_3 :::"denominator"::: )  "y" ")" ) ")" )); commutativity  
(Bool  "for" (Set (Var "b1")) "," (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  )  "st" (Bool (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k6_arytm_3 :::"numerator"::: )  (Set (Var "x")) ")" )  ($#k9_ordinal3 :::"*^"::: )  (Set  "("  ($#k6_arytm_3 :::"numerator"::: )  (Set (Var "y")) ")" ) ")" )  ($#k8_arytm_3 :::"/"::: )  (Set  "(" (Set  "("  ($#k7_arytm_3 :::"denominator"::: )  (Set (Var "x")) ")" )  ($#k9_ordinal3 :::"*^"::: )  (Set  "("  ($#k7_arytm_3 :::"denominator"::: )  (Set (Var "y")) ")" ) ")" )))) "holds"  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k6_arytm_3 :::"numerator"::: )  (Set (Var "y")) ")" )  ($#k9_ordinal3 :::"*^"::: )  (Set  "("  ($#k6_arytm_3 :::"numerator"::: )  (Set (Var "x")) ")" ) ")" )  ($#k8_arytm_3 :::"/"::: )  (Set  "(" (Set  "("  ($#k7_arytm_3 :::"denominator"::: )  (Set (Var "y")) ")" )  ($#k9_ordinal3 :::"*^"::: )  (Set  "("  ($#k7_arytm_3 :::"denominator"::: )  (Set (Var "x")) ")" ) ")" ))))
 ; end; 












:: deftheorem    defines :::"+"::: ARYTM_3:def 11 :  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) "holds"  (Bool (Set (Set (Var "x"))  ($#k9_arytm_3 :::"+"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "("  ($#k6_arytm_3 :::"numerator"::: )  (Set (Var "x")) ")" )  ($#k9_ordinal3 :::"*^"::: )  (Set  "("  ($#k7_arytm_3 :::"denominator"::: )  (Set (Var "y")) ")" ) ")" )  ($#k8_ordinal3 :::"+^"::: )  (Set  "(" (Set  "("  ($#k6_arytm_3 :::"numerator"::: )  (Set (Var "y")) ")" )  ($#k9_ordinal3 :::"*^"::: )  (Set  "("  ($#k7_arytm_3 :::"denominator"::: )  (Set (Var "x")) ")" ) ")" ) ")" )  ($#k8_arytm_3 :::"/"::: )  (Set  "(" (Set  "("  ($#k7_arytm_3 :::"denominator"::: )  (Set (Var "x")) ")" )  ($#k9_ordinal3 :::"*^"::: )  (Set  "("  ($#k7_arytm_3 :::"denominator"::: )  (Set (Var "y")) ")" ) ")" )))); 
 
:: deftheorem    defines :::"*'"::: ARYTM_3:def 12 :  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) "holds"  (Bool (Set (Set (Var "x"))  ($#k10_arytm_3 :::"*'"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k6_arytm_3 :::"numerator"::: )  (Set (Var "x")) ")" )  ($#k9_ordinal3 :::"*^"::: )  (Set  "("  ($#k6_arytm_3 :::"numerator"::: )  (Set (Var "y")) ")" ) ")" )  ($#k8_arytm_3 :::"/"::: )  (Set  "(" (Set  "("  ($#k7_arytm_3 :::"denominator"::: )  (Set (Var "x")) ")" )  ($#k9_ordinal3 :::"*^"::: )  (Set  "("  ($#k7_arytm_3 :::"denominator"::: )  (Set (Var "y")) ")" ) ")" )))); 
 
theorem :: ARYTM_3:46 (Bool  "for" (Set (Var "l")) "," (Set (Var "j")) "," (Set (Var "i")) "," (Set (Var "k")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "j"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "l"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "i"))  ($#k8_arytm_3 :::"/"::: )  (Set (Var "j")) ")" )  ($#k9_arytm_3 :::"+"::: )  (Set  "(" (Set (Var "k"))  ($#k8_arytm_3 :::"/"::: )  (Set (Var "l")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "i"))  ($#k9_ordinal3 :::"*^"::: )  (Set (Var "l")) ")" )  ($#k8_ordinal3 :::"+^"::: )  (Set  "(" (Set (Var "j"))  ($#k9_ordinal3 :::"*^"::: )  (Set (Var "k")) ")" ) ")" )  ($#k8_arytm_3 :::"/"::: )  (Set  "(" (Set (Var "j"))  ($#k9_ordinal3 :::"*^"::: )  (Set (Var "l")) ")" )))) ; 
 
theorem :: ARYTM_3:47 (Bool  "for" (Set (Var "k")) "," (Set (Var "i")) "," (Set (Var "j")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "i"))  ($#k8_arytm_3 :::"/"::: )  (Set (Var "k")) ")" )  ($#k9_arytm_3 :::"+"::: )  (Set  "(" (Set (Var "j"))  ($#k8_arytm_3 :::"/"::: )  (Set (Var "k")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "i"))  ($#k8_ordinal3 :::"+^"::: )  (Set (Var "j")) ")" )  ($#k8_arytm_3 :::"/"::: )  (Set (Var "k"))))) ; 
 registration
cluster   ($#v1_xboole_0 :::"empty"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ); 
end; definition:: original: :::"{}"::: redefine func  :::"{}":::  ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ); :: original: :::"one"::: redefine func  :::"one":::  ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ); end; 
theorem :: ARYTM_3:48 (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) "holds"  (Bool (Set (Set (Var "x"))  ($#k10_arytm_3 :::"*'"::: )  (Set  ($#k11_arytm_3 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k11_arytm_3 :::"{}"::: )  ))) ; 
 
theorem :: ARYTM_3:49 (Bool  "for" (Set (Var "l")) "," (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being"   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::) "holds"  (Bool (Set (Set  "(" (Set (Var "i"))  ($#k8_arytm_3 :::"/"::: )  (Set (Var "j")) ")" )  ($#k10_arytm_3 :::"*'"::: )  (Set  "(" (Set (Var "k"))  ($#k8_arytm_3 :::"/"::: )  (Set (Var "l")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "i"))  ($#k9_ordinal3 :::"*^"::: )  (Set (Var "k")) ")" )  ($#k8_arytm_3 :::"/"::: )  (Set  "(" (Set (Var "j"))  ($#k9_ordinal3 :::"*^"::: )  (Set (Var "l")) ")" )))) ; 
 
theorem :: ARYTM_3:50 (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) "holds"  (Bool (Set (Set (Var "x"))  ($#k9_arytm_3 :::"+"::: )  (Set  ($#k11_arytm_3 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "x")))) ; 
 
theorem :: ARYTM_3:51 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k9_arytm_3 :::"+"::: )  (Set (Var "y")) ")" )  ($#k9_arytm_3 :::"+"::: )  (Set (Var "z")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k9_arytm_3 :::"+"::: )  (Set  "(" (Set (Var "y"))  ($#k9_arytm_3 :::"+"::: )  (Set (Var "z")) ")" )))) ; 
 
theorem :: ARYTM_3:52 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k10_arytm_3 :::"*'"::: )  (Set (Var "y")) ")" )  ($#k10_arytm_3 :::"*'"::: )  (Set (Var "z")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k10_arytm_3 :::"*'"::: )  (Set  "(" (Set (Var "y"))  ($#k10_arytm_3 :::"*'"::: )  (Set (Var "z")) ")" )))) ; 
 
theorem :: ARYTM_3:53 (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) "holds"  (Bool (Set (Set (Var "x"))  ($#k10_arytm_3 :::"*'"::: )  (Set  ($#k12_arytm_3 :::"one"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "x")))) ; 
 
theorem :: ARYTM_3:54 (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  )  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k11_arytm_3 :::"{}"::: )  ))) "holds"  (Bool  "ex" (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) "st" (Bool (Set (Set (Var "x"))  ($#k10_arytm_3 :::"*'"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Num 1)))) ; 
 
theorem :: ARYTM_3:55 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  )  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k11_arytm_3 :::"{}"::: )  ))) "holds"  (Bool  "ex" (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) "st" (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k10_arytm_3 :::"*'"::: )  (Set (Var "z")))))) ; 
 
theorem :: ARYTM_3:56 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  )  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k11_arytm_3 :::"{}"::: )  )) & (Bool (Set (Set (Var "x"))  ($#k10_arytm_3 :::"*'"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k10_arytm_3 :::"*'"::: )  (Set (Var "z"))))) "holds"  (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Var "z")))) ; 
 
theorem :: ARYTM_3:57 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) "holds"  (Bool (Set (Set (Var "x"))  ($#k10_arytm_3 :::"*'"::: )  (Set  "(" (Set (Var "y"))  ($#k9_arytm_3 :::"+"::: )  (Set (Var "z")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k10_arytm_3 :::"*'"::: )  (Set (Var "y")) ")" )  ($#k9_arytm_3 :::"+"::: )  (Set  "(" (Set (Var "x"))  ($#k10_arytm_3 :::"*'"::: )  (Set (Var "z")) ")" )))) ; 
 
theorem :: ARYTM_3:58 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) "holds"  (Bool (Set (Set (Var "i"))  ($#k9_arytm_3 :::"+"::: )  (Set (Var "j")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i"))  ($#k8_ordinal3 :::"+^"::: )  (Set (Var "j"))))) ; 
 
theorem :: ARYTM_3:59 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) "holds"  (Bool (Set (Set (Var "i"))  ($#k10_arytm_3 :::"*'"::: )  (Set (Var "j")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i"))  ($#k9_ordinal3 :::"*^"::: )  (Set (Var "j"))))) ; 
 
theorem :: ARYTM_3:60 (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) (Bool  "ex" (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) "st" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "y"))  ($#k9_arytm_3 :::"+"::: )  (Set (Var "y")))))) ; 
 definitionlet "x", "y" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ); pred "x" :::"<='"::: "y" means :: ARYTM_3:def 13 (Bool  "ex" (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) "st" (Bool "y"  ($#r1_hidden :::"="::: )  (Set "x"  ($#k9_arytm_3 :::"+"::: )  (Set (Var "z"))))); connectedness  
(Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  )  "st" (Bool (Bool  "("   "for" (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  )  "holds" (Bool (Bool  "not" (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k9_arytm_3 :::"+"::: )  (Set (Var "z")))))  ")" )) "holds"  (Bool  "ex" (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) "st" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "y"))  ($#k9_arytm_3 :::"+"::: )  (Set (Var "z"))))))
 ; end; 





:: deftheorem    defines :::"<='"::: ARYTM_3:def 13 :  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r3_arytm_3 :::"<='"::: )  (Set (Var "y"))) "iff" (Bool  "ex" (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) "st" (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k9_arytm_3 :::"+"::: )  (Set (Var "z")))))  ")" )); 
 notationlet "x", "y" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ); antonym "y" :::"<"::: "x" for "x" :::"<='"::: "y"; end; 





theorem :: ARYTM_3:61 (Bool  "for" (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "holds" (Bool (Bool  "not" (Set  ($#k4_tarski :::"["::: ) (Set  ($#k11_arytm_3 :::"{}"::: ) ) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k5_arytm_3 :::"RAT+"::: )  )))) ; 
 
theorem :: ARYTM_3:62 (Bool  "for" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "r")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  )  "st" (Bool (Bool (Set (Set (Var "s"))  ($#k9_arytm_3 :::"+"::: )  (Set (Var "t")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k9_arytm_3 :::"+"::: )  (Set (Var "t"))))) "holds"  (Bool (Set (Var "s"))  ($#r1_hidden :::"="::: )  (Set (Var "r")))) ; 
 
theorem :: ARYTM_3:63 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  )  "st" (Bool (Bool (Set (Set (Var "r"))  ($#k9_arytm_3 :::"+"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set   ($#k11_arytm_3 :::"{}"::: )  ))) "holds"  (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set   ($#k11_arytm_3 :::"{}"::: )  ))) ; 
 
theorem :: ARYTM_3:64 (Bool  "for" (Set (Var "s")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) "holds"  (Bool (Set   ($#k11_arytm_3 :::"{}"::: )  )  ($#r3_arytm_3 :::"<='"::: )  (Set (Var "s")))) ; 
 
theorem :: ARYTM_3:65 (Bool  "for" (Set (Var "s")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  )  "st" (Bool (Bool (Set (Var "s"))  ($#r3_arytm_3 :::"<='"::: )  (Set   ($#k11_arytm_3 :::"{}"::: )  ))) "holds"  (Bool (Set (Var "s"))  ($#r1_hidden :::"="::: )  (Set   ($#k11_arytm_3 :::"{}"::: )  ))) ; 
 
theorem :: ARYTM_3:66 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  )  "st" (Bool (Bool (Set (Var "r"))  ($#r3_arytm_3 :::"<='"::: )  (Set (Var "s"))) & (Bool (Set (Var "s"))  ($#r3_arytm_3 :::"<='"::: )  (Set (Var "r")))) "holds"  (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Var "s")))) ; 
 
theorem :: ARYTM_3:67 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "t")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  )  "st" (Bool (Bool (Set (Var "r"))  ($#r3_arytm_3 :::"<='"::: )  (Set (Var "s"))) & (Bool (Set (Var "s"))  ($#r3_arytm_3 :::"<='"::: )  (Set (Var "t")))) "holds"  (Bool (Set (Var "r"))  ($#r3_arytm_3 :::"<='"::: )  (Set (Var "t")))) ; 
 
theorem :: ARYTM_3:68 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "r"))  ($#r3_arytm_3 :::"<"::: )  (Set (Var "s"))) "iff" (Bool  "("  (Bool (Set (Var "r"))  ($#r3_arytm_3 :::"<='"::: )  (Set (Var "s"))) & (Bool (Set (Var "r"))  ($#r1_hidden :::"<>"::: )  (Set (Var "s")))  ")" )  ")" )) ; 
 
theorem :: ARYTM_3:69 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "t")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  )  "st" (Bool (Bool  "("  (Bool  "("  (Bool (Set (Var "r"))  ($#r3_arytm_3 :::"<"::: )  (Set (Var "s"))) & (Bool (Set (Var "s"))  ($#r3_arytm_3 :::"<='"::: )  (Set (Var "t")))  ")" ) "or" (Bool  "("  (Bool (Set (Var "r"))  ($#r3_arytm_3 :::"<='"::: )  (Set (Var "s"))) & (Bool (Set (Var "s"))  ($#r3_arytm_3 :::"<"::: )  (Set (Var "t")))  ")" )  ")" )) "holds"  (Bool (Set (Var "r"))  ($#r3_arytm_3 :::"<"::: )  (Set (Var "t")))) ; 
 
theorem :: ARYTM_3:70 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "t")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  )  "st" (Bool (Bool (Set (Var "r"))  ($#r3_arytm_3 :::"<"::: )  (Set (Var "s"))) & (Bool (Set (Var "s"))  ($#r3_arytm_3 :::"<"::: )  (Set (Var "t")))) "holds"  (Bool (Set (Var "r"))  ($#r3_arytm_3 :::"<"::: )  (Set (Var "t")))) ; 
 
theorem :: ARYTM_3:71 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  )  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_ordinal1 :::"omega"::: )  )) & (Bool (Set (Set (Var "x"))  ($#k9_arytm_3 :::"+"::: )  (Set (Var "y")))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_ordinal1 :::"omega"::: )  ))) "holds"  (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_ordinal1 :::"omega"::: )  ))) ; 
 
theorem :: ARYTM_3:72 (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  )  (Bool  "for" (Set (Var "i")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r3_arytm_3 :::"<"::: )  (Set (Var "x"))) & (Bool (Set (Var "x"))  ($#r3_arytm_3 :::"<"::: )  (Set (Set (Var "i"))  ($#k9_arytm_3 :::"+"::: )  (Set  ($#k12_arytm_3 :::"one"::: ) )))) "holds"  (Bool  "not" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_ordinal1 :::"omega"::: )  ))))) ; 
 
theorem :: ARYTM_3:73 (Bool  "for" (Set (Var "t")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  )  "st" (Bool (Bool (Set (Var "t"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k11_arytm_3 :::"{}"::: )  ))) "holds"  (Bool  "ex" (Set (Var "r")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "r"))  ($#r3_arytm_3 :::"<"::: )  (Set (Var "t"))) & (Bool (Bool  "not" (Set (Var "r"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_ordinal1 :::"omega"::: )  )))  ")" ))) ; 
 
theorem :: ARYTM_3:74 (Bool  "for" (Set (Var "t")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) "holds"   (Bool  "("  (Bool  "{"  (Set (Var "s")) where s "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) : (Bool (Set (Var "s"))  ($#r3_arytm_3 :::"<"::: )  (Set (Var "t")))  "}"    ($#r2_hidden :::"in"::: )  (Set   ($#k5_arytm_3 :::"RAT+"::: )  )) "iff" (Bool (Set (Var "t"))  ($#r1_hidden :::"="::: )  (Set   ($#k11_arytm_3 :::"{}"::: )  ))  ")" )) ; 
 
theorem :: ARYTM_3:75 (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k5_arytm_3 :::"RAT+"::: ) )  "st" (Bool (Bool  "ex" (Set (Var "t")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "t"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "t"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k11_arytm_3 :::"{}"::: )  ))  ")" )) & (Bool  "("   "for" (Set (Var "r")) "," (Set (Var "s")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  )  "st" (Bool (Bool (Set (Var "r"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "s"))  ($#r3_arytm_3 :::"<='"::: )  (Set (Var "r")))) "holds"  (Bool (Set (Var "s"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))  ")" )) "holds"  (Bool  "ex" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "r3")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "r1"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "r2"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "r3"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "r1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "r2"))) & (Bool (Set (Var "r2"))  ($#r1_hidden :::"<>"::: )  (Set (Var "r3"))) & (Bool (Set (Var "r3"))  ($#r1_hidden :::"<>"::: )  (Set (Var "r1")))  ")" ))) ; 
 
theorem :: ARYTM_3:76 (Bool  "for" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "r")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) "holds"   (Bool  "("  (Bool (Set (Set (Var "s"))  ($#k9_arytm_3 :::"+"::: )  (Set (Var "t")))  ($#r3_arytm_3 :::"<='"::: )  (Set (Set (Var "r"))  ($#k9_arytm_3 :::"+"::: )  (Set (Var "t")))) "iff" (Bool (Set (Var "s"))  ($#r3_arytm_3 :::"<='"::: )  (Set (Var "r")))  ")" )) ; 
 
theorem :: ARYTM_3:77 (Bool  "for" (Set (Var "s")) "," (Set (Var "t")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) "holds"  (Bool (Set (Var "s"))  ($#r3_arytm_3 :::"<='"::: )  (Set (Set (Var "s"))  ($#k9_arytm_3 :::"+"::: )  (Set (Var "t"))))) ; 
 
theorem :: ARYTM_3:78 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  )  "holds"  (Bool  "("   "not" (Bool (Set (Set (Var "r"))  ($#k10_arytm_3 :::"*'"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set   ($#k11_arytm_3 :::"{}"::: )  )) "or" (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set   ($#k11_arytm_3 :::"{}"::: )  )) "or" (Bool (Set (Var "s"))  ($#r1_hidden :::"="::: )  (Set   ($#k11_arytm_3 :::"{}"::: )  ))  ")" )) ; 
 
theorem :: ARYTM_3:79 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "t")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  )  "st" (Bool (Bool (Set (Var "r"))  ($#r3_arytm_3 :::"<='"::: )  (Set (Set (Var "s"))  ($#k10_arytm_3 :::"*'"::: )  (Set (Var "t"))))) "holds"  (Bool  "ex" (Set (Var "t0")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s"))  ($#k10_arytm_3 :::"*'"::: )  (Set (Var "t0")))) & (Bool (Set (Var "t0"))  ($#r3_arytm_3 :::"<='"::: )  (Set (Var "t")))  ")" ))) ; 
 
theorem :: ARYTM_3:80 (Bool  "for" (Set (Var "t")) "," (Set (Var "s")) "," (Set (Var "r")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  )  "st" (Bool (Bool (Set (Var "t"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k11_arytm_3 :::"{}"::: )  )) & (Bool (Set (Set (Var "s"))  ($#k10_arytm_3 :::"*'"::: )  (Set (Var "t")))  ($#r3_arytm_3 :::"<='"::: )  (Set (Set (Var "r"))  ($#k10_arytm_3 :::"*'"::: )  (Set (Var "t"))))) "holds"  (Bool (Set (Var "s"))  ($#r3_arytm_3 :::"<='"::: )  (Set (Var "r")))) ; 
 
theorem :: ARYTM_3:81 (Bool  "for" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "s1")) "," (Set (Var "s2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  )  "holds"  (Bool  "("   "not" (Bool (Set (Set (Var "r1"))  ($#k9_arytm_3 :::"+"::: )  (Set (Var "r2")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s1"))  ($#k9_arytm_3 :::"+"::: )  (Set (Var "s2")))) "or" (Bool (Set (Var "r1"))  ($#r3_arytm_3 :::"<='"::: )  (Set (Var "s1"))) "or" (Bool (Set (Var "r2"))  ($#r3_arytm_3 :::"<='"::: )  (Set (Var "s2")))  ")" )) ; 
 
theorem :: ARYTM_3:82 (Bool  "for" (Set (Var "s")) "," (Set (Var "r")) "," (Set (Var "t")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  )  "st" (Bool (Bool (Set (Var "s"))  ($#r3_arytm_3 :::"<='"::: )  (Set (Var "r")))) "holds"  (Bool (Set (Set (Var "s"))  ($#k10_arytm_3 :::"*'"::: )  (Set (Var "t")))  ($#r3_arytm_3 :::"<='"::: )  (Set (Set (Var "r"))  ($#k10_arytm_3 :::"*'"::: )  (Set (Var "t"))))) ; 
 
theorem :: ARYTM_3:83 (Bool  "for" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "s1")) "," (Set (Var "s2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  )  "holds"  (Bool  "("   "not" (Bool (Set (Set (Var "r1"))  ($#k10_arytm_3 :::"*'"::: )  (Set (Var "r2")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s1"))  ($#k10_arytm_3 :::"*'"::: )  (Set (Var "s2")))) "or" (Bool (Set (Var "r1"))  ($#r3_arytm_3 :::"<='"::: )  (Set (Var "s1"))) "or" (Bool (Set (Var "r2"))  ($#r3_arytm_3 :::"<='"::: )  (Set (Var "s2")))  ")" )) ; 
 
theorem :: ARYTM_3:84 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set   ($#k11_arytm_3 :::"{}"::: )  )) "iff" (Bool (Set (Set (Var "r"))  ($#k9_arytm_3 :::"+"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set (Var "s")))  ")" )) ; 
 
theorem :: ARYTM_3:85 (Bool  "for" (Set (Var "s1")) "," (Set (Var "t1")) "," (Set (Var "s2")) "," (Set (Var "t2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  )  "st" (Bool (Bool (Set (Set (Var "s1"))  ($#k9_arytm_3 :::"+"::: )  (Set (Var "t1")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s2"))  ($#k9_arytm_3 :::"+"::: )  (Set (Var "t2")))) & (Bool (Set (Var "s1"))  ($#r3_arytm_3 :::"<='"::: )  (Set (Var "s2")))) "holds"  (Bool (Set (Var "t2"))  ($#r3_arytm_3 :::"<='"::: )  (Set (Var "t1")))) ; 
 
theorem :: ARYTM_3:86 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "t")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  )  "st" (Bool (Bool (Set (Var "r"))  ($#r3_arytm_3 :::"<='"::: )  (Set (Var "s"))) & (Bool (Set (Var "s"))  ($#r3_arytm_3 :::"<='"::: )  (Set (Set (Var "r"))  ($#k9_arytm_3 :::"+"::: )  (Set (Var "t"))))) "holds"  (Bool  "ex" (Set (Var "t0")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "s"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k9_arytm_3 :::"+"::: )  (Set (Var "t0")))) & (Bool (Set (Var "t0"))  ($#r3_arytm_3 :::"<='"::: )  (Set (Var "t")))  ")" ))) ; 
 
theorem :: ARYTM_3:87 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "t")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  )  "st" (Bool (Bool (Set (Var "r"))  ($#r3_arytm_3 :::"<='"::: )  (Set (Set (Var "s"))  ($#k9_arytm_3 :::"+"::: )  (Set (Var "t"))))) "holds"  (Bool  "ex" (Set (Var "s0")) "," (Set (Var "t0")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s0"))  ($#k9_arytm_3 :::"+"::: )  (Set (Var "t0")))) & (Bool (Set (Var "s0"))  ($#r3_arytm_3 :::"<='"::: )  (Set (Var "s"))) & (Bool (Set (Var "t0"))  ($#r3_arytm_3 :::"<='"::: )  (Set (Var "t")))  ")" ))) ; 
 
theorem :: ARYTM_3:88 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "t")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  )  "st" (Bool (Bool (Set (Var "r"))  ($#r3_arytm_3 :::"<"::: )  (Set (Var "s"))) & (Bool (Set (Var "r"))  ($#r3_arytm_3 :::"<"::: )  (Set (Var "t")))) "holds"  (Bool  "ex" (Set (Var "t0")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "t0"))  ($#r3_arytm_3 :::"<='"::: )  (Set (Var "s"))) & (Bool (Set (Var "t0"))  ($#r3_arytm_3 :::"<='"::: )  (Set (Var "t"))) & (Bool (Set (Var "r"))  ($#r3_arytm_3 :::"<"::: )  (Set (Var "t0")))  ")" ))) ; 
 
theorem :: ARYTM_3:89 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "t")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  )  "st" (Bool (Bool (Set (Var "r"))  ($#r3_arytm_3 :::"<='"::: )  (Set (Var "s"))) & (Bool (Set (Var "s"))  ($#r3_arytm_3 :::"<='"::: )  (Set (Var "t"))) & (Bool (Set (Var "s"))  ($#r1_hidden :::"<>"::: )  (Set (Var "t")))) "holds"  (Bool (Set (Var "r"))  ($#r1_hidden :::"<>"::: )  (Set (Var "t")))) ; 
 
theorem :: ARYTM_3:90 (Bool  "for" (Set (Var "s")) "," (Set (Var "r")) "," (Set (Var "t")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  )  "st" (Bool (Bool (Set (Var "s"))  ($#r3_arytm_3 :::"<"::: )  (Set (Set (Var "r"))  ($#k9_arytm_3 :::"+"::: )  (Set (Var "t")))) & (Bool (Set (Var "t"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k11_arytm_3 :::"{}"::: )  ))) "holds"  (Bool  "ex" (Set (Var "r0")) "," (Set (Var "t0")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "s"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r0"))  ($#k9_arytm_3 :::"+"::: )  (Set (Var "t0")))) & (Bool (Set (Var "r0"))  ($#r3_arytm_3 :::"<='"::: )  (Set (Var "r"))) & (Bool (Set (Var "t0"))  ($#r3_arytm_3 :::"<='"::: )  (Set (Var "t"))) & (Bool (Set (Var "t0"))  ($#r1_hidden :::"<>"::: )  (Set (Var "t")))  ")" ))) ; 
 
theorem :: ARYTM_3:91 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k5_arytm_3 :::"RAT+"::: ) )  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set   ($#k5_arytm_3 :::"RAT+"::: )  ))) "holds"  (Bool  "ex" (Set (Var "s")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "s"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool  "("   "for" (Set (Var "r")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  )  "st" (Bool (Bool (Set (Var "r"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))) "holds"  (Bool (Set (Var "r"))  ($#r3_arytm_3 :::"<='"::: )  (Set (Var "s")))  ")" )  ")" ))) ; 
 
theorem :: ARYTM_3:92 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) (Bool  "ex" (Set (Var "t")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) "st"  (Bool  "("  (Bool (Set (Set (Var "r"))  ($#k9_arytm_3 :::"+"::: )  (Set (Var "t")))  ($#r1_hidden :::"="::: )  (Set (Var "s"))) "or" (Bool (Set (Set (Var "s"))  ($#k9_arytm_3 :::"+"::: )  (Set (Var "t")))  ($#r1_hidden :::"="::: )  (Set (Var "r")))  ")" ))) ; 
 
theorem :: ARYTM_3:93 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  )  "st" (Bool (Bool (Set (Var "r"))  ($#r3_arytm_3 :::"<"::: )  (Set (Var "s")))) "holds"  (Bool  "ex" (Set (Var "t")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "r"))  ($#r3_arytm_3 :::"<"::: )  (Set (Var "t"))) & (Bool (Set (Var "t"))  ($#r3_arytm_3 :::"<"::: )  (Set (Var "s")))  ")" ))) ; 
 
theorem :: ARYTM_3:94 (Bool  "for" (Set (Var "r")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) (Bool  "ex" (Set (Var "s")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) "st" (Bool (Set (Var "r"))  ($#r3_arytm_3 :::"<"::: )  (Set (Var "s"))))) ; 
 
theorem :: ARYTM_3:95 (Bool  "for" (Set (Var "t")) "," (Set (Var "r")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  )  "st" (Bool (Bool (Set (Var "t"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k11_arytm_3 :::"{}"::: )  ))) "holds"  (Bool  "ex" (Set (Var "s")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "s"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_ordinal1 :::"omega"::: )  )) & (Bool (Set (Var "r"))  ($#r3_arytm_3 :::"<='"::: )  (Set (Set (Var "s"))  ($#k10_arytm_3 :::"*'"::: )  (Set (Var "t"))))  ")" ))) ; 
 scheme  :: ARYTM_3:sch 1 DisNat{ F1() ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ), F2() ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ), F3() ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ), P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "ex" (Set (Var "s")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_arytm_3 :::"RAT+"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "s"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_ordinal1 :::"omega"::: )  )) & (Bool P1[(Set (Var "s"))]) & (Bool P1[(Set (Set (Var "s"))  ($#k9_arytm_3 :::"+"::: )  (Set F2 "("  ")" ))])  ")" ))
 provided
(Bool (Set F2 "("  ")" )  ($#r1_hidden :::"="::: )  (Num 1))
 and  
(Bool (Set F1 "("  ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k11_arytm_3 :::"{}"::: )  ))
 and  
(Bool (Set F3 "("  ")" )  ($#r2_hidden :::"in"::: )  (Set   ($#k4_ordinal1 :::"omega"::: )  ))
 and  
(Bool P1[(Set F1 "("  ")" )])
 and  
(Bool P1[(Set F3 "("  ")" )])
 proof 


end;