let L be Boolean LATTICE; :: thesis: for F being Filter of L holds
( ( F is proper & F is prime ) iff F is ultra )
let F be Filter of L; :: thesis: ( ( F is proper & F is prime ) iff F is ultra )
thus ( F is proper & F is prime implies F is ultra ) :: thesis: ( F is ultra implies ( F is proper & F is prime ) )

proof

assume A1: F is proper ; :: thesis: ( not F is prime or F is ultra )
assume A2: for x, y being Element of L holds
( not x "\/" y in F or x in F or y in F ) ; :: according to WAYBEL_7:def 2 :: thesis: F is ultra
thus F is proper by A1; :: according to WAYBEL_7:def 3 :: thesis: for G being Filter of L holds
( not F c= G or F = G or G = the carrier of L )
let G be Filter of L; :: thesis: ( not F c= G or F = G or G = the carrier of L )
assume A3: ( F c= G & F <> G ) ; :: thesis: G = the carrier of L
then consider x being set such that
A4: ( ( x in F & not x in G ) or ( x in G & not x in F ) ) by TARSKI:2;
reconsider x = x as Element of L by A4;
set y = 'not' x;
( x "\/" ('not' x) = Top L & Top L in F ) by WAYBEL_4:22, YELLOW_5:37;
then 'not' x in F by A2, A3, A4;
then x "/\" ('not' x) in G by A3, A4, WAYBEL_0:41;
then A5: Bottom L in G by YELLOW_5:37;
thus G c= the carrier of L ; :: according to XBOOLE_0:def 10 :: thesis: the carrier of L c= G
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of L or x in G )
assume x in the carrier of L ; :: thesis: x in G
then reconsider x = x as Element of L ;
x >= Bottom L by YELLOW_0:44;
hence x in G by A5, WAYBEL_0:def 20; :: thesis: verum

end;

assume A6: ( F is proper & ( for G being Filter of L holds
( not F c= G or F = G or G = the carrier of L ) ) ) ; :: according to WAYBEL_7:def 3 :: thesis: ( F is proper & F is prime )
hence F is proper ; :: thesis: F is prime

now

let a be Element of L; :: thesis: ( not a in F implies 'not' a in F )
assume A7: ( not a in F & not 'not' a in F ) ; :: thesis: contradiction
set b = 'not' a;
( {a} c= F \/ {a} & a in {a} ) by TARSKI:def 1, XBOOLE_1:7;
then ( F c= F \/ {a} & a in F \/ {a} & F \/ {a} c= uparrow (fininfs (F \/ {a})) ) by WAYBEL_0:62, XBOOLE_1:7;
then ( F c= uparrow (fininfs (F \/ {a})) & a in uparrow (fininfs (F \/ {a})) ) by XBOOLE_1:1;
then uparrow (fininfs (F \/ {a})) = the carrier of L by A6, A7;
then consider c being Element of L such that
A8: ( c in F & 'not' a >= c "/\" (inf {a}) ) by Lm1;
c <= Top L by YELLOW_0:45;
then A9: c = c "/\" (Top L) by YELLOW_0:25
.= c "/\" (a "\/" ('not' a)) by YELLOW_5:37
.= (c "/\" a) "\/" (c "/\" ('not' a)) by WAYBEL_1:def 3 ;
( inf {a} = a & c "/\" ('not' a) <= 'not' a ) by YELLOW_0:23, YELLOW_0:39;
then c <= 'not' a by A8, A9, YELLOW_0:22;
hence contradiction by A7, A8, WAYBEL_0:def 20; :: thesis: verum

end;

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