begin
Lm1:
for A being set
for B, C, D being Subset of st B \ C = {} holds
B misses D \ C
Lm2:
for A, B, C being set holds (A /\ B) \ C = (A \ C) /\ (B \ C)
theorem Th1:
theorem Th2:
theorem
theorem Th4:
Lm3:
for X being TopStruct
for X0 being SubSpace of X holds TopStruct(# the carrier of X0,the topology of X0 #) is strict SubSpace of X
theorem Th5:
theorem
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem
theorem
theorem
theorem Th15:
:: deftheorem Def1 defines open TSEP_1:def 1 :
Lm4:
for T being TopStruct holds TopStruct(# the carrier of T,the topology of T #) is SubSpace of T
theorem Th16:
theorem
theorem
theorem
theorem Th20:
begin
:: deftheorem Def2 defines union TSEP_1:def 2 :
theorem
theorem Th22:
theorem
theorem
theorem
:: deftheorem Def3 defines misses TSEP_1:def 3 :
:: deftheorem TSEP_1:def 4 :
canceled;
:: deftheorem Def5 defines meet TSEP_1:def 5 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th29:
theorem Th30:
theorem
theorem
theorem
theorem
theorem
theorem
begin
theorem
canceled;
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
theorem Th49:
:: deftheorem TSEP_1:def 6 :
canceled;
:: deftheorem Def7 defines are_weakly_separated TSEP_1:def 7 :
theorem
canceled;
theorem Th51:
theorem Th52:
theorem Th53:
theorem Th54:
theorem Th55:
theorem Th56:
theorem Th57:
theorem Th58:
theorem Th59:
theorem Th60:
theorem Th61:
theorem Th62:
theorem Th63:
theorem Th64:
theorem Th65:
theorem Th66:
theorem Th67:
begin
:: deftheorem Def8 defines are_separated TSEP_1:def 8 :
theorem
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th77:
theorem
theorem
theorem
theorem
theorem
theorem Th83:
:: deftheorem Def9 defines are_weakly_separated TSEP_1:def 9 :
theorem
canceled;
theorem Th85:
theorem Th86:
theorem Th87:
theorem Th88:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem