Definition. Ideal of a Forcing Notion [002F]

    An ideal of a forcing notion is a subset satisfiying

    1. and then (downward stability)
    2. then there exists with (directedness)