let G be SimpleGraph; :: thesis: ( ( for x, y being set st x <> y & x in Vertices G & y in Vertices G holds
{x,y} in Edges G ) implies G is clique )
assume A1: for x, y being set st x <> y & x in Vertices G & y in Vertices G holds
{x,y} in Edges G ; :: thesis: G is clique

now :: thesis: for x, y being set st x in Vertices G & y in Vertices G holds
{x,y} in G

let x, y be set ; :: thesis: ( x in Vertices G & y in Vertices G implies {b₁,b₂} in G )
assume that
A2: x in Vertices G and
A3: y in Vertices G ; :: thesis: {b₁,b₂} in G

per cases ( x <> y or x = y ) ;

suppose x <> y ; :: thesis: {b₁,b₂} in G

then {x,y} in Edges G by A2, A3, A1;
hence {x,y} in G ; :: thesis: verum

end;

suppose x = y ; :: thesis: {b₁,b₂} in G

then {x,y} = {x} by ENUMSET1:29;
hence {x,y} in G by A2, Th24; :: thesis: verum

end;

end;

end;

then G = CompleteSGraph (Vertices G) by Th32;
hence G is clique ; :: thesis: verum