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
A1: u in Vertices C and
A2: v in Vertices C ; :: thesis: {u,v} in C
C = CompleteSGraph (Vertices C) by Def13;
hence {u,v} in C by A1, A2, Th34; :: thesis: verum