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

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

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

proof

ATOM L c= (PRIME (L opp)) \ {(Bottom L)}
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;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

proof

hence
ATOM L = (PRIME (L opp)) \ {(Bottom L)}
by A1, XBOOLE_0:def 10; :: thesis: verum
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;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