:: HEYTING3  semantic presentation begin  scheme  :: HEYTING3:sch 1 SSubsetUniq{ F1() ->    ($#l1_struct_0 :::"1-sorted"::: )  , P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "for" (Set (Var "A1")) "," (Set (Var "A2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "("  ")" )  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "A1"))) "iff" (Bool P1[(Set (Var "x"))])  ")" )  ")" ) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "A2"))) "iff" (Bool P1[(Set (Var "x"))])  ")" )  ")" )) "holds"  (Bool (Set (Var "A1"))  ($#r1_hidden :::"="::: )  (Set (Var "A2"))))
 proof 


end; registrationlet "A", "x" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set  ($#k2_zfmisc_1 :::"[:"::: ) "A" "," (Set  ($#k1_tarski :::"{"::: ) "x" ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ->   ($#v1_funct_1 :::"Function-like"::: )   ; 
end; 
theorem :: HEYTING3:1 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) (Bool  "ex" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st" (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")) ")" )  ($#k1_finsub_1 :::"\/"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k6_domain_1 :::"}"::: ) ))))) ; 
 
theorem :: HEYTING3:2 (Bool  "for" (Set (Var "X")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) )  "holds"  (Bool  "not" (Bool  "for" (Set (Var "k")) "being"   ($#v1_abian :::"odd"::: )     ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))))) ; 
 
theorem :: HEYTING3:3 (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k8_mcart_1 :::"[:"::: ) (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "k")) ($#k6_domain_1 :::"}"::: ) ) ($#k8_mcart_1 :::":]"::: ) ) (Bool  "ex" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st" (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set  ($#k8_mcart_1 :::"[:"::: ) (Set  "(" (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")) ")" )  ($#k1_finsub_1 :::"\/"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k6_domain_1 :::"}"::: ) ) ")" ) "," (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "k")) ($#k6_domain_1 :::"}"::: ) ) ($#k8_mcart_1 :::":]"::: ) ))))) ; 
 
theorem :: HEYTING3:4 (Bool  "for" (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k8_mcart_1 :::"[:"::: ) (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "m")) ($#k6_domain_1 :::"}"::: ) ) ($#k8_mcart_1 :::":]"::: ) )  "holds"  (Bool  "not" (Bool  "for" (Set (Var "k")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set  ($#k1_domain_1 :::"["::: ) (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "k")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "m")) ($#k1_domain_1 :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "X"))))))) ; 
 
theorem :: HEYTING3:5 (Bool  "for" (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k8_mcart_1 :::"[:"::: ) (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "m")) ($#k6_domain_1 :::"}"::: ) ) ($#k8_mcart_1 :::":]"::: ) ) (Bool  "ex" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "for" (Set (Var "l")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "l"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "k")))) "holds"  (Bool  "not" (Bool (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "l")) "," (Set (Var "m")) ($#k1_domain_1 :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "X")))))))) ; 
 
theorem :: HEYTING3:6 (Bool  "for" (Set (Var "L")) "being"   ($#v14_lattices :::"upper-bounded"::: )    ($#l3_lattices :::"Lattice":::) "holds"  (Bool (Set   ($#k6_lattices :::"Top"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_yellow_0 :::"Top"::: )  (Set  "("  ($#k3_lattice3 :::"LattPOSet"::: )  (Set (Var "L")) ")" )))) ; 
 
theorem :: HEYTING3:7 (Bool  "for" (Set (Var "L")) "being"   ($#v13_lattices :::"lower-bounded"::: )    ($#l3_lattices :::"Lattice":::) "holds"  (Bool (Set   ($#k5_lattices :::"Bottom"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_yellow_0 :::"Bottom"::: )  (Set  "("  ($#k3_lattice3 :::"LattPOSet"::: )  (Set (Var "L")) ")" )))) ; 
 begin  
theorem :: HEYTING3:8 (Bool  "for" (Set (Var "V")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "C")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set  "("  ($#k4_partfun1 :::"PFuncs"::: )   "(" (Set (Var "V")) "," (Set (Var "C")) ")"  ")" ))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "B"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool (Set (Set (Var "B"))  ($#k3_heyting2 :::"=>>"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))))) ; 
 
theorem :: HEYTING3:9 (Bool  "for" (Set (Var "V")) "," (Set (Var "V9")) "," (Set (Var "C")) "," (Set (Var "C9")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "V"))  ($#r1_tarski :::"c="::: )  (Set (Var "V9"))) & (Bool (Set (Var "C"))  ($#r1_tarski :::"c="::: )  (Set (Var "C9")))) "holds"  (Bool (Set   ($#k1_substlat :::"SubstitutionSet"::: )   "(" (Set (Var "V")) "," (Set (Var "C")) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_substlat :::"SubstitutionSet"::: )   "(" (Set (Var "V9")) "," (Set (Var "C9")) ")" ))) ; 
 
theorem :: HEYTING3:10 (Bool  "for" (Set (Var "V")) "," (Set (Var "V9")) "," (Set (Var "C")) "," (Set (Var "C9")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set  "("  ($#k4_partfun1 :::"PFuncs"::: )   "(" (Set (Var "V")) "," (Set (Var "C")) ")"  ")" ))  (Bool  "for" (Set (Var "B")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set  "("  ($#k4_partfun1 :::"PFuncs"::: )   "(" (Set (Var "V9")) "," (Set (Var "C9")) ")"  ")" ))  "st" (Bool (Bool (Set (Var "V"))  ($#r1_tarski :::"c="::: )  (Set (Var "V9"))) & (Bool (Set (Var "C"))  ($#r1_tarski :::"c="::: )  (Set (Var "C9"))) & (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Var "B")))) "holds"  (Bool (Set   ($#k3_substlat :::"mi"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_substlat :::"mi"::: )  (Set (Var "B"))))))) ; 
 
theorem :: HEYTING3:11 (Bool  "for" (Set (Var "V")) "," (Set (Var "V9")) "," (Set (Var "C")) "," (Set (Var "C9")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "V"))  ($#r1_tarski :::"c="::: )  (Set (Var "V9"))) & (Bool (Set (Var "C"))  ($#r1_tarski :::"c="::: )  (Set (Var "C9")))) "holds"  (Bool (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" (Set  "("  ($#k5_substlat :::"SubstLatt"::: )   "(" (Set (Var "V")) "," (Set (Var "C")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" (Set  "("  ($#k5_substlat :::"SubstLatt"::: )   "(" (Set (Var "V9")) "," (Set (Var "C9")) ")"  ")" ))  ($#k1_realset1 :::"||"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k5_substlat :::"SubstLatt"::: )   "(" (Set (Var "V")) "," (Set (Var "C")) ")"  ")" ))))) ; 
 definitionlet "V", "C" be    ($#m1_hidden :::"set"::: )  ; func  :::"SubstPoset":::  "(" "V" "," "C" ")"  ->    ($#l1_orders_2 :::"RelStr"::: )   equals :: HEYTING3:def 1 (Set   ($#k3_lattice3 :::"LattPOSet"::: )  (Set  "("  ($#k5_substlat :::"SubstLatt"::: )   "(" "V" "," "C" ")"  ")" )); end; 






:: deftheorem    defines :::"SubstPoset"::: HEYTING3:def 1 :  (Bool  "for" (Set (Var "V")) "," (Set (Var "C")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_heyting3 :::"SubstPoset"::: )   "(" (Set (Var "V")) "," (Set (Var "C")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_lattice3 :::"LattPOSet"::: )  (Set  "("  ($#k5_substlat :::"SubstLatt"::: )   "(" (Set (Var "V")) "," (Set (Var "C")) ")"  ")" )))); 
 registrationlet "V", "C" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k1_heyting3 :::"SubstPoset"::: )   "(" "V" "," "C" ")" ) ->   ($#v1_lattice3 :::"with_suprema"::: )     ($#v2_lattice3 :::"with_infima"::: )   ; 
end; registrationlet "V", "C" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k1_heyting3 :::"SubstPoset"::: )   "(" "V" "," "C" ")" ) ->   ($#v3_orders_2 :::"reflexive"::: )     ($#v4_orders_2 :::"transitive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )   ; 
end; 
theorem :: HEYTING3:12 (Bool  "for" (Set (Var "V")) "," (Set (Var "C")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k1_heyting3 :::"SubstPoset"::: )   "(" (Set (Var "V")) "," (Set (Var "C")) ")"  ")" ) "holds"   (Bool  "("  (Bool (Set (Var "a"))  ($#r3_orders_2 :::"<="::: )  (Set (Var "b"))) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "a")))) "holds"  (Bool  "ex" (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "b"))) & (Bool (Set (Var "y"))  ($#r1_tarski :::"c="::: )  (Set (Var "x")))  ")" )))  ")" ))) ; 
 
theorem :: HEYTING3:13 (Bool  "for" (Set (Var "V")) "," (Set (Var "V9")) "," (Set (Var "C")) "," (Set (Var "C9")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "V"))  ($#r1_tarski :::"c="::: )  (Set (Var "V9"))) & (Bool (Set (Var "C"))  ($#r1_tarski :::"c="::: )  (Set (Var "C9")))) "holds"  (Bool (Set   ($#k1_heyting3 :::"SubstPoset"::: )   "(" (Set (Var "V")) "," (Set (Var "C")) ")" ) "is"   ($#v4_yellow_0 :::"full"::: )     ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set   ($#k1_heyting3 :::"SubstPoset"::: )   "(" (Set (Var "V9")) "," (Set (Var "C9")) ")" ))) ; 
 definitionlet "n", "k" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); func  :::"PFArt":::  "(" "n" "," "k" ")"  ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k4_partfun1 :::"PFuncs"::: )   "(" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k6_domain_1 :::"{"::: ) "k" ($#k6_domain_1 :::"}"::: ) ) ")" ) means :: HEYTING3:def 2 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "("  (Bool  "ex" (Set (Var "m")) "being"   ($#v1_abian :::"odd"::: )     ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Num 2)  ($#k4_nat_1 :::"*"::: )  "n")) & (Bool (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "m")) "," "k" ($#k1_domain_1 :::"]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Var "x")))  ")" )) "or" (Bool (Set  ($#k1_domain_1 :::"["::: ) (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  "n" ")" ) "," "k" ($#k1_domain_1 :::"]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Var "x")))  ")" )  ")" )); end; 






:: deftheorem    defines :::"PFArt"::: HEYTING3:def 2 :  (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "b3")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k4_partfun1 :::"PFuncs"::: )   "(" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "k")) ($#k6_domain_1 :::"}"::: ) ) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_heyting3 :::"PFArt"::: )   "(" (Set (Var "n")) "," (Set (Var "k")) ")" )) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b3"))) "iff" (Bool  "("  (Bool  "ex" (Set (Var "m")) "being"   ($#v1_abian :::"odd"::: )     ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")))) & (Bool (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "m")) "," (Set (Var "k")) ($#k1_domain_1 :::"]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Var "x")))  ")" )) "or" (Bool (Set  ($#k1_domain_1 :::"["::: ) (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" ) "," (Set (Var "k")) ($#k1_domain_1 :::"]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Var "x")))  ")" )  ")" ))  ")" ))); 
 registrationlet "n", "k" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 
cluster (Set   ($#k2_heyting3 :::"PFArt"::: )   "(" "n" "," "k" ")" ) ->   ($#v1_finset_1 :::"finite"::: )   ; 
end; definitionlet "n", "k" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); func  :::"PFCrt":::  "(" "n" "," "k" ")"  ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k4_partfun1 :::"PFuncs"::: )   "(" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k6_domain_1 :::"{"::: ) "k" ($#k6_domain_1 :::"}"::: ) ) ")" ) means :: HEYTING3:def 3 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "ex" (Set (Var "m")) "being"   ($#v1_abian :::"odd"::: )     ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  "n" ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1))) & (Bool (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "m")) "," "k" ($#k1_domain_1 :::"]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Var "x")))  ")" ))  ")" )); end; 






:: deftheorem    defines :::"PFCrt"::: HEYTING3:def 3 :  (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "b3")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k4_partfun1 :::"PFuncs"::: )   "(" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "k")) ($#k6_domain_1 :::"}"::: ) ) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_heyting3 :::"PFCrt"::: )   "(" (Set (Var "n")) "," (Set (Var "k")) ")" )) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b3"))) "iff" (Bool  "ex" (Set (Var "m")) "being"   ($#v1_abian :::"odd"::: )     ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1))) & (Bool (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "m")) "," (Set (Var "k")) ($#k1_domain_1 :::"]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Var "x")))  ")" ))  ")" ))  ")" ))); 
 registrationlet "n", "k" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 
cluster (Set   ($#k3_heyting3 :::"PFCrt"::: )   "(" "n" "," "k" ")" ) ->   ($#v1_finset_1 :::"finite"::: )   ; 
end; 
theorem :: HEYTING3:14 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set  ($#k1_domain_1 :::"["::: ) (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "k")) ($#k1_domain_1 :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k3_heyting3 :::"PFCrt"::: )   "(" (Set (Var "n")) "," (Set (Var "k")) ")" ))) ; 
 
theorem :: HEYTING3:15 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k3_heyting3 :::"PFCrt"::: )   "(" (Set (Var "n")) "," (Set (Var "k")) ")" )  ($#r1_xboole_0 :::"misses"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  ($#k1_domain_1 :::"["::: ) (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 3) ")" ) "," (Set (Var "k")) ($#k1_domain_1 :::"]"::: ) ) ($#k6_domain_1 :::"}"::: ) ))) ; 
 
theorem :: HEYTING3:16 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k3_heyting3 :::"PFCrt"::: )   "(" (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_heyting3 :::"PFCrt"::: )   "(" (Set (Var "n")) "," (Set (Var "k")) ")"  ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  ($#k1_domain_1 :::"["::: ) (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 3) ")" ) "," (Set (Var "k")) ($#k1_domain_1 :::"]"::: ) ) ($#k6_domain_1 :::"}"::: ) )))) ; 
 
theorem :: HEYTING3:17 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k3_heyting3 :::"PFCrt"::: )   "(" (Set (Var "n")) "," (Set (Var "k")) ")" )  ($#r2_xboole_0 :::"c<"::: )  (Set   ($#k3_heyting3 :::"PFCrt"::: )   "(" (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "k")) ")" ))) ; 
 registrationlet "n", "k" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 
cluster (Set   ($#k2_heyting3 :::"PFArt"::: )   "(" "n" "," "k" ")" ) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; 
theorem :: HEYTING3:18 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "holds" (Bool (Bool  "not" (Set   ($#k2_heyting3 :::"PFArt"::: )   "(" (Set (Var "n")) "," (Set (Var "m")) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k3_heyting3 :::"PFCrt"::: )   "(" (Set (Var "k")) "," (Set (Var "m")) ")" )))) ; 
 
theorem :: HEYTING3:19 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k")))) "holds"  (Bool (Set   ($#k3_heyting3 :::"PFCrt"::: )   "(" (Set (Var "n")) "," (Set (Var "m")) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k3_heyting3 :::"PFCrt"::: )   "(" (Set (Var "k")) "," (Set (Var "m")) ")" ))) ; 
 
theorem :: HEYTING3:20 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k2_heyting3 :::"PFArt"::: )   "(" (Num 1) "," (Set (Var "n")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k7_domain_1 :::"{"::: ) (Set  ($#k1_domain_1 :::"["::: ) (Num 1) "," (Set (Var "n")) ($#k1_domain_1 :::"]"::: ) ) "," (Set  ($#k1_domain_1 :::"["::: ) (Num 2) "," (Set (Var "n")) ($#k1_domain_1 :::"]"::: ) ) ($#k7_domain_1 :::"}"::: ) ))) ; 
 definitionlet "n", "k" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); func  :::"PFBrt":::  "(" "n" "," "k" ")"  ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set  "("  ($#k4_partfun1 :::"PFuncs"::: )   "(" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k6_domain_1 :::"{"::: ) "k" ($#k6_domain_1 :::"}"::: ) ) ")"  ")" )) means :: HEYTING3:def 4 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "("  (Bool  "ex" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  "n") & (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_heyting3 :::"PFArt"::: )   "(" (Set (Var "m")) "," "k" ")" ))  ")" )) "or" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_heyting3 :::"PFCrt"::: )   "(" "n" "," "k" ")" ))  ")" )  ")" )); end; 






:: deftheorem    defines :::"PFBrt"::: HEYTING3:def 4 :  (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "b3")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set  "("  ($#k4_partfun1 :::"PFuncs"::: )   "(" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "k")) ($#k6_domain_1 :::"}"::: ) ) ")"  ")" )) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_heyting3 :::"PFBrt"::: )   "(" (Set (Var "n")) "," (Set (Var "k")) ")" )) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b3"))) "iff" (Bool  "("  (Bool  "ex" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_heyting3 :::"PFArt"::: )   "(" (Set (Var "m")) "," (Set (Var "k")) ")" ))  ")" )) "or" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_heyting3 :::"PFCrt"::: )   "(" (Set (Var "n")) "," (Set (Var "k")) ")" ))  ")" )  ")" ))  ")" ))); 
 
theorem :: HEYTING3:21 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_heyting3 :::"PFBrt"::: )   "(" (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "k")) ")" ))) "holds"  (Bool  "ex" (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_heyting3 :::"PFBrt"::: )   "(" (Set (Var "n")) "," (Set (Var "k")) ")" )) & (Bool (Set (Var "y"))  ($#r1_tarski :::"c="::: )  (Set (Var "x")))  ")" )))) ; 
 
theorem :: HEYTING3:22 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "holds" (Bool (Bool  "not" (Set   ($#k3_heyting3 :::"PFCrt"::: )   "(" (Set (Var "n")) "," (Set (Var "k")) ")" )  ($#r2_hidden :::"in"::: )  (Set   ($#k4_heyting3 :::"PFBrt"::: )   "(" (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "k")) ")" )))) ; 
 
theorem :: HEYTING3:23 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set   ($#k2_heyting3 :::"PFArt"::: )   "(" (Set (Var "n")) "," (Set (Var "m")) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k2_heyting3 :::"PFArt"::: )   "(" (Set (Var "k")) "," (Set (Var "m")) ")" ))) "holds"  (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set (Var "k")))) ; 
 
theorem :: HEYTING3:24 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set   ($#k3_heyting3 :::"PFCrt"::: )   "(" (Set (Var "n")) "," (Set (Var "m")) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k2_heyting3 :::"PFArt"::: )   "(" (Set (Var "k")) "," (Set (Var "m")) ")" )) "iff" (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "k")))  ")" )) ; 
 begin  
theorem :: HEYTING3:25 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k4_heyting3 :::"PFBrt"::: )   "(" (Set (Var "n")) "," (Set (Var "k")) ")" ) "is"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k1_heyting3 :::"SubstPoset"::: )   "(" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "k")) ($#k6_domain_1 :::"}"::: ) ) ")"  ")" ))) ; 
 definitionlet "k" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); func  :::"PFDrt"::: "k" ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_heyting3 :::"SubstPoset"::: )   "(" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k6_domain_1 :::"{"::: ) "k" ($#k6_domain_1 :::"}"::: ) ) ")"  ")" ) means :: HEYTING3:def 5 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "ex" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_heyting3 :::"PFBrt"::: )   "(" (Set (Var "n")) "," "k" ")" )))  ")" )); end; 





:: deftheorem    defines :::"PFDrt"::: HEYTING3:def 5 :  (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_heyting3 :::"SubstPoset"::: )   "(" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "k")) ($#k6_domain_1 :::"}"::: ) ) ")"  ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_heyting3 :::"PFDrt"::: )  (Set (Var "k")))) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b2"))) "iff" (Bool  "ex" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_heyting3 :::"PFBrt"::: )   "(" (Set (Var "n")) "," (Set (Var "k")) ")" )))  ")" ))  ")" ))); 
 
theorem :: HEYTING3:26 (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k4_heyting3 :::"PFBrt"::: )   "(" (Num 1) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k7_domain_1 :::"{"::: ) (Set  "("  ($#k2_heyting3 :::"PFArt"::: )   "(" (Num 1) "," (Set (Var "k")) ")"  ")" ) "," (Set  "("  ($#k3_heyting3 :::"PFCrt"::: )   "(" (Num 1) "," (Set (Var "k")) ")"  ")" ) ($#k7_domain_1 :::"}"::: ) ))) ; 
 
theorem :: HEYTING3:27 (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "holds" (Bool (Set   ($#k4_heyting3 :::"PFBrt"::: )   "(" (Num 1) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"<>"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ))) ; 
 registrationlet "k" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 
cluster (Set   ($#k4_heyting3 :::"PFBrt"::: )   "(" (Num 1) "," "k" ")" ) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; 
theorem :: HEYTING3:28 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set  ($#k6_domain_1 :::"{"::: ) (Set  "("  ($#k2_heyting3 :::"PFArt"::: )   "(" (Set (Var "n")) "," (Set (Var "k")) ")"  ")" ) ($#k6_domain_1 :::"}"::: ) ) "is"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k1_heyting3 :::"SubstPoset"::: )   "(" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "k")) ($#k6_domain_1 :::"}"::: ) ) ")"  ")" ))) ; 
 
theorem :: HEYTING3:29 (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "V")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k1_heyting3 :::"SubstPoset"::: )   "(" (Set (Var "V")) "," (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "k")) ($#k6_domain_1 :::"}"::: ) ) ")"  ")" )  "st" (Bool (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set (Var "a")))) "holds"  (Bool (Set (Var "X")) "is"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "V")) "," (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "k")) ($#k6_domain_1 :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))))) ; 
 
theorem :: HEYTING3:30 (Bool  "for" (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k1_heyting3 :::"SubstPoset"::: )   "(" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "m")) ($#k6_domain_1 :::"}"::: ) ) ")"  ")" )  "st" (Bool (Bool (Set   ($#k5_heyting3 :::"PFDrt"::: )  (Set (Var "m")))  ($#r1_lattice3 :::"is_>=_than"::: )  (Set (Var "a")))) "holds"  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set (Var "a")))) "holds"  (Bool  "ex" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "n")) "," (Set (Var "m")) ($#k1_domain_1 :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Bool  "not" (Set (Var "n")) "is"   ($#v1_abian :::"odd"::: )  ))  ")" ))))) ; 
 
theorem :: HEYTING3:31 (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k1_heyting3 :::"SubstPoset"::: )   "(" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "k")) ($#k6_domain_1 :::"}"::: ) ) ")"  ")" )  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_heyting3 :::"SubstPoset"::: )   "(" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "k")) ($#k6_domain_1 :::"}"::: ) ) ")"  ")" )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_lattice3 :::"is_<=_than"::: )  (Set (Var "X"))) & (Bool (Set (Var "b"))  ($#r1_lattice3 :::"is_<=_than"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Set (Var "a"))  ($#k13_lattice3 :::""\/""::: )  (Set (Var "b")))  ($#r1_lattice3 :::"is_<=_than"::: )  (Set (Var "X")))))) ; 
 registrationlet "k" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   for    ($#m1_subset_1 :::"Element"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k1_heyting3 :::"SubstPoset"::: )   "(" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k6_domain_1 :::"{"::: ) "k" ($#k6_domain_1 :::"}"::: ) ) ")"  ")" )); 
end; 
theorem :: HEYTING3:32 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k1_heyting3 :::"SubstPoset"::: )   "(" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "n")) ($#k6_domain_1 :::"}"::: ) ) ")"  ")" )  "st" (Bool (Bool (Set   ($#k1_xboole_0 :::"{}"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Var "a")))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )))) ; 
 
theorem :: HEYTING3:33 (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "a")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k1_heyting3 :::"SubstPoset"::: )   "(" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "k")) ($#k6_domain_1 :::"}"::: ) ) ")"  ")" )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ))) "holds"  (Bool  "ex" (Set (Var "f")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_hidden :::"Function":::) "st"  (Bool  "("  (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set (Var "a"))) & (Bool (Set (Var "f"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" )))) ; 
 
theorem :: HEYTING3:34 (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "a")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k1_heyting3 :::"SubstPoset"::: )   "(" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "k")) ($#k6_domain_1 :::"}"::: ) ) ")"  ")" )  (Bool  "for" (Set (Var "a9")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set  "("  ($#k4_partfun1 :::"PFuncs"::: )   "(" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "k")) ($#k6_domain_1 :::"}"::: ) ) ")"  ")" ))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )) & (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "a9")))) "holds"  (Bool (Set   ($#k1_heyting2 :::"Involved"::: )  (Set (Var "a9"))) "is"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ))))) ; 
 
theorem :: HEYTING3:35 (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k1_heyting3 :::"SubstPoset"::: )   "(" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "k")) ($#k6_domain_1 :::"}"::: ) ) ")"  ")" )  (Bool  "for" (Set (Var "a9")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set  "("  ($#k4_partfun1 :::"PFuncs"::: )   "(" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "k")) ($#k6_domain_1 :::"}"::: ) ) ")"  ")" ))  (Bool  "for" (Set (Var "B")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) )  "st" (Bool (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_heyting2 :::"Involved"::: )  (Set (Var "a9")))) & (Bool (Set (Var "a9"))  ($#r1_hidden :::"="::: )  (Set (Var "a")))) "holds"  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set (Var "a")))) "holds"  (Bool  "for" (Set (Var "l")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "l"))  ($#r1_xxreal_0 :::">"::: )  (Set (Set  "("  ($#k1_xxreal_2 :::"max"::: )  (Set (Var "B")) ")" )  ($#k1_nat_1 :::"+"::: )  (Num 1)))) "holds"  (Bool  "not" (Bool (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "l")) "," (Set (Var "k")) ($#k1_domain_1 :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "X")))))))))) ; 
 
theorem :: HEYTING3:36 (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k4_yellow_0 :::"Top"::: )  (Set  "("  ($#k1_heyting3 :::"SubstPoset"::: )   "(" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "k")) ($#k6_domain_1 :::"}"::: ) ) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ))) ; 
 
theorem :: HEYTING3:37 (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k3_yellow_0 :::"Bottom"::: )  (Set  "("  ($#k1_heyting3 :::"SubstPoset"::: )   "(" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "k")) ($#k6_domain_1 :::"}"::: ) ) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: HEYTING3:38 (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k1_heyting3 :::"SubstPoset"::: )   "(" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "k")) ($#k6_domain_1 :::"}"::: ) ) ")"  ")" )  "st" (Bool (Bool (Set (Var "a"))  ($#r3_orders_2 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ))) "holds"  (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )))) ; 
 
theorem :: HEYTING3:39 (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k1_heyting3 :::"SubstPoset"::: )   "(" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "k")) ($#k6_domain_1 :::"}"::: ) ) ")"  ")" )  "st" (Bool (Bool (Set (Var "a"))  ($#r3_orders_2 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )))) ; 
 
theorem :: HEYTING3:40 (Bool  "for" (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k1_heyting3 :::"SubstPoset"::: )   "(" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "m")) ($#k6_domain_1 :::"}"::: ) ) ")"  ")" )  "st" (Bool (Bool (Set   ($#k5_heyting3 :::"PFDrt"::: )  (Set (Var "m")))  ($#r1_lattice3 :::"is_>=_than"::: )  (Set (Var "a")))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )))) ; 
 registrationlet "m" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 
cluster (Set   ($#k1_heyting3 :::"SubstPoset"::: )   "(" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k6_domain_1 :::"{"::: ) "m" ($#k6_domain_1 :::"}"::: ) ) ")" ) ->  ($#~v3_lattice3  "non"   ($#v3_lattice3 :::"complete"::: )   )  ; 
end; registrationlet "m" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 
cluster (Set   ($#k5_substlat :::"SubstLatt"::: )   "(" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k6_domain_1 :::"{"::: ) "m" ($#k6_domain_1 :::"}"::: ) ) ")" ) ->  ($#~v4_lattice3  "non"   ($#v4_lattice3 :::"complete"::: )   )  ; 
end;