theorem Lemma20: :: PREFER_1:36

for R, P being Relation st R misses P & P is symmetric holds
R ~ misses P