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 that
A3: F c= G and
A4: F <> G ; :: thesis: G = the carrier of L
consider x being object such that
A5: ( ( x in F & not x in G ) or ( x in G & not x in F ) ) by A4, TARSKI:2;
reconsider x = x as Element of L by A5;
set y = 'not' x;
x "\/" ('not' x) = Top L by YELLOW_5:34;
then 'not' x in F by A2, A3, A5, WAYBEL_4:22;
then x "/\" ('not' x) in G by A3, A5, WAYBEL_0:41;
then A6: Bottom L in G by YELLOW_5:34;
thus G c= the carrier of L ; :: according to XBOOLE_0:def 10 :: thesis: the carrier of L c= G
let x be object ; :: 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 A6, WAYBEL_0:def 20; :: thesis: verum

end;

assume that
A7: F is proper and
A8: 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 )
thus F is proper by A7; :: thesis: F is prime

now :: thesis: for a being Element of L st not a in F holds
'not' a in F

let a be Element of L; :: thesis: ( not a in F implies 'not' a in F )
assume that
A9: not a in F and
A10: not 'not' a in F ; :: thesis: contradiction
set b = 'not' a;
A11: F \/ {a} c= uparrow (fininfs (F \/ {a})) by WAYBEL_0:62;
( {a} c= F \/ {a} & a in {a} ) by TARSKI:def 1, XBOOLE_1:7;
then a in F \/ {a} ;
then ( F c= F \/ {a} & a in uparrow (fininfs (F \/ {a})) ) by A11, XBOOLE_1:7;
then uparrow (fininfs (F \/ {a})) = the carrier of L by A8, A9, A11, XBOOLE_1:1;
then consider c being Element of L such that
A12: c in F and
A13: 'not' a >= c "/\" (inf {a}) by Lm1;
c <= Top L by YELLOW_0:45;
then A14: c = c "/\" (Top L) by YELLOW_0:25
.= c "/\" (a "\/" ('not' a)) by YELLOW_5:34
.= (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 A13, A14, YELLOW_0:22;
hence contradiction by A10, A12, WAYBEL_0:def 20; :: thesis: verum

end;

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