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 ( downarrow p is prime & p = sup (downarrow p) ) by Th37, WAYBEL_0:34;
hence ex P being prime Ideal of L st p = sup P ; :: according to WAYBEL_7:def 6 :: thesis: verum