theorem Th17: :: SCMYCIEL:17

for X being set st X is void holds
PairsOf X = {}