let L be distributive continuous LATTICE; :: thesis: for p being Element of L st uparrow (fininfs ((downarrow p) `)) misses waybelow p holds
p is pseudoprime
let p be Element of L; :: thesis: ( uparrow (fininfs ((downarrow p) `)) misses waybelow p implies p is pseudoprime )
set I = waybelow p;
set F = uparrow (fininfs ((downarrow p) `));
A1: ( ex_sup_of downarrow p,L & sup (downarrow p) = p ) by WAYBEL_0:34;
(downarrow p) ` c= uparrow (fininfs ((downarrow p) `)) by WAYBEL_0:62;
then A2: (uparrow (fininfs ((downarrow p) `))) ` c= ((downarrow p) `) ` by SUBSET_1:12;
assume uparrow (fininfs ((downarrow p) `)) misses waybelow p ; :: thesis: p is pseudoprime
then consider P being Ideal of L such that
A3: P is prime and
A4: waybelow p c= P and
A5: P misses uparrow (fininfs ((downarrow p) `)) by Th23;
reconsider P = P as prime Ideal of L by A3;
A6: ex_sup_of P,L by WAYBEL_0:75;
( ex_sup_of waybelow p,L & p = sup (waybelow p) ) by WAYBEL_0:75, WAYBEL_3:def 5;
then A7: sup P >= p by A4, A6, YELLOW_0:34;
take P ; :: according to WAYBEL_7:def 6 :: thesis: p = sup P
P c= (uparrow (fininfs ((downarrow p) `))) ` by A5, SUBSET_1:23;
then sup P <= p by A6, A2, A1, XBOOLE_1:1, YELLOW_0:34;
hence p = sup P by A7, ORDERS_2:2; :: thesis: verum