begin
theorem Th1:
:: deftheorem Def1 defines constitute_a_decomposition TSEP_2:def 1 :
for X being TopSpace
for A1, A2 being Subset of X holds
( A1,A2 constitute_a_decomposition iff ( A1 misses A2 & A1 \/ A2 = the carrier of X ) );
theorem
theorem
canceled;
theorem Th4:
theorem Th5:
theorem Th6:
theorem
theorem Th8:
theorem Th9:
theorem Th10:
theorem
theorem Th12:
theorem
theorem Th14:
theorem
begin
theorem Th16:
theorem
theorem
theorem Th19:
theorem
theorem
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
begin
:: deftheorem Def2 defines constitute_a_decomposition TSEP_2:def 2 :
for X being non empty TopSpace
for X1, X2 being SubSpace of X holds
( X1,X2 constitute_a_decomposition iff for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds
A1,A2 constitute_a_decomposition );
theorem Th30:
theorem
canceled;
theorem Th32:
theorem
theorem Th34:
theorem Th35:
theorem
theorem Th37:
theorem
begin
theorem Th39:
theorem
theorem Th41:
theorem
theorem
theorem
theorem
theorem Th46:
theorem
theorem
theorem