begin
begin
begin
scheme
Regr1{
F1()
-> Nat,
P1[
set ] } :
provided
A1:
P1[
F1()]
and A2:
for
k being
Element of
NAT st
k < F1() &
P1[
k + 1] holds
P1[
k]
begin
begin
begin
begin
begin
begin
begin
theorem Th41:
for
n being
Ordinal for
p,
q,
r being
bag of
n st
p < q &
q < r holds
p < r
theorem
for
n being
Ordinal for
p,
q,
r being
bag of
n st
p < q &
q <=' r holds
p < r
theorem
for
n being
Ordinal for
p,
q,
r being
bag of
n st
p <=' q &
q < r holds
p < r
theorem Th46:
for
n being
set for
d,
b being
bag of
n st ( for
k being
set st
k in n holds
d . k <= b . k ) holds
d divides b
theorem Th48:
for
X being
set for
b1,
b2 being
bag of
X holds
(b2 + b1) -' b1 = b2
theorem Th50:
for
n being
set for
b,
b1,
b2 being
bag of
n st
b = b1 + b2 holds
b1 divides b
Lm1:
for n being Ordinal holds BagOrder n is_reflexive_in Bags n
Lm2:
for n being Ordinal holds BagOrder n is_antisymmetric_in Bags n
Lm3:
for n being Ordinal holds BagOrder n is_transitive_in Bags n
Lm4:
for n being Ordinal holds BagOrder n linearly_orders Bags n