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 ) )

( 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 that

A3: a "\/" b in F and

A4: not a in F and

A5: not b in F ; :: thesis: contradiction

( 'not' a in F & 'not' b in F ) by A2, A4, A5;

then ('not' a) "/\" ('not' b) in F by WAYBEL_0:41;

then 'not' (a "\/" b) in F by YELLOW_5:36;

then ('not' (a "\/" b)) "/\" (a "\/" b) in F by A3, WAYBEL_0:41;

then A6: Bottom L in F by YELLOW_5:34;

a >= Bottom L by YELLOW_0:44;

hence contradiction by A4, A6, WAYBEL_0:def 20; :: thesis: verum

( 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 A2:
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:34;

then a "\/" ('not' a) in F by WAYBEL_4:22;

hence ( a in F or 'not' a in F ) by A1; :: thesis: verum

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

then a "\/" ('not' a) in F by WAYBEL_4:22;

hence ( a in F or 'not' a in F ) by A1; :: thesis: verum

( 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 that

A3: a "\/" b in F and

A4: not a in F and

A5: not b in F ; :: thesis: contradiction

( 'not' a in F & 'not' b in F ) by A2, A4, A5;

then ('not' a) "/\" ('not' b) in F by WAYBEL_0:41;

then 'not' (a "\/" b) in F by YELLOW_5:36;

then ('not' (a "\/" b)) "/\" (a "\/" b) in F by A3, WAYBEL_0:41;

then A6: Bottom L in F by YELLOW_5:34;

a >= Bottom L by YELLOW_0:44;

hence contradiction by A4, A6, WAYBEL_0:def 20; :: thesis: verum