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