begin
theorem Th1:
theorem Th2:
theorem Th3:
Lm1:
for S, T being non empty with_suprema Poset
for f being Function of S,T st f is directed-sups-preserving holds
f is monotone
theorem Th4:
begin
:: deftheorem Def1 defines Open WAYBEL_6:def 1 :
for L being non empty reflexive RelStr
for X being Subset of L holds
( X is Open iff for x being Element of L st x in X holds
ex y being Element of L st
( y in X & y << x ) );
theorem
theorem
theorem
theorem Th8:
theorem Th9:
begin
:: deftheorem Def2 defines meet-irreducible WAYBEL_6:def 2 :
for G being non empty RelStr
for g being Element of G holds
( g is meet-irreducible iff for x, y being Element of G holds
( not g = x "/\" y or x = g or y = g ) );
:: deftheorem defines join-irreducible WAYBEL_6:def 3 :
for G being non empty RelStr
for g being Element of G holds
( g is join-irreducible iff for x, y being Element of G holds
( not g = x "\/" y or x = g or y = g ) );
:: deftheorem Def4 defines IRR WAYBEL_6:def 4 :
for L being non empty RelStr
for b2 being Subset of L holds
( b2 = IRR L iff for x being Element of L holds
( x in b2 iff x is meet-irreducible ) );
theorem Th10:
theorem
theorem
theorem Th13:
theorem Th14:
begin
:: deftheorem Def5 defines order-generating WAYBEL_6:def 5 :
for L being non empty RelStr
for X being Subset of L holds
( X is order-generating iff for x being Element of L holds
( ex_inf_of (uparrow x) /\ X,L & x = inf ((uparrow x) /\ X) ) );
theorem Th15:
theorem
theorem Th17:
theorem Th18:
theorem Th19:
begin
:: deftheorem Def6 defines prime WAYBEL_6:def 6 :
for L being non empty RelStr
for l being Element of L holds
( l is prime iff for x, y being Element of L holds
( not x "/\" y <= l or x <= l or y <= l ) );
:: deftheorem Def7 defines PRIME WAYBEL_6:def 7 :
for L being non empty RelStr
for b2 being Subset of L holds
( b2 = PRIME L iff for x being Element of L holds
( x in b2 iff x is prime ) );
:: deftheorem Def8 defines co-prime WAYBEL_6:def 8 :
for L being non empty RelStr
for l being Element of L holds
( l is co-prime iff l ~ is prime );
theorem Th20:
theorem
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem
theorem
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem
theorem Th37:
Lm2:
for L being complete continuous LATTICE st ( for l being Element of L ex X being Subset of L st
( l = sup X & ( for x being Element of L st x in X holds
x is co-prime ) ) ) holds
L is completely-distributive
Lm3:
for L being complete completely-distributive LATTICE holds
( L is distributive & L is continuous & L ~ is continuous )
Lm4:
for L being complete LATTICE st L is distributive & L is continuous & L ~ is continuous holds
for l being Element of L ex X being Subset of L st
( l = sup X & ( for x being Element of L st x in X holds
x is co-prime ) )
theorem
theorem