begin
theorem Th1:
theorem Th2:
Lm1:
for X being non empty set
for a, b, c being Element of X holds a,b followed_by c is Function of NAT ,X
;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th6:
:: deftheorem DYNKIN:def 1 :
canceled;
:: deftheorem Def2 defines seqIntersection DYNKIN:def 2 :
begin
:: deftheorem Def3 defines disjoint_valued DYNKIN:def 3 :
theorem Th7:
:: deftheorem DYNKIN:def 4 :
canceled;
:: deftheorem defines disjointify DYNKIN:def 5 :
:: deftheorem Def6 defines disjointify DYNKIN:def 6 :
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
begin
:: deftheorem Def7 defines Dynkin_System DYNKIN:def 7 :
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
begin
theorem Th23:
:: deftheorem Def8 defines generated_Dynkin_System DYNKIN:def 8 :
:: deftheorem Def9 defines DynSys DYNKIN:def 9 :
theorem Th24:
theorem Th25:
theorem Th26:
theorem