let L be distributive Lattice; 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; ( 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
; 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.> )
;
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;
verum
end;
set I = (.a.>;
set F = <.b.);
set I1 = (.b.>;
set F1 = <.a.);