:: NAT_1  semantic presentation begin  




















theorem :: NAT_1:1 (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))  ")" )) "holds"  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))))) ; 
 registrationlet "n", "k" be   ($#m1_hidden :::"Nat":::); 
cluster (Set "n"  ($#k2_xcmplx_0 :::"+"::: )  "k") ->   ($#v7_ordinal1 :::"natural"::: )   ; 
end; definitionlet "n" be   ($#m1_hidden :::"Nat":::); let "k" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); :: original: :::"+"::: redefine func "n" :::"+"::: "k" ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); end; definitionlet "n" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "k" be   ($#m1_hidden :::"Nat":::); :: original: :::"+"::: redefine func "n" :::"+"::: "k" ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); end; scheme  :: NAT_1:sch 1 Ind{ P1[  ($#m1_hidden :::"Nat":::)] } : 
(Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool P1[(Set (Var "k"))]))
 provided
(Bool P1[(Set   ($#k6_numbers :::"0"::: )  )])
 and  
(Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool P1[(Set (Var "k"))])) "holds"  (Bool P1[(Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1))]))
 proof 


end; scheme  :: NAT_1:sch 2 NatInd{ P1[  ($#m1_hidden :::"Nat":::)] } : 
(Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool P1[(Set (Var "k"))]))
 provided
(Bool P1[(Set   ($#k6_numbers :::"0"::: )  )])
 and  
(Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool P1[(Set (Var "k"))])) "holds"  (Bool P1[(Set (Set (Var "k"))  ($#k1_nat_1 :::"+"::: )  (Num 1))]))
 proof 


end; registrationlet "n", "k" be   ($#m1_hidden :::"Nat":::); 
cluster (Set "n"  ($#k3_xcmplx_0 :::"*"::: )  "k") ->   ($#v7_ordinal1 :::"natural"::: )   ; 
end; definitionlet "n" be   ($#m1_hidden :::"Nat":::); let "k" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); :: original: :::"*"::: redefine func "n" :::"*"::: "k" ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); end; definitionlet "n" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "k" be   ($#m1_hidden :::"Nat":::); :: original: :::"*"::: redefine func "n" :::"*"::: "k" ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); end; 
theorem :: NAT_1:2 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i")))) ; 
 
theorem :: NAT_1:3 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_hidden :::"<>"::: )  (Set (Var "i")))) "holds"  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "i")))) ; 
 
theorem :: NAT_1:4 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "h")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j")))) "holds"  (Bool (Set (Set (Var "i"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "h")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "j"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "h"))))) ; 
 
theorem :: NAT_1:5 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "holds" (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "i"))  ($#k1_nat_1 :::"+"::: )  (Num 1)))) ; 
 
theorem :: NAT_1:6 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "holds"  (Bool  "("  (Bool (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool  "ex" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "st" (Bool (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k1_nat_1 :::"+"::: )  (Num 1))))  ")" )) ; 
 
theorem :: NAT_1:7 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "j")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "j"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) ; 
 registration
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )    ($#v1_ordinal1 :::"epsilon-transitive"::: )     ($#v2_ordinal1 :::"epsilon-connected"::: )     ($#v3_ordinal1 :::"ordinal"::: )     ($#v7_ordinal1 :::"natural"::: )     ($#v1_xcmplx_0 :::"complex"::: )     ($#v1_xxreal_0 :::"ext-real"::: )     ($#v1_xreal_0 :::"real"::: )     ($#v1_finset_1 :::"finite"::: )     ($#v1_card_1 :::"cardinal"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registrationlet "m" be   ($#m1_hidden :::"Nat":::); let "n" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )   ($#m1_hidden :::"Nat":::); 
cluster (Set "m"  ($#k2_xcmplx_0 :::"+"::: )  "n") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )  ; 

cluster (Set "n"  ($#k2_xcmplx_0 :::"+"::: )  "m") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )  ; 
end; scheme  :: NAT_1:sch 3 DefbyInd{ F1() ->   ($#m1_hidden :::"Nat":::), F2(  ($#m1_hidden :::"Nat":::) ","   ($#m1_hidden :::"Nat":::)) ->   ($#m1_hidden :::"Nat":::), P1[  ($#m1_hidden :::"Nat":::) ","   ($#m1_hidden :::"Nat":::)] } : 
(Bool  "("  (Bool  "("   "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) (Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "st" (Bool P1[(Set (Var "k")) "," (Set (Var "n"))]))  ")" ) & (Bool  "("   "for" (Set (Var "k")) "," (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool P1[(Set (Var "k")) "," (Set (Var "n"))]) & (Bool P1[(Set (Var "k")) "," (Set (Var "m"))])) "holds"  (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set (Var "m")))  ")" )  ")" )
 provided
(Bool  "for" (Set (Var "k")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool P1[(Set (Var "k")) "," (Set (Var "n"))]) "iff" (Bool  "("  (Bool  "("  (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" ))  ")" ) "or" (Bool  "ex" (Set (Var "m")) "," (Set (Var "l")) "being"   ($#m1_hidden :::"Nat":::) "st"  (Bool  "("  (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k1_nat_1 :::"+"::: )  (Num 1))) & (Bool P1[(Set (Var "m")) "," (Set (Var "l"))]) & (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set F2 "(" (Set (Var "k")) "," (Set (Var "l")) ")" ))  ")" ))  ")" )  ")" ))
 proof 


end; 
theorem :: NAT_1:8 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_hidden :::"Nat":::)  "holds"  (Bool  "("   "not" (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "j"))  ($#k1_nat_1 :::"+"::: )  (Num 1))) "or" (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) "or" (Bool (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "j"))  ($#k1_nat_1 :::"+"::: )  (Num 1)))  ")" )) ; 
 
theorem :: NAT_1:9 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "i"))  ($#k1_nat_1 :::"+"::: )  (Num 1))) & (Bool (Bool  "not" (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Set (Var "j"))))) "holds"  (Bool (Set (Var "j"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i"))  ($#k1_nat_1 :::"+"::: )  (Num 1)))) ; 
 
theorem :: NAT_1:10 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j")))) "holds"  (Bool  "ex" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "st" (Bool (Set (Var "j"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "k")))))) ; 
 
theorem :: NAT_1:11 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "j"))))) ; 
 scheme  :: NAT_1:sch 4 CompInd{ P1[  ($#m1_hidden :::"Nat":::)] } : 
(Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool P1[(Set (Var "k"))]))
 provided
(Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "k")))) "holds"  (Bool P1[(Set (Var "n"))])  ")" )) "holds"  (Bool P1[(Set (Var "k"))]))
 proof 


end; scheme  :: NAT_1:sch 5 Min{ P1[  ($#m1_hidden :::"Nat":::)] } : 
(Bool  "ex" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "st"  (Bool  "("  (Bool P1[(Set (Var "k"))]) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool P1[(Set (Var "n"))])) "holds"  (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))  ")" )  ")" ))
 provided
(Bool  "ex" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "st" (Bool P1[(Set (Var "k"))]))
 proof 


end; scheme  :: NAT_1:sch 6 Max{ P1[  ($#m1_hidden :::"Nat":::)], F1() ->   ($#m1_hidden :::"Nat":::) } : 
(Bool  "ex" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "st"  (Bool  "("  (Bool P1[(Set (Var "k"))]) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool P1[(Set (Var "n"))])) "holds"  (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k")))  ")" )  ")" ))
 provided
(Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool P1[(Set (Var "k"))])) "holds"  (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set F1 "("  ")" )))
 and  
(Bool  "ex" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "st" (Bool P1[(Set (Var "k"))]))
 proof 


end; 
theorem :: NAT_1:12 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "h")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j")))) "holds"  (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "j"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "h"))))) ; 
 
