let L be distributive LATTICE; :: thesis: PRIME L = IRR L

now

let l1 be set ; :: thesis: ( l1 in PRIME L implies l1 in IRR L )
assume A1: l1 in PRIME L ; :: thesis: l1 in IRR L
then reconsider l = l1 as Element of PRIME L ;
reconsider l = l as Element of L by A1;
l is prime by A1, Def7;
then l is meet-irreducible by Th27;
hence l1 in IRR L by Def4; :: thesis: verum

end;

hence PRIME L c= IRR L by TARSKI:def 3; :: according to XBOOLE_0:def 10 :: thesis: IRR L c= PRIME L

now

let l1 be set ; :: thesis: ( l1 in IRR L implies l1 in PRIME L )
assume A2: l1 in IRR L ; :: thesis: l1 in PRIME L
then reconsider l = l1 as Element of IRR L ;
reconsider l = l as Element of L by A2;
l is meet-irreducible by A2, Def4;
then l is prime by Th27;
hence l1 in PRIME L by Def7; :: thesis: verum

end;

hence IRR L c= PRIME L by TARSKI:def 3; :: thesis: verum