begin
Lm1:
for L being non empty RelStr
for f being Function of NAT ,the carrier of L
for n being Element of NAT holds { (f . k) where k is Element of NAT : k <= n } is non empty finite Subset of
:: deftheorem Def1 defines closed WAYBEL12:def 1 :
:: deftheorem Def2 defines dense WAYBEL12:def 2 :
theorem
canceled;
theorem Th2:
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem Th8:
theorem
theorem
theorem
theorem Th12:
theorem Th13:
theorem Th14:
theorem
theorem Th16:
theorem
theorem Th18:
theorem
theorem Th20:
theorem Th21:
theorem
theorem Th23:
theorem
theorem Th25:
theorem
Lm2:
for L being non empty RelStr
for V being Subset of holds { x where x is Element of : V "/\" {x} c= V } is Subset of
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem
Lm3:
for L being Semilattice
for F being Filter of L holds F = uparrow (fininfs F)
:: deftheorem Def3 defines GeneratorSet WAYBEL12:def 3 :
Lm4:
for L being Semilattice
for F being Filter of L
for G being GeneratorSet of F holds G c= F
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
begin
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
:: deftheorem Def4 defines dense WAYBEL12:def 4 :
theorem
:: deftheorem Def5 defines dense WAYBEL12:def 5 :
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
:: deftheorem defines Baire WAYBEL12:def 6 :
theorem