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 )

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

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

( 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 A12:
I in PRIME (InclPoset (Ids L))
; :: thesis: I is prime
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

end;( 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

hence
I in PRIME (InclPoset (Ids L))
by WAYBEL_6:def 7; :: thesis: verum
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;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

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

then A19:
X "/\" Y <= i
by YELLOW_1:3;
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;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

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