let L be LATTICE; :: thesis: for p being Element of L st p is prime holds
downarrow p is prime
let p be Element of L; :: thesis: ( p is prime implies downarrow p is prime )
assume A1: for x, y being Element of L holds
( not x "/\" y <= p or x <= p or y <= p ) ; :: according to WAYBEL_6:def 6 :: thesis: downarrow p is prime
let x, y be Element of L; :: according to WAYBEL_7:def 1 :: thesis: ( not x "/\" y in downarrow p or x in downarrow p or y in downarrow p )
assume x "/\" y in downarrow p ; :: thesis: ( x in downarrow p or y in downarrow p )
then x "/\" y <= p by WAYBEL_0:17;
then ( x <= p or y <= p ) by A1;
hence ( x in downarrow p or y in downarrow p ) by WAYBEL_0:17; :: thesis: verum