let L be LATTICE; :: thesis: for l being Element of L st l is prime holds
l is meet-irreducible
let l be Element of L; :: thesis: ( l is prime implies l is meet-irreducible )
assume A1: l is prime ; :: thesis: l is meet-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 A3: ( l <= x & l <= y ) by YELLOW_0:23;
x "/\" y <= l by A2;
then ( x <= l or y <= l ) by A1, Def6;
hence ( x = l or y = l ) by A3, ORDERS_2:25; :: thesis: verum