:: FINSUB_1  semantic presentation begin  




definitionlet "IT" be    ($#m1_hidden :::"set"::: )  ; attr "IT" is  :::"cup-closed":::  means :: FINSUB_1:def 1 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  "IT") & (Bool (Set (Var "Y"))  ($#r2_hidden :::"in"::: )  "IT")) "holds"  (Bool (Set (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")))  ($#r2_hidden :::"in"::: )  "IT")); attr "IT" is  :::"cap-closed":::  means :: FINSUB_1:def 2 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  "IT") & (Bool (Set (Var "Y"))  ($#r2_hidden :::"in"::: )  "IT")) "holds"  (Bool (Set (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")))  ($#r2_hidden :::"in"::: )  "IT")); attr "IT" is  :::"diff-closed":::  means :: FINSUB_1:def 3 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  "IT") & (Bool (Set (Var "Y"))  ($#r2_hidden :::"in"::: )  "IT")) "holds"  (Bool (Set (Set (Var "X"))  ($#k6_subset_1 :::"\"::: )  (Set (Var "Y")))  ($#r2_hidden :::"in"::: )  "IT")); end; 












:: deftheorem    defines :::"cup-closed"::: FINSUB_1:def 1 :  (Bool  "for" (Set (Var "IT")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v1_finsub_1 :::"cup-closed"::: )  ) "iff" (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set (Var "IT"))) & (Bool (Set (Var "Y"))  ($#r2_hidden :::"in"::: )  (Set (Var "IT")))) "holds"  (Bool (Set (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")))  ($#r2_hidden :::"in"::: )  (Set (Var "IT"))))  ")" )); 
 
:: deftheorem    defines :::"cap-closed"::: FINSUB_1:def 2 :  (Bool  "for" (Set (Var "IT")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v2_finsub_1 :::"cap-closed"::: )  ) "iff" (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set (Var "IT"))) & (Bool (Set (Var "Y"))  ($#r2_hidden :::"in"::: )  (Set (Var "IT")))) "holds"  (Bool (Set (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")))  ($#r2_hidden :::"in"::: )  (Set (Var "IT"))))  ")" )); 
 
:: deftheorem    defines :::"diff-closed"::: FINSUB_1:def 3 :  (Bool  "for" (Set (Var "IT")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v3_finsub_1 :::"diff-closed"::: )  ) "iff" (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set (Var "IT"))) & (Bool (Set (Var "Y"))  ($#r2_hidden :::"in"::: )  (Set (Var "IT")))) "holds"  (Bool (Set (Set (Var "X"))  ($#k6_subset_1 :::"\"::: )  (Set (Var "Y")))  ($#r2_hidden :::"in"::: )  (Set (Var "IT"))))  ")" )); 
 definitionlet "IT" be    ($#m1_hidden :::"set"::: )  ; attr "IT" is  :::"preBoolean":::  means :: FINSUB_1:def 4 (Bool  "("  (Bool "IT" "is"   ($#v1_finsub_1 :::"cup-closed"::: )  ) & (Bool "IT" "is"   ($#v3_finsub_1 :::"diff-closed"::: )  )  ")" ); end; 




:: deftheorem    defines :::"preBoolean"::: FINSUB_1:def 4 :  (Bool  "for" (Set (Var "IT")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v4_finsub_1 :::"preBoolean"::: )  ) "iff" (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v1_finsub_1 :::"cup-closed"::: )  ) & (Bool (Set (Var "IT")) "is"   ($#v3_finsub_1 :::"diff-closed"::: )  )  ")" )  ")" )); 
 registration
cluster   ($#v4_finsub_1 :::"preBoolean"::: )    ->   ($#v1_finsub_1 :::"cup-closed"::: )     ($#v3_finsub_1 :::"diff-closed"::: )    for    ($#m1_hidden :::"set"::: )  ; 

cluster   ($#v1_finsub_1 :::"cup-closed"::: )     ($#v3_finsub_1 :::"diff-closed"::: )    ->   ($#v4_finsub_1 :::"preBoolean"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registration
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_finsub_1 :::"cup-closed"::: )     ($#v2_finsub_1 :::"cap-closed"::: )     ($#v3_finsub_1 :::"diff-closed"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; 
theorem :: FINSUB_1:1 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "A")) "is"   ($#v4_finsub_1 :::"preBoolean"::: )  ) "iff" (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "Y"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Set (Var "X"))  ($#k6_subset_1 :::"\"::: )  (Set (Var "Y")))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))  ")" ))  ")" )) ; 
 


definitionlet "A" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v4_finsub_1 :::"preBoolean"::: )     ($#m1_hidden :::"set"::: )  ; let "X", "Y" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "A")); :: original: :::"\/"::: redefine func "X" :::"\/"::: "Y" ->    ($#m1_subset_1 :::"Element"::: )   "of" "A"; :: original: :::"\"::: redefine func "X" :::"\"::: "Y" ->    ($#m1_subset_1 :::"Element"::: )   "of" "A"; end; 
theorem :: FINSUB_1:2 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v4_finsub_1 :::"preBoolean"::: )     ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X")) "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))) & (Bool (Set (Var "Y")) "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A")))) "holds"  (Bool (Set (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y"))) "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))))) ; 
 
