>>580
つづき

＜証明＞
https://proofwiki.org/wiki/Infinite_Sequence_Property_of_Strictly_Well-Founded_Relation
proofwiki
Infinite Sequence Property of Strictly Well-Founded Relation
Contents
1 Theorem
2 Proof
2.1 Reverse Implication
2.2 Forward Implication
3 Axiom of Dependent Choice
4 Sources

Theorem
Let (S,R) be a relational structure.
Then R is a strictly well-founded relation if and only if there is no infinite sequence ?an? of elements of S such that:
∀n∈N:an+1 R an

Proof
Reverse Implication
Suppose R is not a strictly well-founded relation.
So by definition there exists a non-empty subset T of S which has no strictly minimal element.
Let a∈T.

Since a is not strictly minimal in T, we can find b∈T:bRa.
This holds for all a∈T.
Hence the restriction R↑T×T of R to T×T is a right-total endorelation on T.

So, by the Axiom of Dependent Choice, it follows that there is an infinite sequence ?an? in T such that:
∀n∈N:an+1 R an
It follows by the Rule of Transposition that if there is no infinite sequence ?an? of elements of S such that:
∀n∈N:an+1 R an
then R is a strictly well-founded relation.
□

つづく