let L be Lattice; :: thesis: for I being Ideal of L holds
( I is prime iff I .: is prime )
let I be Ideal of L; :: thesis: ( I is prime iff I .: is prime )
thus ( I is prime implies I .: is prime ) :: thesis: ( I .: is prime implies I is prime )

proof

assume A1: for p, q being Element of L holds
( p "/\" q in I iff ( p in I or q in I ) ) ; :: according to FILTER_2:def 10 :: thesis: I .: is prime
let p9 be Element of (L .:); :: according to FILTER_0:def 5 :: thesis: for b₁ being Element of the carrier of (L .:) holds
( ( not p9 "\/" b₁ in I .: or p9 in I .: or b₁ in I .: ) & ( ( not p9 in I .: & not b₁ in I .: ) or p9 "\/" b₁ in I .: ) )
let q9 be Element of (L .:); :: thesis: ( ( not p9 "\/" q9 in I .: or p9 in I .: or q9 in I .: ) & ( ( not p9 in I .: & not q9 in I .: ) or p9 "\/" q9 in I .: ) )
p9 "\/" q9 = (.: p9) "/\" (.: q9) ;
hence ( ( not p9 "\/" q9 in I .: or p9 in I .: or q9 in I .: ) & ( ( not p9 in I .: & not q9 in I .: ) or p9 "\/" q9 in I .: ) ) by A1; :: thesis: verum

end;

assume A2: for p9, q9 being Element of (L .:) holds
( p9 "\/" q9 in I .: iff ( p9 in I .: or q9 in I .: ) ) ; :: according to FILTER_0:def 5 :: thesis: I is prime
let p be Element of L; :: according to FILTER_2:def 10 :: thesis: for q being Element of L holds
( p "/\" q in I iff ( p in I or q in I ) )
let q be Element of L; :: thesis: ( p "/\" q in I iff ( p in I or q in I ) )
(p .:) "\/" (q .:) = p "/\" q ;
hence ( p "/\" q in I iff ( p in I or q in I ) ) by A2; :: thesis: verum