let L be complete Lattice; :: thesis:
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 ) } = {}

assume { d where d is Element of L : ( d [= Bottom L & d <> Bottom L ) } <> {} ; :: thesis:
then reconsider X = { d where d is Element of L : ( d [= Bottom L & d <> Bottom L ) } as non empty set ;
set x = the Element of X;
the Element of X in X ;
then consider x9 being Element of L such that
x9 = the Element of X and
A2: ( x9 [= Bottom L & x9 <> Bottom L ) ;
Bottom L [= x9 by LATTICES:16;
hence contradiction by A2, LATTICES:8; :: thesis:

end;

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) )

reconsider L9 = LattPOSet L as non empty antisymmetric lower-bounded RelStr ;
let x, y be Element of (LattPOSet L); :: thesis:
reconsider x9 = x as Element of L9 ;
reconsider y9 = y as Element of L9 ;
assume Bottom (LattPOSet L) = x "\/" y ; :: thesis:
then A5: ( Bottom (LattPOSet L) >= x & Bottom (LattPOSet L) >= y ) by YELLOW_0:22;
( x9 >= Bottom L9 or y9 >= Bottom L9 ) by YELLOW_0:44;
hence ( x = Bottom (LattPOSet L) or y = Bottom (LattPOSet L) ) by A5, ORDERS_2:2; :: thesis:

end;

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; :: thesis: