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 ex c being Element of L st
( c in {a,b} & c <= p ) by A2, Th35;
hence ( a <= p or b <= p ) by 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
hence p is pseudoprime by A1, Lm3, Th34; :: thesis: verum