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, Th24;
hence ( A in F or X \ A in F ) by Th9; :: 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

let a be Element of (BoolePoset X); :: thesis: ( a in F or 'not' a in F )
'not' a = X \ a by Th9;
hence ( a in F or 'not' a in F ) by A1, A3; :: thesis: verum

end;

hence F is prime by Th24; :: thesis: verum