theorem LemmaAuxIrr: :: PREFER_1:13

for P, R being Relation st P misses R holds
P ~ misses R ~