begin
theorem Th1:
for
m,
k,
i,
n being
Nat st
m + k <= i &
i <= n + k holds
ex
mn being
Nat st
(
mn + k = i &
m <= mn &
mn <= n )
theorem Th2:
for
m,
n,
k,
l,
i being
Nat st
m <= n &
k <= l &
m + k <= i &
i <= n + l holds
ex
mn,
kl being
Nat st
(
mn + kl = i &
m <= mn &
mn <= n &
k <= kl &
kl <= l )
theorem Th3:
for
m,
n being
Nat st
m < n holds
ex
k being
Nat st
(
m + k = n &
k > 0 )
theorem Th4:
begin
theorem
theorem
theorem Th7:
theorem
theorem Th9:
theorem Th10:
theorem
theorem Th12:
theorem
theorem
theorem
theorem Th16:
theorem Th17:
theorem
begin
:: deftheorem defines |^ FLANG_2:def 1 :
theorem Th19:
for
E,
x being
set for
A being
Subset of
for
m,
n being
Nat holds
(
x in A |^ m,
n iff ex
k being
Nat st
(
m <= k &
k <= n &
x in A |^ k ) )
theorem Th20:
theorem Th21:
for
E being
set for
A being
Subset of
for
m,
n being
Nat holds
(
A |^ m,
n = {} iff (
m > n or (
m > 0 &
A = {} ) ) )
theorem Th22:
theorem Th23:
theorem
theorem Th25:
theorem Th26:
theorem
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
for
E being
set for
A being
Subset of
for
m,
n,
k,
l being
Nat st
m <= n &
k <= l holds
(A |^ m,n) ^^ (A |^ k,l) = A |^ (m + k),
(n + l)
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem
theorem
theorem Th45:
theorem Th46:
theorem
theorem
theorem
theorem
theorem Th51:
theorem Th52:
theorem Th53:
theorem
theorem
theorem
for
E being
set for
A being
Subset of
for
m,
n,
k,
l being
Nat holds
(A |^ m,n) |^ k,
l c= A |^ (m * k),
(n * l)
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th64:
theorem
theorem Th66:
theorem
theorem
theorem Th69:
theorem
theorem Th71:
theorem Th72:
begin
:: deftheorem defines ? FLANG_2:def 2 :
theorem Th73:
for
E,
x being
set for
A being
Subset of holds
(
x in A ? iff ex
k being
Nat st
(
k <= 1 &
x in A |^ k ) )
theorem
theorem Th75:
theorem Th76:
theorem
theorem Th78:
theorem Th79:
theorem Th80:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th93:
theorem Th94:
theorem Th95:
theorem Th96:
theorem Th97:
theorem Th98:
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th105:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem