let L be Lattice; :: thesis: for F being Ideal of L st not F is prime holds
ex a, b being Element of L st
( a "/\" b in F & not a in F & not b in F )
let F be Ideal of L; :: thesis: ( not F is prime implies ex a, b being Element of L st
( a "/\" b in F & not a in F & not b in F ) )
assume not F is prime ; :: thesis: ex a, b being Element of L st
( a "/\" b in F & not a in F & not b in F )
then consider a, b being Element of L such that
Z1: ( ( a "/\" b in F & not a in F & not b in F ) or ( ( a in F or b in F ) & not a "/\" b in F ) ) by FILTER_2:def 10;

now :: thesis: ( not a "/\" b in F implies ( not a in F & not b in F ) )

assume ( not a "/\" b in F & ( a in F or b in F ) ) ; :: thesis: contradiction

per cases then ( ( not a "/\" b in F & a in F ) or ( not a "/\" b in F & b in F ) ) ;

suppose ( not a "/\" b in F & a in F ) ; :: thesis: contradiction

hence contradiction by FILTER_2:22; :: thesis: verum

end;

suppose ( not a "/\" b in F & b in F ) ; :: thesis: contradiction

hence contradiction by FILTER_2:22; :: thesis: verum

end;

end;

end;

hence ex a, b being Element of L st
( a "/\" b in F & not a in F & not b in F ) by Z1; :: thesis: verum