let G be with_finite_clique# SimpleGraph; :: thesis: ( clique# G = 0 implies Vertices G = {} )
assume A1: clique# G = 0 ; :: thesis: Vertices G = {}
assume Vertices G <> {} ; :: thesis: contradiction
then consider v being object such that
A2: v in Vertices G by XBOOLE_0:def 1;
consider D being finite Clique of G such that
A3: Vertices D = {v} by A2, Th52;
order D <= 0 by A1, Def15;
hence contradiction by A3; :: thesis: verum