theorem :: NAT_1:13 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "j"))  ($#k1_nat_1 :::"+"::: )  (Num 1))) "iff" (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j")))  ")" )) ; 
 
theorem :: NAT_1:14 (Bool  "for" (Set (Var "j")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<"::: )  (Num 1))) "holds"  (Bool (Set (Var "j"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: NAT_1:15 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Set (Var "i"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "j")))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: NAT_1:16 (Bool  "for" (Set (Var "k")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "k"))))) ; 
 scheme  :: NAT_1:sch 7 Regr{ P1[  ($#m1_hidden :::"Nat":::)] } : 
(Bool P1[(Set   ($#k6_numbers :::"0"::: )  )])
 provided
(Bool  "ex" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "st" (Bool P1[(Set (Var "k"))]))
 and  
(Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool P1[(Set (Var "k"))])) "holds"  (Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "st"  (Bool  "("  (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "k"))) & (Bool P1[(Set (Var "n"))])  ")" )))
 proof 


end; 
theorem :: NAT_1:17 (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "m")))) "holds"  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) (Bool  "ex" (Set (Var "k")) "," (Set (Var "t")) "being"   ($#m1_hidden :::"Nat":::) "st"  (Bool  "("  (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "m"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "k")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "t")))) & (Bool (Set (Var "t"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "m")))  ")" )))) ; 
 
theorem :: NAT_1:18 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "k")) "," (Set (Var "t")) "," (Set (Var "k1")) "," (Set (Var "t1")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "m"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "k")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "t")))) & (Bool (Set (Var "t"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "m"))) & (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "m"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "k1")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "t1")))) & (Bool (Set (Var "t1"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "m")))) "holds"  (Bool  "("  (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Set (Var "k1"))) & (Bool (Set (Var "t"))  ($#r1_hidden :::"="::: )  (Set (Var "t1")))  ")" )) ; 
 registration
cluster   ($#v7_ordinal1 :::"natural"::: )    ->   ($#v3_ordinal1 :::"ordinal"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registration
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v3_ordinal1 :::"ordinal"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set  ($#k1_numbers :::"REAL"::: ) ))); 
end; 
theorem :: NAT_1:19 (Bool  "for" (Set (Var "k")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "k"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "n")))) "iff" (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))  ")" )) ; 
 
