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

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