begin
:: deftheorem Def1 defines negation_faithful GOEDELCP:def 1 :
:: deftheorem Def2 defines with_examples GOEDELCP:def 2 :
theorem
theorem Th2:
theorem Th3:
theorem
theorem Th5:
theorem Th6:
theorem
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
begin
theorem Th18:
:: deftheorem Def3 defines ExCl GOEDELCP:def 3 :
theorem Th19:
theorem Th20:
Lm1:
for A being non empty set st A is countable holds
ex f being Function st
( dom f = NAT & A = rng f )
:: deftheorem Def4 defines Ex-bound_in GOEDELCP:def 4 :
:: deftheorem Def5 defines Ex-the_scope_of GOEDELCP:def 5 :
:: deftheorem Def6 defines bound_in GOEDELCP:def 6 :
:: deftheorem Def7 defines the_scope_of GOEDELCP:def 7 :
:: deftheorem defines still_not-bound_in GOEDELCP:def 8 :
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
begin
theorem Th35:
theorem Th36:
theorem Th37:
theorem