theorem Th13: :: SCMYCIEL:13

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