theorem :: NAT_1:20 (Bool  "for" (Set (Var "k")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set (Var "n"))  ($#k6_xcmplx_0 :::"-"::: )  (Num 1)) "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ))) ; 
 
theorem :: NAT_1:21 (Bool  "for" (Set (Var "k")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set (Var "n"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "k"))) "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ))) ; 
 begin  
theorem :: NAT_1:22 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds"  (Bool  "("   "not" (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1))) "or" (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n"))) "or" (Bool (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set (Var "n")))  ")" )) ; 
 
theorem :: NAT_1:23 (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "holds"  (Bool  "("   "not" (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<"::: )  (Num 2)) "or" (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Num 1))  ")" )) ; 
 registration
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )    ($#v1_ordinal1 :::"epsilon-transitive"::: )     ($#v2_ordinal1 :::"epsilon-connected"::: )     ($#v3_ordinal1 :::"ordinal"::: )     ($#v7_ordinal1 :::"natural"::: )     ($#v1_xcmplx_0 :::"complex"::: )     ($#v1_xxreal_0 :::"ext-real"::: )     ($#v1_xreal_0 :::"real"::: )     ($#v1_finset_1 :::"finite"::: )     ($#v1_card_1 :::"cardinal"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 
end; registration
cluster   ->  ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )   for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 
end; registration
cluster   ($#v7_ordinal1 :::"natural"::: )    ->  ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )   for    ($#m1_hidden :::"set"::: )  ; 
end; 
theorem :: NAT_1:24 (Bool  "for" (Set (Var "i")) "," (Set (Var "h")) "," (Set (Var "j")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "h"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "j"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "i"))))) "holds"  (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "h")))) ; 
 scheme  :: NAT_1:sch 8 Ind1{ F1() ->   ($#m1_hidden :::"Nat":::), P1[  ($#m1_hidden :::"Nat":::)] } : 
(Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set F1 "("  ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i")))) "holds"  (Bool P1[(Set (Var "i"))]))
 provided
(Bool P1[(Set F1 "("  ")" )])
 and  
(Bool  "for" (Set (Var "j")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set F1 "("  ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool P1[(Set (Var "j"))])) "holds"  (Bool P1[(Set (Set (Var "j"))  ($#k1_nat_1 :::"+"::: )  (Num 1))]))
 proof 


end; scheme  :: NAT_1:sch 9 CompInd1{ F1() ->   ($#m1_hidden :::"Nat":::), P1[  ($#m1_hidden :::"Nat":::)] } : 
(Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Set F1 "("  ")" ))) "holds"  (Bool P1[(Set (Var "k"))]))
 provided
(Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Set F1 "("  ")" )) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Set F1 "("  ")" )) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "k")))) "holds"  (Bool P1[(Set (Var "n"))])  ")" )) "holds"  (Bool P1[(Set (Var "k"))]))
 proof 


