environ
vocabularies HIDDEN, REWRITE1, WAYBEL_0, TARSKI, EQREL_1, XXREAL_0, LATTICES, YELLOW_0, STRUCT_0, YELLOW_1, ZFMISC_1, ORDERS_2, WELLORD2, XXREAL_2, RELAT_2, XBOOLE_0, SUBSET_1, CARD_FIL, XBOOLEAN, FINSET_1, SETFAM_1, ORDINAL2, LATTICE3, INT_2, ARYTM_0, RELAT_1, WAYBEL_6, METRIC_1, ORDINAL1, PRE_TOPC, RCOMP_1, WAYBEL_3, FUNCT_1, CANTOR_1, RLVECT_3, MSSUBFAM, WAYBEL_4, CAT_1, MCART_1, WAYBEL_7;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, RELSET_1, FUNCT_1, FINSET_1, FUNCT_2, DOMAIN_1, ORDERS_1, STRUCT_0, PRE_TOPC, TOPS_2, CANTOR_1, ORDINAL1, ORDERS_2, LATTICE3, ALG_1, YELLOW_0, WAYBEL_0, YELLOW_1, WAYBEL_1, YELLOW_3, WAYBEL_3, YELLOW_7, WAYBEL_6, WAYBEL_4;
definitions TARSKI, YELLOW_0, WAYBEL_0, PRE_TOPC, TOPS_2, WAYBEL_3, WAYBEL_6, XBOOLE_0, STRUCT_0;
theorems TARSKI, ZFMISC_1, SUBSET_1, CANTOR_1, TOPS_2, SETFAM_1, ORDERS_2, YELLOW_0, WAYBEL_0, ORDERS_1, YELLOW_2, WAYBEL_1, YELLOW_1, WAYBEL_3, FINSET_1, FUNCT_1, LATTICE3, WAYBEL_6, YELLOW_7, WAYBEL_5, WAYBEL_4, YELLOW_3, MCART_1, FUNCT_5, YELLOW_5, ORDINAL1, XBOOLE_0, XBOOLE_1, STRUCT_0;
schemes FUNCT_1, FINSET_1;
registrations XBOOLE_0, SUBSET_1, FINSET_1, STRUCT_0, PRE_TOPC, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, YELLOW_3, WAYBEL_3, WAYBEL_4, YELLOW_7, WAYBEL_6, RELAT_1;
constructors HIDDEN, SETFAM_1, DOMAIN_1, TOPS_2, TEX_2, CANTOR_1, WAYBEL_1, YELLOW_3, YELLOW_4, WAYBEL_3, WAYBEL_4, WAYBEL_6;
requirements HIDDEN, SUBSET, BOOLE;
equalities YELLOW_0, WAYBEL_0, WAYBEL_3, SUBSET_1, STRUCT_0;
expansions TARSKI, YELLOW_0, WAYBEL_0, PRE_TOPC, TOPS_2, WAYBEL_3, WAYBEL_6, XBOOLE_0, SUBSET_1, STRUCT_0;
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) )
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;
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;