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 )
( x in Ids L & y in Ids L ) by A1;
then ( ex J being Ideal of L st x = J & ex J being Ideal of L st y = J ) ;
then reconsider X = x, Y = y as Ideal of L ;
assume x "/\" y <= i ; :: thesis: ( x <= i or y <= i )
then x "/\" y c= I by YELLOW_1:3;
then A3: X /\ Y c= I by YELLOW_2:45;
assume ( not x <= i & not y <= i ) ; :: thesis: contradiction
then A4: ( not X c= I & not Y c= I ) by YELLOW_1:3;
then consider a being set such that
A5: ( a in X & not a in I ) by TARSKI:def 3;
consider b being set such that
A6: ( b in Y & not b in I ) by A4, TARSKI:def 3;
reconsider a = a, b = b as Element of L by A5, A6;
( a "/\" b <= a & a "/\" b <= b ) by YELLOW_0:23;
then ( a "/\" b in X & a "/\" b in Y ) by A5, A6, WAYBEL_0:def 19;
then a "/\" b in X /\ Y by XBOOLE_0:def 4;
hence contradiction by A2, A3, A5, A6; :: thesis: verum

end;

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

end;

assume I in PRIME (InclPoset (Ids L)) ; :: thesis: I is prime
then A7: i is prime by WAYBEL_6:def 7;
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;
( x <= x & y <= y ) ;
then A8: ( x in X & y in Y ) by WAYBEL_0:17;
then x "/\" y in (downarrow x) "/\" (downarrow y) by YELLOW_4:37;
then A9: ( x "/\" y in X /\ Y & X /\ Y = X "/\" Y ) by YELLOW_2:45, YELLOW_4:50;
assume A10: x "/\" y in I ; :: thesis: ( x in I or y in I )
X "/\" Y c= I

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in X "/\" Y or a in I )
assume a in X "/\" Y ; :: thesis: a in I
then A11: ( a in X & a in Y ) by A9, XBOOLE_0:def 4;
then reconsider a = a as Element of L ;
( a <= x & a <= y ) by A11, WAYBEL_0:17;
then a <= x "/\" y by YELLOW_0:23;
hence a in I by A10, WAYBEL_0:def 19; :: thesis: verum

end;

then X "/\" Y <= i by YELLOW_1:3;
then ( X <= i or Y <= i ) by A7, WAYBEL_6:def 6;
then ( X c= I or Y c= I ) by YELLOW_1:3;
hence ( x in I or y in I ) by A8; :: thesis: verum