theorem :: FINSUB_1:3 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v4_finsub_1 :::"preBoolean"::: )     ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X")) "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))) & (Bool (Set (Var "Y")) "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A")))) "holds"  (Bool (Set (Set (Var "X"))  ($#k5_xboole_0 :::"\+\"::: )  (Set (Var "Y"))) "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))))) ; 
 
theorem :: FINSUB_1:4 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A")) "holds"   (Bool  "("  (Bool (Set (Set (Var "X"))  ($#k5_xboole_0 :::"\+\"::: )  (Set (Var "Y")))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Set (Var "X"))  ($#k6_subset_1 :::"\"::: )  (Set (Var "Y")))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))  ")" )  ")" )) "holds"  (Bool (Set (Var "A")) "is"   ($#v4_finsub_1 :::"preBoolean"::: )  )) ; 
 
theorem :: FINSUB_1:5 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A")) "holds"   (Bool  "("  (Bool (Set (Set (Var "X"))  ($#k5_xboole_0 :::"\+\"::: )  (Set (Var "Y")))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))  ")" )  ")" )) "holds"  (Bool (Set (Var "A")) "is"   ($#v4_finsub_1 :::"preBoolean"::: )  )) ; 
 
theorem :: FINSUB_1:6 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A")) "holds"   (Bool  "("  (Bool (Set (Set (Var "X"))  ($#k5_xboole_0 :::"\+\"::: )  (Set (Var "Y")))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))  ")" )  ")" )) "holds"  (Bool (Set (Var "A")) "is"   ($#v4_finsub_1 :::"preBoolean"::: )  )) ; 
 definitionlet "A" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v4_finsub_1 :::"preBoolean"::: )     ($#m1_hidden :::"set"::: )  ; let "X", "Y" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "A")); :: original: :::"/\"::: redefine func "X" :::"/\"::: "Y" ->    ($#m1_subset_1 :::"Element"::: )   "of" "A"; :: original: :::"\+\"::: redefine func "X" :::"\+\"::: "Y" ->    ($#m1_subset_1 :::"Element"::: )   "of" "A"; end; 
theorem :: FINSUB_1:7 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v4_finsub_1 :::"preBoolean"::: )     ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_xboole_0 :::"{}"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Var "A")))) ; 
 
theorem :: FINSUB_1:8 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set (Var "A"))) "is"   ($#v4_finsub_1 :::"preBoolean"::: )  )) ; 
 registrationlet "A" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k1_zfmisc_1 :::"bool"::: )  "A") ->   ($#v4_finsub_1 :::"preBoolean"::: )   ; 
end; 
theorem :: FINSUB_1:9 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v4_finsub_1 :::"preBoolean"::: )     ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Bool  "not" (Set (Set (Var "A"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "B"))) "is"   ($#v1_xboole_0 :::"empty"::: )  )) & (Bool (Set (Set (Var "A"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "B"))) "is"   ($#v4_finsub_1 :::"preBoolean"::: )  )  ")" )) ; 
 definitionlet "A" be    ($#m1_hidden :::"set"::: )  ; func  :::"Fin"::: "A" ->   ($#v4_finsub_1 :::"preBoolean"::: )     ($#m1_hidden :::"set"::: )   means :: FINSUB_1:def 5 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "("  (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  "A") & (Bool (Set (Var "X")) "is"   ($#v1_finset_1 :::"finite"::: )  )  ")" )  ")" )); end; 





:: deftheorem    defines :::"Fin"::: FINSUB_1:def 5 :  (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b2")) "being"   ($#v4_finsub_1 :::"preBoolean"::: )     ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set (Var "A")))) "iff" (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set (Var "b2"))) "iff" (Bool  "("  (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "A"))) & (Bool (Set (Var "X")) "is"   ($#v1_finset_1 :::"finite"::: )  )  ")" )  ")" ))  ")" ))); 
 registrationlet "A" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k5_finsub_1 :::"Fin"::: )  "A") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v4_finsub_1 :::"preBoolean"::: )   ; 
end; registrationlet "A" be    ($#m1_hidden :::"set"::: )  ; 
cluster   ->   ($#v1_finset_1 :::"finite"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_finsub_1 :::"Fin"::: )  "A"); 
end; 
theorem :: FINSUB_1:10 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "B")))) "holds"  (Bool (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set (Var "A")))  ($#r1_tarski :::"c="::: )  (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set (Var "B"))))) ; 
 
theorem :: FINSUB_1:11 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set  "(" (Set (Var "A"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  (Set (Var "A")) ")" )  ($#k3_xboole_0 :::"/\"::: )  (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  (Set (Var "B")) ")" )))) ; 
 
theorem :: FINSUB_1:12 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  (Set (Var "A")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  (Set (Var "B")) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set  "(" (Set (Var "A"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "B")) ")" )))) ; 
 
theorem :: FINSUB_1:13 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set (Var "A")))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set (Var "A"))))) ; 
 
theorem :: FINSUB_1:14 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "A")) "is"   ($#v1_finset_1 :::"finite"::: )  )) "holds"  (Bool (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set (Var "A"))))) ; 
 
theorem :: FINSUB_1:15 (Bool (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )) ; 
 definitionlet "A" be    ($#m1_hidden :::"set"::: )  ; mode Finite_Subset of "A" is    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_finsub_1 :::"Fin"::: )  "A"); end; 
theorem :: FINSUB_1:16 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set (Var "A")) "holds"  (Bool (Set (Var "X")) "is"   ($#v1_finset_1 :::"finite"::: )  ))) ; 
 
theorem :: FINSUB_1:17 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set (Var "A")) "holds"  (Bool (Set (Var "X")) "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A"))))) ; 
 
theorem :: FINSUB_1:18 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v1_finset_1 :::"finite"::: )  )) "holds"  (Bool (Set (Var "X")) "is"   ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set (Var "A"))))) ;