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;

( A in F or X \ A in F ) ; :: thesis: F is prime

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

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

hence
F is prime
by Th20; :: thesis: verum( 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;'not' a = X \ a by Th5;

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