end; 
theorem :: NAT_1:25 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds"  (Bool  "("   "not" (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Num 1)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 1))  ")" )) ; 
 
theorem :: NAT_1:26 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds"  (Bool  "("   "not" (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Num 2)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 1)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 2))  ")" )) ; 
 
theorem :: NAT_1:27 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds"  (Bool  "("   "not" (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Num 3)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 1)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 2)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 3))  ")" )) ; 
 
theorem :: NAT_1:28 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds"  (Bool  "("   "not" (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Num 4)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 1)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 2)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 3)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 4))  ")" )) ; 
 
theorem :: NAT_1:29 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds"  (Bool  "("   "not" (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Num 5)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 1)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 2)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 3)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 4)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 5))  ")" )) ; 
 
theorem :: NAT_1:30 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds"  (Bool  "("   "not" (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Num 6)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 1)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 2)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 3)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 4)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 5)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 6))  ")" )) ; 
 
theorem :: NAT_1:31 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds"  (Bool  "("   "not" (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Num 7)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 1)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 2)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 3)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 4)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 5)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 6)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 7))  ")" )) ; 
 
theorem :: NAT_1:32 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds"  (Bool  "("   "not" (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Num 8)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 1)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 2)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 3)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 4)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 5)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 6)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 7)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 8))  ")" )) ; 
 
theorem :: NAT_1:33 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds"  (Bool  "("   "not" (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Num 9)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 1)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 2)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 3)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 4)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 5)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 6)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 7)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 8)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 9))  ")" )) ; 
 
theorem :: NAT_1:34 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds"  (Bool  "("   "not" (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Num 10)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 1)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 2)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 3)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 4)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 5)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 6)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 7)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 8)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 9)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 10))  ")" )) ; 
 
theorem :: NAT_1:35 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds"  (Bool  "("   "not" (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Num 11)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 1)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 2)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 3)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 4)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 5)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 6)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 7)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 8)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 9)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 10)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 11))  ")" )) ; 
 
theorem :: NAT_1:36 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds"  (Bool  "("   "not" (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Num 12)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 1)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 2)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 3)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 4)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 5)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 6)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 7)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 8)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 9)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 10)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 11)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 12))  ")" )) ; 
 
