begin
theorem Th1:
theorem
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
Lm1:
for X, Y being set holds
( X c= Y iff X is Subset of Y )
;
begin
:: deftheorem Def1 defines trivial TEX_1:def 1 :
theorem
begin
:: deftheorem defines cobool TEX_1:def 2 :
:: deftheorem defines ADTS TEX_1:def 3 :
theorem
canceled;
theorem
canceled;
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem Th23:
begin
:: deftheorem TEX_1:def 4 :
canceled;
:: deftheorem defines STS TEX_1:def 5 :
theorem Th24:
theorem Th25:
theorem Th26:
theorem
theorem Th28:
theorem Th29:
theorem
theorem
theorem
theorem
theorem
begin
:: deftheorem Def6 defines discrete TEX_1:def 6 :
theorem
:: deftheorem Def7 defines almost_discrete TEX_1:def 7 :
theorem Th36:
theorem Th37:
theorem
theorem Th39:
theorem
theorem