let L be complete Lattice; :: thesis: ( (Top L) *' = Top L & (Top L) % is meet-irreducible )
set X = { d where d is Element of L : ( Top L [= d & d <> Top L ) } ;
A1: { d where d is Element of L : ( Top L [= d & d <> Top L ) } = {}

proof

assume { d where d is Element of L : ( Top L [= d & d <> Top L ) } <> {} ; :: thesis: contradiction
then reconsider X = { d where d is Element of L : ( Top L [= d & d <> Top 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 & Top L [= x' & x' <> Top L ) ;
x' [= Top L by LATTICES:45;
hence contradiction by A2, LATTICES:26; :: thesis: verum

end;

A3: Top L is_less_than {}

proof

for q being Element of L st q in {} holds
Top L [= q ;
hence Top L is_less_than {} by LATTICE3:def 16; :: thesis: verum

end;

A4: for b being Element of L st b is_less_than {} holds
b [= Top L by LATTICES:45;
(Top L) % = Top (LattPOSet L)

proof

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

end;

hence ( (Top L) *' = Top L & (Top L) % is meet-irreducible ) by A1, A3, A4, LATTICE3:34, WAYBEL_6:10; :: thesis: verum