theorem :: NAT_1:37 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds"  (Bool  "("   "not" (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Num 13)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 1)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 2)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 3)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 4)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 5)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 6)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 7)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 8)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 9)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 10)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 11)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 12)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 13))  ")" )) ; 
 scheme  :: NAT_1:sch 10 Indfrom1{ P1[  ($#m1_hidden :::"Nat":::)] } : 
(Bool  "for" (Set (Var "k")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::) "holds"  (Bool P1[(Set (Var "k"))]))
 provided
(Bool P1[(Num 1)])
 and  
(Bool  "for" (Set (Var "k")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool P1[(Set (Var "k"))])) "holds"  (Bool P1[(Set (Set (Var "k"))  ($#k1_nat_1 :::"+"::: )  (Num 1))]))
 proof 


end; definitionlet "A" be    ($#m1_hidden :::"set"::: )  ; func  :::"min*"::: "A" ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) means :: NAT_1:def 1 (Bool  "("  (Bool it  ($#r2_hidden :::"in"::: )  "A") & (Bool  "("   "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  "A")) "holds"  (Bool it  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k")))  ")" )  ")" ) if (Bool "A" "is"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ))  otherwise (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )); end; 





:: deftheorem    defines :::"min*"::: NAT_1:def 1 :  (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b2")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "A")) "is"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ))) "implies" (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_nat_1 :::"min*"::: )  (Set (Var "A")))) "iff" (Bool  "("  (Bool (Set (Var "b2"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool  "("   "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))) "holds"  (Bool (Set (Var "b2"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k")))  ")" )  ")" )  ")" )  ")"  &  "("  (Bool (Bool (Set (Var "A")) "is" (Bool  "not"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) )))) "implies" (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_nat_1 :::"min*"::: )  (Set (Var "A")))) "iff" (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")"   ")" ))); 
 






theorem :: NAT_1:38 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k4_card_1 :::"succ"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1)))) ; 
 
theorem :: NAT_1:39 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m"))) "iff" (Bool (Set (Var "n"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "m")))  ")" )) ; 
 
theorem :: NAT_1:40 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "n")))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "m")))) "iff" (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m")))  ")" )) ; 
 
theorem :: NAT_1:41 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "n")))  ($#r2_hidden :::"in"::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "m")))) "iff" (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "m")))  ")" )) ; 
 




theorem :: NAT_1:42 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k2_card_1 :::"nextcard"::: )  (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" )))) ; 
 definitionlet "n" be   ($#m1_hidden :::"Nat":::); redefine func  :::"succ"::: "n" equals :: NAT_1:def 2 (Set "n"  ($#k1_nat_1 :::"+"::: )  (Num 1)); end; 





:: deftheorem    defines :::"succ"::: NAT_1:def 2 :  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1)))); 
 
theorem :: NAT_1:43 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))) "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "X")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "Y"))))) ; 
 



theorem :: NAT_1:44 (Bool  "for" (Set (Var "k")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set (Var "n"))) "iff" (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n")))  ")" )) ; 
 
theorem :: NAT_1:45 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1)))) ; 
 
theorem :: NAT_1:46 (Bool  "for" (Set (Var "k")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "n"))))) ; 
 scheme  :: NAT_1:sch 11 LambdaRecEx{ F1() ->    ($#m1_hidden :::"set"::: )  , F2(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )   } : 
(Bool  "ex" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "st"  (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_numbers :::"NAT"::: )  )) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" )) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set F2 "(" (Set (Var "n")) "," (Set  "(" (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")) ")" ) ")" ))  ")" )  ")" ))
 proof 


end; scheme  :: NAT_1:sch 12 LambdaRecExD{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2() ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ), F3(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) } : 
(Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set F1 "("  ")" ) "st"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set F2 "("  ")" )) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "n")) "," (Set  "(" (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")) ")" ) ")" ))  ")" )  ")" ))
 proof 


end; scheme  :: NAT_1:sch 13 RecUn{ F1() ->    ($#m1_hidden :::"set"::: )  , F2() ->   ($#m1_hidden :::"Function":::), F3() ->   ($#m1_hidden :::"Function":::), P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool (Set F2 "("  ")" )  ($#r1_hidden :::"="::: )  (Set F3 "("  ")" ))
 provided
(Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set F2 "("  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_numbers :::"NAT"::: )  ))
 and  
