let L be LATTICE; for l being Element of L st (uparrow l) \ {l} is Filter of L holds
l is irreducible
let l be Element of L; ( (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
; l is irreducible
now for x, y being Element of L st l = x "/\" y & x <> l holds
not y <> llet x,
y be
Element of
L;
( l = x "/\" y & x <> l implies not y <> l )assume that A2:
l = x "/\" y
and A3:
x <> l
and A4:
y <> l
;
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;
verum end;
hence
l is irreducible
; verum