begin
:: deftheorem Def1 defines orientedly_joins GRAPH_4:def 1 :
theorem Th1:
:: deftheorem defines are_orientedly_incident GRAPH_4:def 2 :
theorem Th2:
:: deftheorem defines -SVSet GRAPH_4:def 3 :
:: deftheorem defines -TVSet GRAPH_4:def 4 :
theorem
canceled;
theorem
:: deftheorem Def5 defines is_oriented_vertex_seq_of GRAPH_4:def 5 :
theorem Th5:
theorem
theorem
theorem
begin
theorem
theorem Th10:
theorem Th11:
:: deftheorem defines oriented-vertex-seq GRAPH_4:def 6 :
theorem
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
begin
Lm1:
for G being Graph
for v being Element of G holds <*v*> is_oriented_vertex_seq_of {}
:: deftheorem Def7 defines Simple GRAPH_4:def 7 :
theorem
canceled;
theorem Th18:
theorem
theorem Th20:
theorem Th21:
Lm2:
for p being FinSequence
for m, n being Element of NAT st 1 <= m & m <= n + 1 & n <= len p holds
( (len (m,n -cut p)) + m = n + 1 & ( for i being Element of NAT st i < len (m,n -cut p) holds
(m,n -cut p) . (i + 1) = p . (m + i) ) )
theorem Th22:
theorem
theorem
theorem Th25:
theorem