begin
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem
theorem Th8:
theorem Th9:
theorem
theorem Th11:
theorem Th12:
begin
theorem
theorem
theorem
Lm1:
for T being non empty TopStruct
for A being Subset of
for p being Point of st p in Cl A holds
for K being Basis of
for Q being Subset of st Q in K holds
A meets Q
Lm2:
for T being non empty TopStruct
for A being Subset of
for p being Point of st ( for K being Basis of
for Q being Subset of st Q in K holds
A meets Q ) holds
ex K being Basis of st
for Q being Subset of st Q in K holds
A meets Q
Lm3:
for T being non empty TopStruct
for A being Subset of
for p being Point of st ex K being Basis of st
for Q being Subset of st Q in K holds
A meets Q holds
p in Cl A
theorem
theorem
:: deftheorem Def1 defines basis YELLOW13:def 1 :
:: deftheorem defines basis YELLOW13:def 2 :
theorem Th18:
theorem Th19:
:: deftheorem Def3 defines correct YELLOW13:def 3 :
theorem
theorem
theorem
theorem
:: deftheorem Def4 defines basis YELLOW13:def 4 :
theorem Th24:
theorem Th25:
theorem
theorem
:: deftheorem Def5 defines topological_semilattice YELLOW13:def 5 :
theorem Th28: