begin
begin
Lm1:
for L being with_infima Poset
for F being Filter of L
for X being non empty finite Subset of L
for x being Element of L st x in uparrow (fininfs (F \/ X)) holds
ex a being Element of L st
( a in F & x >= a "/\" (inf X) )
Lm2:
for L being with_suprema Poset
for I being Ideal of L
for X being non empty finite Subset of L
for x being Element of L st x in downarrow (finsups (I \/ X)) holds
ex i being Element of L st
( i in I & x <= i "\/" (sup X) )
begin
begin
Lm3:
now for L being lower-bounded continuous LATTICE
for p being Element of L st L -waybelow is multiplicative & ( for a, b being Element of L holds
( not a "/\" b << p or a <= p or b <= p ) ) holds
p is prime
let L be
lower-bounded continuous LATTICE;
for p being Element of L st L -waybelow is multiplicative & ( for a, b being Element of L holds
( not a "/\" b << p or a <= p or b <= p ) ) holds
p is prime let p be
Element of
L;
( L -waybelow is multiplicative & ( for a, b being Element of L holds
( not a "/\" b << p or a <= p or b <= p ) ) implies p is prime )assume that A1:
L -waybelow is
multiplicative
and A2:
for
a,
b being
Element of
L holds
( not
a "/\" b << p or
a <= p or
b <= p )
and A3:
not
p is
prime
;
contradictionconsider x,
y being
Element of
L such that A4:
x "/\" y <= p
and A5:
not
x <= p
and A6:
not
y <= p
by A3, WAYBEL_6:def 6;
A7:
for
a being
Element of
L holds
( not
waybelow a is
empty &
waybelow a is
directed )
;
then consider u being
Element of
L such that A8:
u << x
and A9:
not
u <= p
by A5, WAYBEL_3:24;
consider v being
Element of
L such that A10:
v << y
and A11:
not
v <= p
by A6, A7, WAYBEL_3:24;
A12:
[v,y] in L -waybelow
by A10, WAYBEL_4:def 1;
[u,x] in L -waybelow
by A8, WAYBEL_4:def 1;
then
[(u "/\" v),(x "/\" y)] in L -waybelow
by A1, A12, Th41;
then
u "/\" v << x "/\" y
by WAYBEL_4:def 1;
then
u "/\" v << p
by A4, WAYBEL_3:2;
hence
contradiction
by A2, A9, A11;
verum
end;