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 L
:: deftheorem Def1 defines closed WAYBEL12:def 1 :
for T being TopStruct
for P being Subset of T holds
( P is closed iff P ` is open );
:: deftheorem Def2 defines dense WAYBEL12:def 2 :
for T being TopStruct
for F being Subset-Family of T holds
( F is dense iff for X being Subset of T st X in F holds
X is dense );
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 L holds { x where x is Element of L : V "/\" {x} c= V } is Subset of L
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 :
for L being Semilattice
for F being Filter of L
for b3 being Subset of L holds
( b3 is GeneratorSet of F iff F = uparrow (fininfs b3) );
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 :
for L being non empty RelStr
for u being Element of L holds
( u is dense iff for v being Element of L st v <> Bottom L holds
u "/\" v <> Bottom L );
theorem
:: deftheorem Def5 defines dense WAYBEL12:def 5 :
for L being non empty RelStr
for D being Subset of L holds
( D is dense iff for d being Element of L st d in D holds
d is dense );
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
:: deftheorem defines Baire WAYBEL12:def 6 :
for T being non empty TopSpace holds
( T is Baire iff for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds
( S is open & S is dense ) ) holds
ex I being Subset of T st
( I = Intersect F & I is dense ) );
theorem