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

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

hence
l is irreducible
; :: thesis: verumnot 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;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