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

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