let L be lower-bounded distributive continuous LATTICE; :: thesis: ( ( for p being Element of L st p is pseudoprime holds
p is prime ) implies L -waybelow is multiplicative )
assume A1: for p being Element of L st p is pseudoprime holds
p is prime ; :: thesis: L -waybelow is multiplicative
given a, x, y being Element of L such that A2: ( [a,x] in L -waybelow & [a,y] in L -waybelow & not [a,(x "/\" y)] in L -waybelow ) ; :: according to WAYBEL_7:def 7 :: thesis: contradiction

now

let z be set ; :: thesis: ( z in waybelow (x "/\" y) implies not z in uparrow a )
assume A3: ( z in waybelow (x "/\" y) & z in uparrow a ) ; :: thesis: contradiction
then reconsider z = z as Element of L ;
( z << x "/\" y & z >= a ) by A3, WAYBEL_0:18, WAYBEL_3:7;
then a << x "/\" y by WAYBEL_3:2;
hence contradiction by A2, WAYBEL_4:def 2; :: thesis: verum

end;

then waybelow (x "/\" y) misses uparrow a by XBOOLE_0:3;
then consider P being Ideal of L such that
A4: ( P is prime & waybelow (x "/\" y) c= P & P misses uparrow a ) by Th27;
set p = sup P;
sup P is pseudoprime by A4, Def6;
then A5: sup P is prime by A1;
( x "/\" y = sup (waybelow (x "/\" y)) & ex_sup_of waybelow (x "/\" y),L & ex_sup_of P,L ) by WAYBEL_0:75, WAYBEL_3:def 5;
then x "/\" y <= sup P by A4, YELLOW_0:34;
then ( ( x <= sup P & a << x ) or ( y <= sup P & a << y ) ) by A2, A5, WAYBEL_4:def 2, WAYBEL_6:def 6;
then ( a << sup P & a <= a ) by WAYBEL_3:2;
then ( a in P & a in uparrow a ) by WAYBEL_0:18, WAYBEL_3:20;
hence contradiction by A4, XBOOLE_0:3; :: thesis: verum