let G be with_finite_clique# SimpleGraph; ( Edges G <> {} implies clique# G >= 2 )
assume A:
Edges G <> {}
; clique# G >= 2
consider e being set such that
B:
e in Edges G
by A, XBOOLE_0:def 1;
consider x, y being set such that
C:
x <> y
and
D:
x in Vertices G
and
E:
y in Vertices G
and
F:
e = {x,y}
by B, SG4;
reconsider S = G SubgraphInducedBy {x,y} as finite Clique of G by F, B, Th8;
G:
Vertices S = (Vertices G) /\ {x,y}
by Sub5;
H:
{x,y} c= Vertices G
by D, E, ZFMISC_1:32;
Vertices S = {x,y}
by G, H, XBOOLE_1:28;
then
order S = 2
by C, CARD_2:57;
hence
clique# G >= 2
by Lcliqueno; verum