theorem Th5: :: FACIRC_1:5

for X, R being set st X is without_pairs & R is Relation holds
X misses R ;