theorem Th12: :: SCMYCIEL:12

for X being set
for x, y being object st x <> y & {x,y} in X holds
{x,y} in PairsOf X