:: deftheorem defines TWOELEMENTSETS SGRAPH1:def 2 :
for A being set holds TWOELEMENTSETS A = { z where z is finite Subset of A : card z = 2 } ;