let L be distributive continuous LATTICE; :: thesis: for p being Element of L st uparrow (fininfs (() `)) misses waybelow p holds
p is pseudoprime

let p be Element of L; :: thesis: ( uparrow (fininfs (() `)) misses waybelow p implies p is pseudoprime )
set I = waybelow p;
set F = uparrow (fininfs (() `));
A1: ( ex_sup_of downarrow p,L & sup () = p ) by WAYBEL_0:34;
(downarrow p) ` c= uparrow (fininfs (() `)) by WAYBEL_0:62;
then A2: (uparrow (fininfs (() `))) ` c= (() `) ` by SUBSET_1:12;
assume uparrow (fininfs (() `)) 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 (() `)) 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 () ) by ;
then A7: sup P >= p by ;
take P ; :: according to WAYBEL_7:def 6 :: thesis: p = sup P
P c= (uparrow (fininfs (() `))) ` by ;
then sup P <= p by ;
hence p = sup P by ; :: thesis: verum