begin
theorem
canceled;
theorem
canceled;
theorem Th3:
theorem Th4:
theorem Th5:
theorem
canceled;
theorem
canceled;
theorem Th8:
theorem Th9:
theorem
theorem Th11:
theorem
theorem Th13:
theorem
theorem Th15:
begin
:: deftheorem Def1 defines prime WAYBEL_7:def 1 :
theorem Th16:
theorem
:: deftheorem Def2 defines prime WAYBEL_7:def 2 :
theorem
theorem Th19:
theorem Th20:
theorem Th21:
theorem
theorem
theorem Th24:
theorem Th25:
:: deftheorem Def3 defines ultra WAYBEL_7:def 3 :
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) )
theorem Th26:
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) )
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
begin
:: deftheorem Def4 defines is_a_cluster_point_of WAYBEL_7:def 4 :
:: deftheorem Def5 defines is_a_convergence_point_of WAYBEL_7:def 5 :
theorem Th31:
theorem Th32:
theorem
theorem Th34:
theorem
theorem
theorem Th37:
begin
:: deftheorem Def6 defines pseudoprime WAYBEL_7:def 6 :
theorem Th38:
theorem Th39:
theorem
theorem
theorem
theorem
:: deftheorem Def7 defines multiplicative WAYBEL_7:def 7 :
theorem
theorem Th45:
theorem
theorem
Lm3:
now
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 2;
[u,x] in L -waybelow
by A8, WAYBEL_4:def 2;
then
[(u "/\" v),(x "/\" y)] in L -waybelow
by A1, A12, Th45;
then
u "/\" v << x "/\" y
by WAYBEL_4:def 2;
then
u "/\" v << p
by A4, WAYBEL_3:2;
hence
contradiction
by A2, A9, A11;
verum
end;
theorem Th48:
theorem
theorem