(Bool (Set (Set F2 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" ))
 and  
(Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool P1[(Set (Var "n")) "," (Set (Set F2 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "n"))) "," (Set (Set F2 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))]))
 and  
(Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set F3 "("  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_numbers :::"NAT"::: )  ))
 and  
(Bool (Set (Set F3 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" ))
 and  
(Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool P1[(Set (Var "n")) "," (Set (Set F3 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "n"))) "," (Set (Set F3 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))]))
 and  
(Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool P1[(Set (Var "n")) "," (Set (Var "x")) "," (Set (Var "y1"))]) & (Bool P1[(Set (Var "n")) "," (Set (Var "x")) "," (Set (Var "y2"))])) "holds"  (Bool (Set (Var "y1"))  ($#r1_hidden :::"="::: )  (Set (Var "y2")))))
 proof 


end; scheme  :: NAT_1:sch 14 RecUnD{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2() ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ), P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ], F3() ->   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set F1 "("  ")" ), F4() ->   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set F1 "("  ")" ) } : 
(Bool (Set F3 "("  ")" )  ($#r2_funct_2 :::"="::: )  (Set F4 "("  ")" ))
 provided
(Bool (Set (Set F3 "("  ")" )  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set F2 "("  ")" ))
 and  
(Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool P1[(Set (Var "n")) "," (Set (Set F3 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "n"))) "," (Set (Set F3 "("  ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))]))
 and  
(Bool (Set (Set F4 "("  ")" )  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set F2 "("  ")" ))
 and  
(Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool P1[(Set (Var "n")) "," (Set (Set F4 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "n"))) "," (Set (Set F4 "("  ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))]))
 and  
(Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  "st" (Bool (Bool P1[(Set (Var "n")) "," (Set (Var "x")) "," (Set (Var "y1"))]) & (Bool P1[(Set (Var "n")) "," (Set (Var "x")) "," (Set (Var "y2"))])) "holds"  (Bool (Set (Var "y1"))  ($#r1_hidden :::"="::: )  (Set (Var "y2")))))
 proof 


end; scheme  :: NAT_1:sch 15 LambdaRecUn{ F1() ->    ($#m1_hidden :::"set"::: )  , F2(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )  , F3() ->   ($#m1_hidden :::"Function":::), F4() ->   ($#m1_hidden :::"Function":::) } : 
(Bool (Set F3 "("  ")" )  ($#r1_hidden :::"="::: )  (Set F4 "("  ")" ))
 provided
(Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set F3 "("  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_numbers :::"NAT"::: )  ))
 and  
(Bool (Set (Set F3 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" ))
 and  
(Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set F3 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set F2 "(" (Set (Var "n")) "," (Set  "(" (Set F3 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "n")) ")" ) ")" )))
 and  
(Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set F4 "("  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_numbers :::"NAT"::: )  ))
 and  
(Bool (Set (Set F4 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" ))
 and  
(Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set F4 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set F2 "(" (Set (Var "n")) "," (Set  "(" (Set F4 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "n")) ")" ) ")" )))
 proof 


end; scheme  :: NAT_1:sch 16 LambdaRecUnD{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2() ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ), F3(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ), F4() ->   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set F1 "("  ")" ), F5() ->   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set F1 "("  ")" ) } : 
(Bool (Set F4 "("  ")" )  ($#r2_funct_2 :::"="::: )  (Set F5 "("  ")" ))
 provided
(Bool (Set (Set F4 "("  ")" )  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set F2 "("  ")" ))
 and  
(Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set F4 "("  ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "n")) "," (Set  "(" (Set F4 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "n")) ")" ) ")" )))
 and  
(Bool (Set (Set F5 "("  ")" )  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set F2 "("  ")" ))
 and  
(Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set F5 "("  ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "n")) "," (Set  "(" (Set F5 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "n")) ")" ) ")" )))
 proof 


