let R be finite RelStr ; :: thesis: clique# R <= card the carrier of R
consider C being finite Clique of R such that
A1: card C = clique# R by DILWORTH:def 4;
card C c= card the carrier of R by CARD_1:11;
hence clique# R <= card the carrier of R by A1, NAT_1:39; :: thesis: verum