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

now :: thesis: for x, y being Element of L st l = x "/\" y & x <> l holds
not y <> l

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

end;

hence l is irreducible ; :: thesis: verum