let L be complete Lattice; :: thesis: for a being Element of L st a is co-atomic holds
a is completely-meet-irreducible
let a be Element of L; :: thesis: ( a is co-atomic implies a is completely-meet-irreducible )
set X = { x where x is Element of L : ( a [= x & x <> a ) } ;
assume a is co-atomic ; :: thesis: a is completely-meet-irreducible
then A1: a is-lower-neighbour-of Top L ;
then A2: a <> Top L ;
A3: for x being object st x in { x where x is Element of L : ( a [= x & x <> a ) } holds
x in {(Top L)}

proof

let x be object ; :: thesis: ( x in { x where x is Element of L : ( a [= x & x <> a ) } implies x in {(Top L)} )
assume x in { x where x is Element of L : ( a [= x & x <> a ) } ; :: thesis: x in {(Top L)}
then A4: ex x9 being Element of L st
( x9 = x & a [= x9 & x9 <> a ) ;
then reconsider x = x as Element of L ;
x [= Top L by LATTICES:19;
then x = Top L by A1, A4;
hence x in {(Top L)} by TARSKI:def 1; :: thesis: verum

end;

A5: a [= Top L by A1;
A6: for x being object st x in {(Top L)} holds
x in { x where x is Element of L : ( a [= x & x <> a ) }

proof

let x be object ; :: thesis: ( x in {(Top L)} implies x in { x where x is Element of L : ( a [= x & x <> a ) } )
assume x in {(Top L)} ; :: thesis: x in { x where x is Element of L : ( a [= x & x <> a ) }
then x = Top L by TARSKI:def 1;
hence x in { x where x is Element of L : ( a [= x & x <> a ) } by A2, A5; :: thesis: verum

end;

Top L = "/\" ({(Top L)},L) by LATTICE3:42
.= a *' by A3, A6, TARSKI:2 ;
hence a is completely-meet-irreducible by A2; :: thesis: verum