let L be LATTICE; :: thesis: for l being Element of L st (uparrow l) \ {l} is Filter of L holds
l is meet-irreducible
let l be Element of L; :: thesis: ( (uparrow l) \ {l} is Filter of L implies l is meet-irreducible )
assume A1: (uparrow l) \ {l} is Filter of L ; :: thesis: l is meet-irreducible
set F = (uparrow l) \ {l};

now

let x, y be Element of L; :: thesis: ( l = x "/\" y & x <> l implies not y <> l )
assume A2: ( l = x "/\" y & x <> l & y <> l ) ; :: thesis: contradiction
then ( l <= x & l <= y ) by YELLOW_0:23;
then ( x in uparrow l & y in uparrow l ) by WAYBEL_0:18;
then ( x in (uparrow l) \ {l} & y in (uparrow l) \ {l} ) by A2, ZFMISC_1:64;
then consider z being Element of L such that
A3: ( z in (uparrow l) \ {l} & z <= x & z <= y ) by A1, WAYBEL_0:def 2;
l >= z by A2, A3, YELLOW_0:23;
then l in (uparrow l) \ {l} by A1, A3, WAYBEL_0:def 20;
hence contradiction by ZFMISC_1:64; :: thesis: verum

end;

hence l is meet-irreducible by Def2; :: thesis: verum