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

proof

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

end;

A3: Bottom L is_greater_than {}

proof

for q being Element of L st q in {} holds
q [= Bottom L ;
hence Bottom L is_greater_than {} by LATTICE3:def 17; :: thesis: verum

end;

A4: for b being Element of L st b is_greater_than {} holds
Bottom L [= b by LATTICES:41;
A5: (Bottom L) % = Bottom (LattPOSet L)

proof

Bottom (LattPOSet L) = "\/" {} ,(LattPOSet L) by YELLOW_0:def 11
.= "\/" {} ,L by YELLOW_0:29
.= Bottom L by A3, A4, LATTICE3:def 21 ;
hence (Bottom L) % = Bottom (LattPOSet L) by LATTICE3:def 3; :: thesis: verum

end;

Bottom (LattPOSet L) is join-irreducible

proof

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

proof

let x, y be Element of (LattPOSet L); :: thesis: ( not Bottom (LattPOSet L) = x "\/" y or x = Bottom (LattPOSet L) or y = Bottom (LattPOSet L) )
assume Bottom (LattPOSet L) = x "\/" y ; :: thesis: ( x = Bottom (LattPOSet L) or y = Bottom (LattPOSet L) )
then A6: ( Bottom (LattPOSet L) >= x & Bottom (LattPOSet L) >= y ) by YELLOW_0:22;
reconsider L' = LattPOSet L as non empty antisymmetric lower-bounded RelStr ;
reconsider x' = x as Element of L' ;
reconsider y' = y as Element of L' ;
( x' >= Bottom L' or y' >= Bottom L' ) by YELLOW_0:44;
hence ( x = Bottom (LattPOSet L) or y = Bottom (LattPOSet L) ) by A6, ORDERS_2:25; :: thesis: verum

end;

hence Bottom (LattPOSet L) is join-irreducible by WAYBEL_6:def 3; :: thesis: verum

end;

hence ( *' (Bottom L) = Bottom L & (Bottom L) % is join-irreducible ) by A1, A3, A4, A5, LATTICE3:def 21; :: thesis: verum