end; registrationlet "x", "y" be   ($#m1_hidden :::"Nat":::); 
cluster (Set   ($#k3_xxreal_0 :::"min"::: )   "(" "x" "," "y" ")" ) ->   ($#v7_ordinal1 :::"natural"::: )   ; 

cluster (Set   ($#k4_xxreal_0 :::"max"::: )   "(" "x" "," "y" ")" ) ->   ($#v7_ordinal1 :::"natural"::: )   ; 
end; definitionlet "x", "y" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); :: original: :::"min"::: redefine func  :::"min":::  "(" "x" "," "y" ")"  ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); :: original: :::"max"::: redefine func  :::"max":::  "(" "x" "," "y" ")"  ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); end; scheme  :: NAT_1:sch 17 MinIndex{ F1(  ($#m1_hidden :::"Nat":::)) ->   ($#m1_hidden :::"Nat":::) } : 
(Bool  "ex" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "st"  (Bool  "("  (Bool (Set F1 "(" (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set F1 "(" (Set (Var "n")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))  ")" )  ")" ))
 provided
(Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "holds"  (Bool  "("  (Bool (Set F1 "(" (Set  "(" (Set (Var "k"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#r1_xxreal_0 :::"<"::: )  (Set F1 "(" (Set (Var "k")) ")" )) "or" (Bool (Set F1 "(" (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ))
 proof 


end; definitionlet "D" be    ($#m1_hidden :::"set"::: )  ; let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set (Const "D")); let "n" be   ($#m1_hidden :::"Nat":::); :: original: :::"."::: redefine func "f" :::"."::: "n" ->    ($#m1_subset_1 :::"Element"::: )   "of" "D"; end; definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; mode sequence of "X" is   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "," "X"; end; definitionlet "s" be   ($#m1_hidden :::"ManySortedSet":::) "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "k" be   ($#m1_hidden :::"Nat":::); func "s" :::"^\"::: "k" ->   ($#m1_hidden :::"ManySortedSet":::) "of" (Set   ($#k5_numbers :::"NAT"::: )  ) means :: NAT_1:def 3 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set "s"  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  "k" ")" )))); end; 






:: deftheorem    defines :::"^\"::: NAT_1:def 3 :  (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s"))  ($#k9_nat_1 :::"^\"::: )  (Set (Var "k")))) "iff" (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "b3"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "k")) ")" ))))  ")" )))); 
 registrationlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "s" be (Set (Const "X"))  ($#v5_relat_1 :::"-valued"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "k" be   ($#m1_hidden :::"Nat":::); 
cluster (Set "s"  ($#k9_nat_1 :::"^\"::: )  "k") -> "X"  ($#v5_relat_1 :::"-valued"::: )   ; 
end; definitionlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "s" be   ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); let "k" be   ($#m1_hidden :::"Nat":::); :: original: :::"^\"::: redefine func "s" :::"^\"::: "k" ->   ($#m1_subset_1 :::"sequence":::) "of" "X"; end; 










theorem :: NAT_1:47 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "s"))  ($#k10_nat_1 :::"^\"::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r2_funct_2 :::"="::: )  (Set (Var "s"))))) ; 
 
theorem :: NAT_1:48 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "k")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Set (Var "s"))  ($#k10_nat_1 :::"^\"::: )  (Set (Var "k")) ")" )  ($#k10_nat_1 :::"^\"::: )  (Set (Var "m")))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "s"))  ($#k10_nat_1 :::"^\"::: )  (Set  "(" (Set (Var "k"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "m")) ")" )))))) ; 
 
theorem :: NAT_1:49 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "k")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Set (Var "s"))  ($#k10_nat_1 :::"^\"::: )  (Set (Var "k")) ")" )  ($#k10_nat_1 :::"^\"::: )  (Set (Var "m")))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "s"))  ($#k10_nat_1 :::"^\"::: )  (Set (Var "m")) ")" )  ($#k10_nat_1 :::"^\"::: )  (Set (Var "k"))))))) ; 
 registrationlet "N" be   ($#m1_subset_1 :::"sequence":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ); let "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "s" be   ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); 
cluster (Set "N"  ($#k3_relat_1 :::"*"::: )  "s") -> (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )   "X"  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )   ; 
end; registrationlet "N" be   ($#m1_subset_1 :::"sequence":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ); let "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "s" be   ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); 
cluster (Set "N"  ($#k3_relat_1 :::"*"::: )  "s") ->   ($#v1_partfun1 :::"total"::: )   ; 
end; 
theorem :: NAT_1:50 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "N")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "holds"  (Bool (Set (Set  "(" (Set (Var "s"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "N")) ")" )  ($#k10_nat_1 :::"^\"::: )  (Set (Var "k")))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "s"))  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set (Var "N"))  ($#k10_nat_1 :::"^\"::: )  (Set (Var "k")) ")" ))))))) ; 
 
theorem :: NAT_1:51 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "s"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "s"))))))) ; 
 
theorem :: NAT_1:52 (Bool  "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "s"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r2_hidden :::"in"::: )  (Set (Var "Y")))  ")" )) "holds"  (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "s")))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))))) ; 
 
theorem :: NAT_1:53 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds"  (Bool  "("  (Bool (Set (Var "n")) "is"   ($#v1_xboole_0 :::"zero"::: )  ) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 1)) "or" (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Num 1))  ")" )) ; 
 
theorem :: NAT_1:54 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "l")) where l "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool (Set (Var "l"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))  "}"  )) ; 
 scheme  :: NAT_1:sch 18 MinPred{ F1(   ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )) ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ), P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "ex" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool P1[(Set (Var "k"))]) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool P1[(Set (Var "n"))])) "holds"  (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))  ")" )  ")" ))
 provided
(Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "holds"  (Bool  "("  (Bool (Set F1 "(" (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#r1_xxreal_0 :::"<"::: )  (Set F1 "(" (Set (Var "k")) ")" )) "or" (Bool P1[(Set (Var "k"))])  ")" ))
 proof 


end; registrationlet "k" be   ($#m1_hidden :::"Ordinal":::); let "x" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set "k"  ($#k2_funcop_1 :::"-->"::: )  "x") ->   ($#v5_ordinal1 :::"T-Sequence-like"::: )   ; 
end; 
theorem :: NAT_1:55 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "(" (Set (Var "s"))  ($#k9_nat_1 :::"^\"::: )  (Set (Var "k")) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "s")))))) ; 
 
theorem :: NAT_1:56 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m"))) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 2))) & (Bool (Bool  "not" (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set (Var "n")))) & (Bool (Bool  "not" (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1))))) "holds"  (Bool (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 2))))) ; 
 
theorem :: NAT_1:57 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m"))) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 3))) & (Bool (Bool  "not" (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set (Var "n")))) & (Bool (Bool  "not" (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1)))) & (Bool (Bool  "not" (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 2))))) "holds"  (Bool (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 3))))) ; 
 
theorem :: NAT_1:58 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m"))) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 4))) & (Bool (Bool  "not" (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set (Var "n")))) & (Bool (Bool  "not" (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1)))) & (Bool (Bool  "not" (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 2)))) & (Bool (Bool  "not" (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 3))))) "holds"  (Bool (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 4))))) ; 
 
theorem :: NAT_1:59 (Bool  "for" (Set (Var "X")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "X"))))) "holds"  (Bool  "ex" (Set (Var "x1")) "," (Set (Var "x2")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "x1"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "x2"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "x1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x2")))  ")" ))) ; 
 
theorem :: NAT_1:60 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds"  (Bool  "("   "not" (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Num 14)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 1)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 2)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 3)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 4)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 5)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 6)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 7)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 8)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 9)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 10)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 11)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 12)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 13)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 14))  ")" )) ;