:: deftheorem Def14 defines with_finite_clique# SCMYCIEL:def 14 :
for G being SimpleGraph holds
( G is with_finite_clique# iff ex C being finite Clique of G st
for D being finite Clique of G holds order D <= order C );