let L be LATTICE; :: thesis: for p being Element of L st p is prime holds
p is pseudoprime
let p be Element of L; :: thesis: ( p is prime implies p is pseudoprime )
assume p is prime ; :: thesis: p is pseudoprime
then A1: downarrow p is prime by Th33;
p = sup (downarrow p) by WAYBEL_0:34;
hence ex P being prime Ideal of L st p = sup P by A1; :: according to WAYBEL_7:def 6 :: thesis: verum