theorem Th58: :: FOMODEL0:58

for A, X, y being set st not y in proj2 X holds
[:A,{y}:] misses X