let L be distributive Lattice; :: thesis: for a, b being Element of L st not a [= b holds
ex P being Ideal of L st
( P is prime & not a in P & b in P )
let a, b be Element of L; :: thesis: ( not a [= b implies ex P being Ideal of L st
( P is prime & not a in P & b in P ) )
assume AA: not a [= b ; :: thesis: ex P being Ideal of L st
( P is prime & not a in P & b in P )
ZZ: <.a.) misses (.b.>

proof

assume <.a.) meets (.b.> ; :: thesis: contradiction
then consider y being object such that
A2: ( y in (.b.> & y in <.a.) ) by XBOOLE_0:3;
reconsider y = y as Element of L by A2;
A4: y [= b by A2, FILTER_2:28;
a [= y by A2, FILTER_0:15;
hence contradiction by AA, A4, LATTICES:7; :: thesis: verum

end;

set I1 = (.b.>;
set F1 = <.a.);
consider P being Ideal of L such that
B1: ( P is prime & (.b.> c= P & P misses <.a.) ) by Th15, ZZ;
B2: b in P by B1, FILTER_2:28;
a in <.a.) ;
then not a in P by B1, XBOOLE_0:3;
hence ex P being Ideal of L st
( P is prime & not a in P & b in P ) by B1, B2; :: thesis: verum