let L be complete Lattice; ( *' (Bottom L) = Bottom L & (Bottom L) % is join-irreducible )
set X = { d where d is Element of L : ( d [= Bottom L & d <> Bottom L ) } ;
A1:
{ d where d is Element of L : ( d [= Bottom L & d <> Bottom L ) } = {}
A3:
for b being Element of L st b is_greater_than {} holds
Bottom L [= b
by LATTICES:16;
A4:
for x, y being Element of (LattPOSet L) holds
( not Bottom (LattPOSet L) = x "\/" y or x = Bottom (LattPOSet L) or y = Bottom (LattPOSet L) )
for q being Element of L st q in {} holds
q [= Bottom L
;
then A6:
Bottom L is_greater_than {}
by LATTICE3:def 17;
Bottom (LattPOSet L) =
"\/" ({},(LattPOSet L))
by YELLOW_0:def 11
.=
"\/" ({},L)
by YELLOW_0:29
.=
Bottom L
by A6, A3, LATTICE3:def 21
;
then
(Bottom L) % = Bottom (LattPOSet L)
by LATTICE3:def 3;
hence
( *' (Bottom L) = Bottom L & (Bottom L) % is join-irreducible )
by A1, A6, A3, A4, LATTICE3:def 21, WAYBEL_6:def 3; verum