let L be lower-bounded arithmetic LATTICE; :: thesis: for p being Element of L st p is pseudoprime holds
p is prime
let p be Element of L; :: thesis: ( p is pseudoprime implies p is prime )
L -waybelow is multiplicative by Th20;
hence ( p is pseudoprime implies p is prime ) by WAYBEL_7:45; :: thesis: verum