let L be Boolean LATTICE; :: thesis: ATOM L = (PRIME (L opp)) \ {(Bottom L)}
A1: (PRIME (L opp)) \ {(Bottom L)} c= ATOM L

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (PRIME (L opp)) \ {(Bottom L)} or x in ATOM L )
assume A2: x in (PRIME (L opp)) \ {(Bottom L)} ; :: thesis: x in ATOM L
then reconsider x9 = x as Element of (L opp) ;
x in PRIME (L opp) by A2, XBOOLE_0:def 5;
then A3: x9 is prime by WAYBEL_6:def 7;
not x in {(Bottom L)} by A2, XBOOLE_0:def 5;
then x9 <> Bottom L by TARSKI:def 1;
then A4: ~ x9 <> Bottom L by LATTICE3:def 7;
(~ x9) ~ = ~ x9 by LATTICE3:def 6
.= x9 by LATTICE3:def 7 ;
then ~ x9 is co-prime by A3, WAYBEL_6:def 8;
then ~ x9 is atom by A4, Th20;
then ~ x9 in ATOM L by Def2;
hence x in ATOM L by LATTICE3:def 7; :: thesis: verum

end;

ATOM L c= (PRIME (L opp)) \ {(Bottom L)}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ATOM L or x in (PRIME (L opp)) \ {(Bottom L)} )
assume A5: x in ATOM L ; :: thesis: x in (PRIME (L opp)) \ {(Bottom L)}
then reconsider x9 = x as Element of L ;
A6: x9 is atom by A5, Def2;
then x9 ~ is prime by WAYBEL_6:def 8;
then x9 ~ in PRIME (L opp) by WAYBEL_6:def 7;
then A7: x in PRIME (L opp) by LATTICE3:def 6;
x <> Bottom L by A6;
then not x in {(Bottom L)} by TARSKI:def 1;
hence x in (PRIME (L opp)) \ {(Bottom L)} by A7, XBOOLE_0:def 5; :: thesis: verum

end;

hence ATOM L = (PRIME (L opp)) \ {(Bottom L)} by A1, XBOOLE_0:def 10; :: thesis: verum