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