consider A being finite StableSet of R such that
A: for B being finite StableSet of R holds card A >= card B by Lfwidth;
given B being StableSet of R such that B: not B is finite ; :: thesis: contradiction
consider C being finite Subset of B such that
C: card C > card A by B, Sinfset;
C is StableSet of R by AChain0;
hence contradiction by A, C; :: thesis: verum