let L be distributive LATTICE; :: thesis: for I being Ideal of L

for F being Filter of L st I misses F holds

ex P being Filter of L st

( P is prime & F c= P & I misses P )

let I be Ideal of L; :: thesis: for F being Filter of L st I misses F holds

ex P being Filter of L st

( P is prime & F c= P & I misses P )

let F be Filter of L; :: thesis: ( I misses F implies ex P being Filter of L st

( P is prime & F c= P & I misses P ) )

assume A1: I misses F ; :: thesis: ex P being Filter of L st

( P is prime & F c= P & I misses P )

reconsider I9 = F as Ideal of (L opp) by YELLOW_7:27, YELLOW_7:29;

reconsider F9 = I as Filter of (L opp) by YELLOW_7:26, YELLOW_7:28;

consider P9 being Ideal of (L opp) such that

A2: ( P9 is prime & I9 c= P9 & P9 misses F9 ) by A1, Th23;

reconsider P = P9 as Filter of L by YELLOW_7:27, YELLOW_7:29;

take P ; :: thesis: ( P is prime & F c= P & I misses P )

thus ( P is prime & F c= P & I misses P ) by A2, Th17; :: thesis: verum

for F being Filter of L st I misses F holds

ex P being Filter of L st

( P is prime & F c= P & I misses P )

let I be Ideal of L; :: thesis: for F being Filter of L st I misses F holds

ex P being Filter of L st

( P is prime & F c= P & I misses P )

let F be Filter of L; :: thesis: ( I misses F implies ex P being Filter of L st

( P is prime & F c= P & I misses P ) )

assume A1: I misses F ; :: thesis: ex P being Filter of L st

( P is prime & F c= P & I misses P )

reconsider I9 = F as Ideal of (L opp) by YELLOW_7:27, YELLOW_7:29;

reconsider F9 = I as Filter of (L opp) by YELLOW_7:26, YELLOW_7:28;

consider P9 being Ideal of (L opp) such that

A2: ( P9 is prime & I9 c= P9 & P9 misses F9 ) by A1, Th23;

reconsider P = P9 as Filter of L by YELLOW_7:27, YELLOW_7:29;

take P ; :: thesis: ( P is prime & F c= P & I misses P )

thus ( P is prime & F c= P & I misses P ) by A2, Th17; :: thesis: verum