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 :
theorem
theorem
theorem
theorem Th8:
theorem Th9:
begin
:: deftheorem Def2 defines meet-irreducible WAYBEL_6:def 2 :
:: deftheorem defines join-irreducible WAYBEL_6:def 3 :
:: deftheorem Def4 defines IRR WAYBEL_6:def 4 :
theorem Th10:
theorem
theorem
theorem Th13:
theorem Th14:
begin
:: deftheorem Def5 defines order-generating WAYBEL_6:def 5 :
theorem Th15:
theorem
theorem Th17:
theorem Th18:
theorem Th19:
begin
:: deftheorem Def6 defines prime WAYBEL_6:def 6 :
:: deftheorem Def7 defines PRIME WAYBEL_6:def 7 :
:: deftheorem Def8 defines co-prime WAYBEL_6:def 8 :
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 ex X being Subset of st
( l = sup X & ( for x being Element of 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 ex X being Subset of st
( l = sup X & ( for x being Element of st x in X holds
x is co-prime ) )
theorem
theorem