:: deftheorem defines XorDelta PETRI_3:def 3 :
for I being non trivial set holds XorDelta I = { [i,j] where i, j is Element of I : i <> j } ;