begin
theorem
begin
:: deftheorem defines |^.. FLANG_3:def 1 :
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem
theorem Th9:
theorem Th10:
theorem Th11:
theorem
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem
theorem Th32:
theorem Th33:
theorem
theorem Th35:
theorem
theorem Th37:
theorem Th38:
theorem
theorem Th40:
theorem Th41:
theorem
theorem
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
begin
:: deftheorem defines + FLANG_3:def 2 :
theorem Th48:
for
E,
x being
set for
A being
Subset of holds
(
x in A + iff ex
n being
Nat st
(
n > 0 &
x in A |^ n ) )
theorem Th49:
theorem Th50:
theorem
theorem Th52:
theorem Th53:
theorem
theorem Th55:
theorem Th56:
theorem Th57:
theorem Th58:
theorem Th59:
theorem Th60:
theorem Th61:
theorem
theorem
theorem
theorem
theorem Th66:
theorem
theorem
theorem
theorem
theorem
theorem Th72:
theorem
theorem
theorem Th75:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th86:
theorem Th87:
theorem
theorem
theorem Th90:
theorem
theorem Th92:
theorem
theorem
theorem
theorem