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: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;
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 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