let D be Clique of R; :: thesis: D is finite
consider C being finite Clique of R such that
A: for D being finite Clique of R holds card D <= card C by Lfheight;
assume not D is finite ; :: thesis: contradiction
then consider Y being finite Subset of D such that
B: card Y > card C by Sinfset;
Y is Clique of R by Clique37;
hence contradiction by B, A; :: thesis: verum