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) ` ));
assume uparrow (fininfs ((downarrow p) ` )) misses waybelow p ; :: thesis: p is pseudoprime
then consider P being Ideal of L such that
A1: ( P is prime & waybelow p c= P & P misses uparrow (fininfs ((downarrow p) ` )) ) by Th27;
reconsider P = P as prime Ideal of L by A1;
take P ; :: according to WAYBEL_7:def 6 :: thesis: p = sup P
A2: ( ex_sup_of P,L & ex_sup_of waybelow p,L & ex_sup_of downarrow p,L ) by WAYBEL_0:75;
(downarrow p) ` c= uparrow (fininfs ((downarrow p) ` )) by WAYBEL_0:62;
then ( P c= (uparrow (fininfs ((downarrow p) ` ))) ` & (uparrow (fininfs ((downarrow p) ` ))) ` c= ((downarrow p) ` ) ` & ((downarrow p) ` ) ` = downarrow p ) by A1, SUBSET_1:31, SUBSET_1:43;
then ( P c= downarrow p & sup (downarrow p) = p & p = sup (waybelow p) & sup (waybelow p) <= sup P ) by A1, A2, WAYBEL_0:34, WAYBEL_3:def 5, XBOOLE_1:1, YELLOW_0:34;
then ( sup P <= p & sup P >= p ) by A2, YELLOW_0:34;
hence p = sup P by ORDERS_2:25; :: thesis: verum