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 ;
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: ( Top L [= x9 & x9 <> Top L ) ;
x9 [= Top L by LATTICES:19;
hence contradiction by A2, LATTICES:8; :: thesis: verum
end;
A3: for b being Element of L st b is_less_than {} holds
b [= Top L by LATTICES:19;
for q being Element of L st q in {} holds
Top L [= q ;
then A4: Top L is_less_than {} by LATTICE3:def 16;
Top (LattPOSet L) = "/\" ({},(LattPOSet L)) by YELLOW_0:def 12
.= "/\" ({},L) by YELLOW_0:29
.= Top L by A4, A3, LATTICE3:34 ;
then (Top L) % = Top (LattPOSet L) by LATTICE3:def 3;
hence ( (Top L) *' = Top L & (Top L) % is meet-irreducible ) by A1, A4, A3, LATTICE3:34, WAYBEL_6:10; :: thesis: verum