:: deftheorem defines KVertices GRAPH_3A:def 1 :
KVertices = {0,1,2,3};