:: deftheorem Def13 defines K_ SGRAPH1:def 13 :
for n being Element of NAT
for b₂ being SimpleGraph of NAT holds
( b₂ = K_ n iff ex ee being finite Subset of (TWOELEMENTSETS (Seg n)) st
( ee = { {i,j} where i, j is Element of NAT : ( i in Seg n & j in Seg n & i <> j ) } & b₂ = SimpleGraphStruct(# (Seg n),ee #) ) );