let C be clique SimpleGraph; :: thesis: for u, v being set st u in Vertices C & v in Vertices C holds
{u,v} in C
let u, v be set ; :: thesis: ( u in Vertices C & v in Vertices C implies {u,v} in C )
assume that
A: u in Vertices C and
B: v in Vertices C ; :: thesis: {u,v} in C
C = CompleteSGraph (Vertices C) by Lclique;
hence {u,v} in C by A, B, CSG1; :: thesis: verum