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