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

( 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;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