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

proof

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

end;

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

proof

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

end;

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