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:31;
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 Th27;
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:43;
then sup P <= p by A6, A2, A1, XBOOLE_1:1, YELLOW_0:34;
hence p = sup P by A7, ORDERS_2:25; :: thesis: verum