let L be Lattice; :: thesis: for I being Ideal of L holds
( I is prime iff ( I ` is Filter of L or I ` = {} ) )
let I be Ideal of L; :: thesis: ( I is prime iff ( I ` is Filter of L or I ` = {} ) )
set F = I ` ;
thus ( not I is prime or I ` is Filter of L or I ` = {} ) :: thesis: ( ( I ` is Filter of L or I ` = {} ) implies I is prime )

proof

assume I is prime ; :: thesis: ( I ` is Filter of L or I ` = {} )
then A1: for x, y being Element of L holds
( not x "/\" y in I or x in I or y in I ) by FILTER_2:def 10;
A2: I ` is meet-closed

proof

let x, y be Element of L; :: according to LATTICES:def 24 :: thesis: ( not x in I ` or not y in I ` or x "/\" y in I ` )
assume ( x in I ` & y in I ` ) ; :: thesis: x "/\" y in I `
then ( not x in I & not y in I ) by XBOOLE_0:def 5;
hence x "/\" y in I ` by A1, SUBSET_1:29; :: thesis: verum

end;

I ` is final

proof

let x, y be Element of L; :: according to LATTICES:def 23 :: thesis: ( not x [= y or not x in I ` or y in I ` )
assume that
A5: x [= y and
A4: x in I ` ; :: thesis: y in I `
( y in I implies x in I ) by A5, LATTICES:def 22;
hence y in I ` by A4, XBOOLE_0:def 5; :: thesis: verum

end;

hence ( I ` is Filter of L or I ` = {} ) by A2; :: thesis: verum

end;

assume A6: ( I ` is Filter of L or I ` = {} ) ; :: thesis: I is prime
for x, y being Element of L holds
( x "/\" y in I iff ( x in I or y in I ) )

proof

let x, y be Element of L; :: thesis: ( x "/\" y in I iff ( x in I or y in I ) )

hereby :: thesis: ( ( x in I or y in I ) implies x "/\" y in I )

assume x "/\" y in I ; :: thesis: ( x in I or y in I )
then T1: not x "/\" y in I ` by XBOOLE_0:def 5;

per cases ( I ` is Filter of L or I ` = {} ) by A6;

suppose I ` is Filter of L ; :: thesis: ( x in I or y in I )

then ( not x in I ` or not y in I ` ) by T1, FILTER_0:9;
hence ( x in I or y in I ) by XBOOLE_0:def 5; :: thesis: verum

end;

suppose T2: I ` = {} ; :: thesis: ( x in I or y in I )

I = (I `) ` ;
hence ( x in I or y in I ) by T2; :: thesis: verum

end;

end;

end;

assume ( x in I or y in I ) ; :: thesis: x "/\" y in I
then T4: ( not x in I ` or not y in I ` ) by XBOOLE_0:def 5;

per cases ( I ` is Filter of L or I ` = {} ) by A6;

suppose I ` is Filter of L ; :: thesis: x "/\" y in I

then not x "/\" y in I ` by FILTER_0:8, T4;
hence x "/\" y in I by XBOOLE_0:def 5; :: thesis: verum

end;

suppose T2: I ` = {} ; :: thesis: x "/\" y in I

I = (I `) ` ;
hence x "/\" y in I by T2; :: thesis: verum

end;

end;

end;

hence I is prime by FILTER_2:def 10; :: thesis: verum