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 F' = I as Filter of (L opp ) by YELLOW_7:26, YELLOW_7:28;
reconsider I' = F as Ideal of (L opp ) by YELLOW_7:27, YELLOW_7:29;
consider P' being Ideal of (L opp ) such that
A2: ( P' is prime & I' c= P' & P' misses F' ) by A1, Th27;
reconsider P = P' 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, Th21; :: thesis: verum