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
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;
hence PRIME L c= IRR L ; :: according to XBOOLE_0:def 10 :: thesis: IRR L c= PRIME L
now :: thesis: for l1 being object st l1 in IRR L holds
l1 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;
hence IRR L c= PRIME L ; :: thesis: verum