:: HILBERT1 semantic presentation begin definitionlet "D" be ($#m1_hidden :::"set"::: ) ; attr "D" is :::"with_VERUM"::: means :: HILBERT1:def 1 (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ($#r2_hidden :::"in"::: ) "D"); end; :: deftheorem defines :::"with_VERUM"::: HILBERT1:def 1 : (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "D")) "is" ($#v1_hilbert1 :::"with_VERUM"::: ) ) "iff" (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) ")" )); definitionlet "D" be ($#m1_hidden :::"set"::: ) ; attr "D" is :::"with_implication"::: means :: HILBERT1:def 2 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "D") & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) "D")) "holds" (Bool (Set (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p")) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) "D")); end; :: deftheorem defines :::"with_implication"::: HILBERT1:def 2 : (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "D")) "is" ($#v2_hilbert1 :::"with_implication"::: ) ) "iff" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p")) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) ")" )); definitionlet "D" be ($#m1_hidden :::"set"::: ) ; attr "D" is :::"with_conjunction"::: means :: HILBERT1:def 3 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "D") & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) "D")) "holds" (Bool (Set (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Num 2) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p")) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) "D")); end; :: deftheorem defines :::"with_conjunction"::: HILBERT1:def 3 : (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "D")) "is" ($#v3_hilbert1 :::"with_conjunction"::: ) ) "iff" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Num 2) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p")) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) ")" )); definitionlet "D" be ($#m1_hidden :::"set"::: ) ; attr "D" is :::"with_propositional_variables"::: means :: HILBERT1:def 4 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Num 3) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ($#r2_hidden :::"in"::: ) "D")); end; :: deftheorem defines :::"with_propositional_variables"::: HILBERT1:def 4 : (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "D")) "is" ($#v4_hilbert1 :::"with_propositional_variables"::: ) ) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Num 3) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) ")" )); definitionlet "D" be ($#m1_hidden :::"set"::: ) ; attr "D" is :::"HP-closed"::: means :: HILBERT1:def 5 (Bool "(" (Bool "D" ($#r1_tarski :::"c="::: ) (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k13_finseq_1 :::"*"::: ) )) & (Bool "D" "is" ($#v1_hilbert1 :::"with_VERUM"::: ) ) & (Bool "D" "is" ($#v2_hilbert1 :::"with_implication"::: ) ) & (Bool "D" "is" ($#v3_hilbert1 :::"with_conjunction"::: ) ) & (Bool "D" "is" ($#v4_hilbert1 :::"with_propositional_variables"::: ) ) ")" ); end; :: deftheorem defines :::"HP-closed"::: HILBERT1:def 5 : (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "D")) "is" ($#v5_hilbert1 :::"HP-closed"::: ) ) "iff" (Bool "(" (Bool (Set (Var "D")) ($#r1_tarski :::"c="::: ) (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k13_finseq_1 :::"*"::: ) )) & (Bool (Set (Var "D")) "is" ($#v1_hilbert1 :::"with_VERUM"::: ) ) & (Bool (Set (Var "D")) "is" ($#v2_hilbert1 :::"with_implication"::: ) ) & (Bool (Set (Var "D")) "is" ($#v3_hilbert1 :::"with_conjunction"::: ) ) & (Bool (Set (Var "D")) "is" ($#v4_hilbert1 :::"with_propositional_variables"::: ) ) ")" ) ")" )); registration cluster ($#v5_hilbert1 :::"HP-closed"::: ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_hilbert1 :::"with_VERUM"::: ) ($#v2_hilbert1 :::"with_implication"::: ) ($#v3_hilbert1 :::"with_conjunction"::: ) ($#v4_hilbert1 :::"with_propositional_variables"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_hilbert1 :::"with_VERUM"::: ) ($#v2_hilbert1 :::"with_implication"::: ) ($#v3_hilbert1 :::"with_conjunction"::: ) ($#v4_hilbert1 :::"with_propositional_variables"::: ) -> ($#v5_hilbert1 :::"HP-closed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "(" (Set ($#k5_numbers :::"NAT"::: ) ) ($#k13_finseq_1 :::"*"::: ) ")" ))); end; definitionfunc :::"HP-WFF"::: -> ($#m1_hidden :::"set"::: ) means :: HILBERT1:def 6 (Bool "(" (Bool it "is" ($#v5_hilbert1 :::"HP-closed"::: ) ) & (Bool "(" "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "D")) "is" ($#v5_hilbert1 :::"HP-closed"::: ) )) "holds" (Bool it ($#r1_tarski :::"c="::: ) (Set (Var "D"))) ")" ) ")" ); end; :: deftheorem defines :::"HP-WFF"::: HILBERT1:def 6 : (Bool "for" (Set (Var "b1")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_hilbert1 :::"HP-WFF"::: ) )) "iff" (Bool "(" (Bool (Set (Var "b1")) "is" ($#v5_hilbert1 :::"HP-closed"::: ) ) & (Bool "(" "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "D")) "is" ($#v5_hilbert1 :::"HP-closed"::: ) )) "holds" (Bool (Set (Var "b1")) ($#r1_tarski :::"c="::: ) (Set (Var "D"))) ")" ) ")" ) ")" )); registration cluster (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) -> ($#v5_hilbert1 :::"HP-closed"::: ) ; end; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v5_hilbert1 :::"HP-closed"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) -> ($#v4_funct_1 :::"functional"::: ) ; end; registration cluster -> ($#v1_finseq_1 :::"FinSequence-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ); end; definitionmode HP-formula is ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ); end; definitionfunc :::"VERUM"::: -> ($#m1_subset_1 :::"HP-formula":::) equals :: HILBERT1:def 7 (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ); let "p", "q" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ); func "p" :::"=>"::: "q" -> ($#m1_subset_1 :::"HP-formula":::) equals :: HILBERT1:def 8 (Set (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) "p" ")" ) ($#k7_finseq_1 :::"^"::: ) "q"); func "p" :::"'&'"::: "q" -> ($#m1_subset_1 :::"HP-formula":::) equals :: HILBERT1:def 9 (Set (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Num 2) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) "p" ")" ) ($#k7_finseq_1 :::"^"::: ) "q"); end; :: deftheorem defines :::"VERUM"::: HILBERT1:def 7 : (Bool (Set ($#k2_hilbert1 :::"VERUM"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) )); :: deftheorem defines :::"=>"::: HILBERT1:def 8 : (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool (Set (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p")) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q"))))); :: deftheorem defines :::"'&'"::: HILBERT1:def 9 : (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool (Set (Set (Var "p")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Num 2) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p")) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q"))))); definitionlet "T" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ); attr "T" is :::"Hilbert_theory"::: means :: HILBERT1:def 10 (Bool "(" (Bool (Set ($#k2_hilbert1 :::"VERUM"::: ) ) ($#r2_hidden :::"in"::: ) "T") & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "p")) ")" )) ($#r2_hidden :::"in"::: ) "T") & (Bool (Set (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) "T") & (Bool (Set (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) "T") & (Bool (Set (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) "T") & (Bool (Set (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "q")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) "T") & "(" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "T") & (Bool (Set (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) "T")) "implies" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) "T") ")" ")" ) ")" ) ")" ); end; :: deftheorem defines :::"Hilbert_theory"::: HILBERT1:def 10 : (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v6_hilbert1 :::"Hilbert_theory"::: ) ) "iff" (Bool "(" (Bool (Set ($#k2_hilbert1 :::"VERUM"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "p")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "q")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & "(" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "T")))) "implies" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) ")" ")" ) ")" ) ")" ) ")" )); definitionlet "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ); func :::"CnPos"::: "X" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) means :: HILBERT1:def 11 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "st" (Bool (Bool (Set (Var "T")) "is" ($#v6_hilbert1 :::"Hilbert_theory"::: ) ) & (Bool "X" ($#r1_tarski :::"c="::: ) (Set (Var "T")))) "holds" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "T")))) ")" )); end; :: deftheorem defines :::"CnPos"::: HILBERT1:def 11 : (Bool "for" (Set (Var "X")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k5_hilbert1 :::"CnPos"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "st" (Bool (Bool (Set (Var "T")) "is" ($#v6_hilbert1 :::"Hilbert_theory"::: ) ) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "T")))) "holds" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "T")))) ")" )) ")" )); definitionfunc :::"HP_TAUT"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) equals :: HILBERT1:def 12 (Set ($#k5_hilbert1 :::"CnPos"::: ) (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) ")" )); end; :: deftheorem defines :::"HP_TAUT"::: HILBERT1:def 12 : (Bool (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k5_hilbert1 :::"CnPos"::: ) (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) ")" ))); theorem :: HILBERT1:1 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool (Set ($#k2_hilbert1 :::"VERUM"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k5_hilbert1 :::"CnPos"::: ) (Set (Var "X"))))) ; theorem :: HILBERT1:2 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool (Set (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "q")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k5_hilbert1 :::"CnPos"::: ) (Set (Var "X")))))) ; theorem :: HILBERT1:3 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k5_hilbert1 :::"CnPos"::: ) (Set (Var "X")))))) ; theorem :: HILBERT1:4 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool (Set (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "p")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k5_hilbert1 :::"CnPos"::: ) (Set (Var "X")))))) ; theorem :: HILBERT1:5 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set ($#k5_hilbert1 :::"CnPos"::: ) (Set (Var "X")))))) ; theorem :: HILBERT1:6 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k5_hilbert1 :::"CnPos"::: ) (Set (Var "X")))))) ; theorem :: HILBERT1:7 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k5_hilbert1 :::"CnPos"::: ) (Set (Var "X")))) & (Bool (Set (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k5_hilbert1 :::"CnPos"::: ) (Set (Var "X"))))) "holds" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k5_hilbert1 :::"CnPos"::: ) (Set (Var "X")))))) ; theorem :: HILBERT1:8 (Bool "for" (Set (Var "T")) "," (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "st" (Bool (Bool (Set (Var "T")) "is" ($#v6_hilbert1 :::"Hilbert_theory"::: ) ) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "T")))) "holds" (Bool (Set ($#k5_hilbert1 :::"CnPos"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Var "T")))) ; theorem :: HILBERT1:9 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k5_hilbert1 :::"CnPos"::: ) (Set (Var "X"))))) ; theorem :: HILBERT1:10 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k5_hilbert1 :::"CnPos"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set ($#k5_hilbert1 :::"CnPos"::: ) (Set (Var "Y"))))) ; theorem :: HILBERT1:11 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool (Set ($#k5_hilbert1 :::"CnPos"::: ) (Set "(" ($#k5_hilbert1 :::"CnPos"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_hilbert1 :::"CnPos"::: ) (Set (Var "X"))))) ; registrationlet "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ); cluster (Set ($#k5_hilbert1 :::"CnPos"::: ) "X") -> ($#v6_hilbert1 :::"Hilbert_theory"::: ) ; end; theorem :: HILBERT1:12 (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v6_hilbert1 :::"Hilbert_theory"::: ) ) "iff" (Bool (Set ($#k5_hilbert1 :::"CnPos"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set (Var "T"))) ")" )) ; theorem :: HILBERT1:13 (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "st" (Bool (Bool (Set (Var "T")) "is" ($#v6_hilbert1 :::"Hilbert_theory"::: ) )) "holds" (Bool (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "T")))) ; registration cluster (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ) -> ($#v6_hilbert1 :::"Hilbert_theory"::: ) ; end; begin theorem :: HILBERT1:14 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool (Set (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ))) ; theorem :: HILBERT1:15 (Bool "for" (Set (Var "q")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "st" (Bool (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ))) "holds" (Bool (Set (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ))) ; theorem :: HILBERT1:16 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool (Set (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set ($#k2_hilbert1 :::"VERUM"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ))) ; theorem :: HILBERT1:17 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "p")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ))) ; theorem :: HILBERT1:18 (Bool "for" (Set (Var "q")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "q")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "p")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "p")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ))) ; theorem :: HILBERT1:19 (Bool "for" (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "q")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "r")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ))) ; theorem :: HILBERT1:20 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "st" (Bool (Bool (Set (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "r")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ))) "holds" (Bool (Set (Set (Var "q")) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "r")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ))) ; theorem :: HILBERT1:21 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "q")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "r")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ))) ; theorem :: HILBERT1:22 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "st" (Bool (Bool (Set (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "q")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "r")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "r")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ))) ; theorem :: HILBERT1:23 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "st" (Bool (Bool (Set (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) )) & (Bool (Set (Set (Var "q")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "r"))) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ))) "holds" (Bool (Set (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "r"))) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ))) ; theorem :: HILBERT1:24 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "s")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "s")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ))) ; theorem :: HILBERT1:25 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "r")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "r")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ))) ; theorem :: HILBERT1:26 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ))) ; theorem :: HILBERT1:27 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q")) ")" ) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ))) ; theorem :: HILBERT1:28 (Bool "for" (Set (Var "q")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool (Set (Set (Var "q")) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "q")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "p")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "p")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ))) ; theorem :: HILBERT1:29 (Bool "for" (Set (Var "s")) "," (Set (Var "q")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "st" (Bool (Bool (Set (Set (Var "s")) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "p")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) )) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ))) "holds" (Bool (Set (Set (Var "s")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ))) ; begin theorem :: HILBERT1:30 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool (Set (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "p")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ))) ; theorem :: HILBERT1:31 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) )) "iff" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) )) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) )) ")" ) ")" )) ; theorem :: HILBERT1:32 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "st" (Bool (Bool (Set (Set (Var "p")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ))) "holds" (Bool (Set (Set (Var "q")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ))) ; theorem :: HILBERT1:33 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "r")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ))) ; theorem :: HILBERT1:34 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "r")) ")" ) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "r")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ))) ; theorem :: HILBERT1:35 (Bool "for" (Set (Var "r")) "," (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "r")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "p")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "r")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "r")) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "q")) ")" ) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ))) ; theorem :: HILBERT1:36 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "p")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ))) ; theorem :: HILBERT1:37 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "p")) ")" ) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "s")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ))) ; theorem :: HILBERT1:38 (Bool "for" (Set (Var "q")) "," (Set (Var "s")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "q")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "s")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "s")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ))) ; theorem :: HILBERT1:39 (Bool "for" (Set (Var "q")) "," (Set (Var "s")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "q")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "s")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "q")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "p")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "s")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ))) ; theorem :: HILBERT1:40 (Bool "for" (Set (Var "p")) "," (Set (Var "s")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "s")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "s")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "s")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ))) ; theorem :: HILBERT1:41 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "s")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "s")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ))) ; theorem :: HILBERT1:42 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k4_hilbert1 :::"'&'"::: ) (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "s")) ")" ) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "s")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ))) ; theorem :: HILBERT1:43 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "p")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ))) ; theorem :: HILBERT1:44 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k4_hilbert1 :::"'&'"::: ) (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "s")) ")" ) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "s")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "q")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ))) ; theorem :: HILBERT1:45 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "s")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "s")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "q")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ))) ; theorem :: HILBERT1:46 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "s")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "p")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "s")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "q")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ))) ; theorem :: HILBERT1:47 (Bool "for" (Set (Var "p")) "," (Set (Var "s")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'&'"::: ) (Set "(" (Set (Var "s")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "q")) ")" ) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'&'"::: ) (Set "(" (Set (Var "q")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "s")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ))) ; theorem :: HILBERT1:48 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k4_hilbert1 :::"'&'"::: ) (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "s")) ")" ) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "s")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ))) ; theorem :: HILBERT1:49 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "s")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'&'"::: ) (Set "(" (Set (Var "q")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "s")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ))) ; theorem :: HILBERT1:50 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'&'"::: ) (Set "(" (Set (Var "q")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "s")) ")" ) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "s")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ))) ;