theorem Th11: :: SCMYCIEL:11

for X, e being set st e in PairsOf X holds
ex x, y being set st
( x <> y & x in union X & y in union X & e = {x,y} )