theorem Th17: :: GRAPH_2:17

for p, q being FinSequence holds rng (p ^' q) c= (rng p) \/ (rng q)