let L be LATTICE; :: thesis: for I being Ideal of L holds
( I is prime iff I in PRIME (InclPoset (Ids L)) )
let I be Ideal of L; :: thesis: ( I is prime iff I in PRIME (InclPoset (Ids L)) )
set P = InclPoset (Ids L);
A1: InclPoset (Ids L) = RelStr(# (Ids L),(RelIncl (Ids L)) #) by YELLOW_1:def 1;
I in Ids L ;
then reconsider i = I as Element of (InclPoset (Ids L)) by A1;
thus ( I is prime implies I in PRIME (InclPoset (Ids L)) ) :: thesis: ( I in PRIME (InclPoset (Ids L)) implies I is prime )

proof

assume A2: for x, y being Element of L holds
( not x "/\" y in I or x in I or y in I ) ; :: according to WAYBEL_7:def 1 :: thesis: I in PRIME (InclPoset (Ids L))
i is prime

proof

let x, y be Element of (InclPoset (Ids L)); :: according to WAYBEL_6:def 6 :: thesis: ( not x "/\" y <= i or x <= i or y <= i )
y in Ids L by A1;
then A3: ex J being Ideal of L st y = J ;
x in Ids L by A1;
then ex J being Ideal of L st x = J ;
then reconsider X = x, Y = y as Ideal of L by A3;
assume x "/\" y <= i ; :: thesis: ( x <= i or y <= i )
then x "/\" y c= I by YELLOW_1:3;
then A4: X /\ Y c= I by YELLOW_2:43;
assume that
A5: not x <= i and
A6: not y <= i ; :: thesis: contradiction
not X c= I by A5, YELLOW_1:3;
then consider a being object such that
A7: a in X and
A8: not a in I ;
not Y c= I by A6, YELLOW_1:3;
then consider b being object such that
A9: b in Y and
A10: not b in I ;
reconsider a = a, b = b as Element of L by A7, A9;
a "/\" b <= b by YELLOW_0:23;
then A11: a "/\" b in Y by A9, WAYBEL_0:def 19;
a "/\" b <= a by YELLOW_0:23;
then a "/\" b in X by A7, WAYBEL_0:def 19;
then a "/\" b in X /\ Y by A11, XBOOLE_0:def 4;
hence contradiction by A2, A4, A8, A10; :: thesis: verum

end;

hence I in PRIME (InclPoset (Ids L)) by WAYBEL_6:def 7; :: thesis: verum

end;

assume A12: I in PRIME (InclPoset (Ids L)) ; :: thesis: I is prime
let x, y be Element of L; :: according to WAYBEL_7:def 1 :: thesis: ( not x "/\" y in I or x in I or y in I )
reconsider X = downarrow x, Y = downarrow y as Ideal of L ;
( X in Ids L & Y in Ids L ) ;
then reconsider X = X, Y = Y as Element of (InclPoset (Ids L)) by A1;
A13: X /\ Y = X "/\" Y by YELLOW_2:43;
assume A14: x "/\" y in I ; :: thesis: ( x in I or y in I )
X "/\" Y c= I

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in X "/\" Y or a in I )
assume A15: a in X "/\" Y ; :: thesis: a in I
then A16: a in X by A13, XBOOLE_0:def 4;
A17: a in Y by A13, A15, XBOOLE_0:def 4;
reconsider a = a as Element of L by A16;
A18: a <= y by A17, WAYBEL_0:17;
a <= x by A16, WAYBEL_0:17;
then a <= x "/\" y by A18, YELLOW_0:23;
hence a in I by A14, WAYBEL_0:def 19; :: thesis: verum

end;

then A19: X "/\" Y <= i by YELLOW_1:3;
i is prime by A12, WAYBEL_6:def 7;
then ( X <= i or Y <= i ) by A19;
then A20: ( X c= I or Y c= I ) by YELLOW_1:3;
y <= y ;
then A21: y in Y by WAYBEL_0:17;
x <= x ;
then x in X by WAYBEL_0:17;
hence ( x in I or y in I ) by A21, A20; :: thesis: verum