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

proof

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

end;

set I = (.a.>;
set F = <.b.);
set I1 = (.b.>;
set F1 = <.a.);

per cases ( (.a.> misses <.b.) or (.b.> misses <.a.) ) by ZZ;

suppose (.a.> misses <.b.) ; :: thesis: ex P being Ideal of L st
( ( P is prime & a in P & not b in P ) or ( not a in P & b in P ) )

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

end;

suppose (.b.> misses <.a.) ; :: thesis: ex P being Ideal of L st
( ( P is prime & a in P & not b in P ) or ( not a in P & b in P ) )

then consider P being Ideal of L such that
B1: ( P is prime & (.b.> c= P & P misses <.a.) ) by Th15;
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 & a in P & not b in P ) or ( not a in P & b in P ) ) by B2; :: thesis: verum

end;

end;