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 ) and
A3: not [a,(x "/\" y)] in L -waybelow ; :: according to WAYBEL_7:def 7 :: thesis: contradiction
now :: thesis: for z being object st z in waybelow (x "/\" y) holds
not z in uparrow a
let z be object ; :: thesis: ( z in waybelow (x "/\" y) implies not z in uparrow a )
assume that
A4: z in waybelow (x "/\" y) and
A5: z in uparrow a ; :: thesis: contradiction
reconsider z = z as Element of L by A4;
( z << x "/\" y & z >= a ) by A4, A5, WAYBEL_0:18, WAYBEL_3:7;
then a << x "/\" y by WAYBEL_3:2;
hence contradiction by A3, WAYBEL_4:def 1; :: thesis: verum
end;
then waybelow (x "/\" y) misses uparrow a by XBOOLE_0:3;
then consider P being Ideal of L such that
A6: P is prime and
A7: waybelow (x "/\" y) c= P and
A8: P misses uparrow a by Th23;
set p = sup P;
sup P is pseudoprime by A6;
then A9: sup P is prime by A1;
a <= a ;
then A10: a in uparrow a by WAYBEL_0:18;
A11: ( x "/\" y = sup (waybelow (x "/\" y)) & ex_sup_of waybelow (x "/\" y),L ) by WAYBEL_0:75, WAYBEL_3:def 5;
ex_sup_of P,L by WAYBEL_0:75;
then x "/\" y <= sup P by A7, A11, YELLOW_0:34;
then ( ( x <= sup P & a << x ) or ( y <= sup P & a << y ) ) by A2, A9, WAYBEL_4:def 1;
then a in P by WAYBEL_3:20;
hence contradiction by A8, A10, XBOOLE_0:3; :: thesis: verum