let L be distributive LATTICE; :: thesis: for l being Element of L holds
( l is prime iff l is irreducible )
let l be Element of L; :: thesis: ( l is prime iff l is irreducible )
thus ( l is prime implies l is irreducible ) by Th24; :: thesis: ( l is irreducible implies l is prime )
thus ( l is irreducible implies l is prime ) :: thesis: verum

proof

assume A1: l is irreducible ; :: thesis: l is prime
let x, y be Element of L; :: according to WAYBEL_6:def 6 :: thesis: ( not x "/\" y <= l or x <= l or y <= l )
assume x "/\" y <= l ; :: thesis: ( x <= l or y <= l )
then l = l "\/" (x "/\" y) by YELLOW_0:24
.= (l "\/" x) "/\" (l "\/" y) by WAYBEL_1:5 ;
then ( l = l "\/" x or l = l "\/" y ) by A1;
hence ( x <= l or y <= l ) by YELLOW_0:24; :: thesis: verum

end;