begin
Lm1:
for t, p, s being real number st 0 < s & t <= p holds
( t < p + s & t - s < p )
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
:: deftheorem Def1 defines Partial_Intersection PROB_3:def 1 :
:: deftheorem Def2 defines Partial_Union PROB_3:def 2 :
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
:: deftheorem Def3 defines Partial_Diff_Union PROB_3:def 3 :
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
:: deftheorem Def4 defines disjoint_valued PROB_3:def 4 :
theorem Th24:
:: deftheorem defines @Partial_Intersection PROB_3:def 5 :
:: deftheorem defines @Partial_Union PROB_3:def 6 :
:: deftheorem defines @Partial_Diff_Union PROB_3:def 7 :
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th42:
theorem
theorem
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
theorem Th51:
theorem Th52:
theorem
theorem Th54:
:: deftheorem Def8 defines Complement PROB_3:def 8 :
:: deftheorem Def9 defines Intersection PROB_3:def 9 :
theorem Th55:
theorem Th56:
theorem Th57:
theorem
theorem Th59:
theorem Th60:
:: deftheorem Def10 defines FinSequence PROB_3:def 10 :
theorem Th61:
theorem Th62:
:: deftheorem defines @Complement PROB_3:def 11 :
theorem
theorem Th64:
theorem Th65:
theorem Th66:
theorem Th67:
theorem Th68:
theorem Th69:
theorem
:: deftheorem Def12 defines non-decreasing-closed PROB_3:def 12 :
:: deftheorem Def13 defines non-increasing-closed PROB_3:def 13 :
theorem Th71:
theorem Th72:
theorem Th73:
theorem Th74:
theorem Th75:
theorem
theorem Th77:
:: deftheorem PROB_3:def 14 :
canceled;
:: deftheorem Def15 defines monotoneclass PROB_3:def 15 :
theorem Th78:
theorem