theorem :: GLIBPRE1:39

for G1, G2 being _Graph
for G3 being Component of G1 st G1 == G2 holds
G3 is Component of G2