:: deftheorem defines K_ SGRAPH1:def 12 :
for n, m being Element of NAT
for b₃ being SimpleGraph of NAT holds
( b₃ = K_ (m,n) iff ex ee being Subset of (TWOELEMENTSETS (Seg (m + n))) st
( ee = { {i,j} where i, j is Element of NAT : ( i in Seg m & j in nat_interval ((m + 1),(m + n)) ) } & b₃ = SimpleGraphStruct(# (Seg (m + n)),ee #) ) );