consider A being finite StableSet of G such that
A1: for B being finite StableSet of G holds card A >= card B by Def23;
take itt = card A; :: thesis: ( ex A being finite StableSet of G st card A = itt & ( for T being finite StableSet of G holds card T <= itt ) )
thus ex A being finite StableSet of G st card A = itt ; :: thesis: for T being finite StableSet of G holds card T <= itt
let T be finite StableSet of G; :: thesis: card T <= itt
thus card T <= itt by A1; :: thesis: verum