consider A being finite StableSet of G such that
A1: for B being finite StableSet of G holds card A >= card B by Def23;
given B being StableSet of G such that A2: B is infinite ; :: thesis: contradiction
consider C being finite Subset of B such that
A3: card C > card A by A2, DILWORTH:5;
C is StableSet of G by Th64;
hence contradiction by A1, A3; :: thesis: verum