let D be Clique of R; :: thesis: D is finite
consider C being finite Clique of R such that
A1: for D being finite Clique of R holds card D <= card C by Def3;
assume D is infinite ; :: thesis: contradiction
then consider Y being finite Subset of D such that
A2: card Y > card C by Th5;
Y is Clique of R by Th9;
hence contradiction by A2, A1; :: thesis: verum