for G being Graph holds (rng the Source of G) \/ (rng the Target of G) c= the carrier of G