let L be lower-bounded continuous LATTICE; :: thesis: ( L -waybelow is multiplicative implies for p being Element of L holds
( p is pseudoprime iff for a, b being Element of L holds
( not a "/\" b << p or a <= p or b <= p ) ) )
assume A1: L -waybelow is multiplicative ; :: thesis: for p being Element of L holds
( p is pseudoprime iff for a, b being Element of L holds
( not a "/\" b << p or a <= p or b <= p ) )
let p be Element of L; :: thesis: ( p is pseudoprime iff for a, b being Element of L holds
( not a "/\" b << p or a <= p or b <= p ) )

hereby :: thesis: ( ( for a, b being Element of L holds
( not a "/\" b << p or a <= p or b <= p ) ) implies p is pseudoprime )

assume A2: p is pseudoprime ; :: thesis: for a, b being Element of L holds
( not a "/\" b << p or a <= p or b <= p )
let a, b be Element of L; :: thesis: ( not a "/\" b << p or a <= p or b <= p )
assume a "/\" b << p ; :: thesis: ( a <= p or b <= p )
then inf {a,b} << p by YELLOW_0:40;
then consider c being Element of L such that
A3: ( c in {a,b} & c <= p ) by A2, Th39;
thus ( a <= p or b <= p ) by A3, TARSKI:def 2; :: thesis: verum

end;

assume for a, b being Element of L holds
( not a "/\" b << p or a <= p or b <= p ) ; :: thesis: p is pseudoprime
then p is prime by A1, Lm3;
hence p is pseudoprime by Th38; :: thesis: verum