let G be with_finite_clique# SimpleGraph; :: thesis: ( clique# G = 0 implies Vertices G = {} )
assume Aa: clique# G = 0 ; :: thesis: Vertices G = {}
assume Vertices G <> {} ; :: thesis: contradiction
then consider v being set such that
Aa1: v in Vertices G by XBOOLE_0:def 1;
consider D being finite Clique of G such that
B1: Vertices D = {v} by Aa1, CliqueS;
order D <= 0 by Aa, Lcliqueno;
hence contradiction by B1; :: thesis: verum