consider A being finite StableSet of R such that
A1: for B being finite StableSet of R holds card A >= card B by Def5;
given B being StableSet of R such that A2: B is infinite ; :: thesis: contradiction
consider C being finite Subset of B such that
A3: card C > card A by A2, Th5;
C is StableSet of R by Th16;
hence contradiction by A1, A3; :: thesis: verum