let L be LATTICE; :: thesis: for l being Element of L st l is prime holds
l is irreducible
let l be Element of L; :: thesis: ( l is prime implies l is irreducible )
assume A1: l is prime ; :: thesis: l is irreducible
let x, y be Element of L; :: according to WAYBEL_6:def 2 :: thesis: ( not l = x "/\" y or x = l or y = l )
assume A2: l = x "/\" y ; :: thesis: ( x = l or y = l )
then x "/\" y <= l ;
then A3: ( x <= l or y <= l ) by A1;
( l <= x & l <= y ) by A2, YELLOW_0:23;
hence ( x = l or y = l ) by A3, ORDERS_2:2; :: thesis: verum