let R be SimpleGraph; :: thesis: ( R is finite implies R is with_finite_stability# )
assume R is finite ; :: thesis: R is with_finite_stability#
then reconsider R9 = R as finite SimpleGraph ;
reconsider VR = Vertices R9 as finite set ;
defpred S₁[ Nat] means ex A being finite StableSet of R9 st card A = c₁;
A1: for k being Nat st S₁[k] holds
k <= card VR by NAT_1:43;
( {} VR is StableSet of R & card {} = 0 ) ;
then A2: ex k being Nat st S₁[k] ;
consider k being Nat such that
A3: S₁[k] and
A4: for n being Nat st S₁[n] holds
n <= k from NAT_1:sch 6(A1, A2);
consider S being finite StableSet of R such that
A5: card S = k by A3;
take S ; :: according to SCMYCIEL:def 23 :: thesis: for B being finite StableSet of R holds card B <= card S
let T be finite StableSet of R; :: thesis: card T <= card S
thus card T <= card S by A5, A4; :: thesis: verum