let G be with_finite_clique# SimpleGraph; ( Edges G <> {} implies clique# G >= 2 )
assume A1:
Edges G <> {}
; clique# G >= 2
consider e being object such that
A2:
e in Edges G
by A1, XBOOLE_0:def 1;
consider x, y being set such that
A3:
x <> y
and
A4:
x in Vertices G
and
A5:
y in Vertices G
and
A6:
e = {x,y}
by A2, Th11;
reconsider S = G SubgraphInducedBy {x,y} as finite Clique of G by A6, A2, Th56;
A7:
Vertices S = (Vertices G) /\ {x,y}
by Th45;
A8:
{x,y} c= Vertices G
by A4, A5, ZFMISC_1:32;
Vertices S = {x,y}
by A7, A8, XBOOLE_1:28;
then
order S = 2
by A3, CARD_2:57;
hence
clique# G >= 2
by Def15; verum