let L be Boolean LATTICE; :: thesis: for F being Filter of L holds
( F is prime iff for a being Element of L holds
( a in F or 'not' a in F ) )
let F be Filter of L; :: thesis: ( F is prime iff for a being Element of L holds
( a in F or 'not' a in F ) )

hereby :: thesis: ( ( for a being Element of L holds
( a in F or 'not' a in F ) ) implies F is prime )

assume A1: F is prime ; :: thesis: for a being Element of L holds
( a in F or 'not' a in F )
let a be Element of L; :: thesis: ( a in F or 'not' a in F )
set b = 'not' a;
a "\/" ('not' a) = Top L by YELLOW_5:37;
then a "\/" ('not' a) in F by WAYBEL_4:22;
hence ( a in F or 'not' a in F ) by A1, Def2; :: thesis: verum

end;

assume A2: for a being Element of L holds
( a in F or 'not' a in F ) ; :: thesis: F is prime
let a, b be Element of L; :: according to WAYBEL_7:def 2 :: thesis: ( not a "\/" b in F or a in F or b in F )
assume A3: ( a "\/" b in F & not a in F & not b in F ) ; :: thesis: contradiction
then ( 'not' a in F & 'not' b in F ) by A2;
then ('not' a) "/\" ('not' b) in F by WAYBEL_0:41;
then 'not' (a "\/" b) in F by YELLOW_5:39;
then ('not' (a "\/" b)) "/\" (a "\/" b) in F by A3, WAYBEL_0:41;
then ( Bottom L in F & a >= Bottom L ) by YELLOW_0:44, YELLOW_5:37;
hence contradiction by A3, WAYBEL_0:def 20; :: thesis: verum