{ the Element of R} is clique ;
hence ex b₁ being Clique of R st
( b₁ is finite & not b₁ is empty ) ; :: thesis: verum