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

proof

assume I is prime ; :: thesis: ( I ` is Ideal 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_0:def 5;
A2: I ` is join-closed

proof

let x, y be Element of L; :: according to LATTICES:def 25 :: 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 initial

proof

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

end;

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

end;

assume A6: ( I ` is Ideal 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 Ideal of L or I ` = {} ) by A6;

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

then ( not x in I ` or not y in I ` ) by T1, FILTER_2:21;
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 Ideal of L or I ` = {} ) by A6;

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

then not x "\/" y in I ` by FILTER_2:86, 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_0:def 5; :: thesis: verum