begin
Lm1:
for G being Graph holds {} is Chain of G
Lm2:
for n being Element of NAT
for G being Graph
for p being Chain of G holds p | (Seg n) is Chain of G
Lm3:
for G being Graph
for H1, H2 being strict Subgraph of G st the carrier of H1 = the carrier of H2 & the carrier' of H1 = the carrier' of H2 holds
H1 = H2
Lm4:
for G being Graph
for H being Subgraph of G holds
( the Source of H in PFuncs ( the carrier' of G, the carrier of G) & the Target of H in PFuncs ( the carrier' of G, the carrier of G) )
theorem Th17:
for
G1,
G2,
G3 being
Graph st
G1 c= G2 &
G2 c= G3 holds
G1 c= G3
theorem Th22:
for
G1,
G,
G2 being
Graph st
G1 c= G &
G2 c= G holds
G1 \/ G2 c= G