let X be set ; :: thesis: for F being Filter of (BoolePoset X) holds
( F is prime iff for A being Subset of X holds
( A in F or X \ A in F ) )
set L = BoolePoset X;
let F be Filter of (BoolePoset X); :: thesis: ( F is prime iff for A being Subset of X holds
( A in F or X \ A in F ) )
BoolePoset X = InclPoset (bool X) by YELLOW_1:4;
then A1: BoolePoset X = RelStr(# (bool X),(RelIncl (bool X)) #) by YELLOW_1:def 1;
hereby :: thesis: ( ( for A being Subset of X holds
( A in F or X \ A in F ) ) implies F is prime )
assume A2: F is prime ; :: thesis: for A being Subset of X holds
( A in F or X \ A in F )
let A be Subset of X; :: thesis: ( A in F or X \ A in F )
reconsider a = A as Element of (BoolePoset X) by A1;
( a in F or 'not' a in F ) by A2, Th20;
hence ( A in F or X \ A in F ) by Th5; :: thesis: verum
end;
assume A3: for A being Subset of X holds
( A in F or X \ A in F ) ; :: thesis: F is prime
now :: thesis: for a being Element of (BoolePoset X) holds
( a in F or 'not' a in F )
let a be Element of (BoolePoset X); :: thesis: ( a in F or 'not' a in F )
'not' a = X \ a by Th5;
hence ( a in F or 'not' a in F ) by A1, A3; :: thesis: verum
end;
hence F is prime by Th20; :: thesis: verum