let L be lower-bounded continuous LATTICE; :: thesis: ( L -waybelow is multiplicative implies for p being Element of L st p is pseudoprime holds
p is prime )
assume A1: L -waybelow is multiplicative ; :: 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 )
assume p is pseudoprime ; :: thesis: p is prime
then for a, b being Element of L holds
( not a "/\" b << p or a <= p or b <= p ) by A1, Th44;
hence p is prime by A1, Lm3; :: thesis: verum