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

now :: thesis: for l1 being object st l1 in PRIME L holds

l1 in IRR L

hence
PRIME L c= IRR L
; :: according to XBOOLE_0:def 10 :: thesis: IRR L c= PRIME Ll1 in IRR L

let l1 be object ; :: 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 irreducible by Th27;

hence l1 in IRR L by Def4; :: thesis: verum

end;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 irreducible by Th27;

hence l1 in IRR L by Def4; :: thesis: verum

now :: thesis: for l1 being object st l1 in IRR L holds

l1 in PRIME L

hence
IRR L c= PRIME L
; :: thesis: veruml1 in PRIME L

let l1 be object ; :: 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 irreducible by A2, Def4;

then l is prime by Th27;

hence l1 in PRIME L by Def7; :: thesis: verum

end;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 irreducible by A2, Def4;

then l is prime by Th27;

hence l1 in PRIME L by Def7; :: thesis: verum