theorem Th2: :: MSSCYC_1:3

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