theorem Th40: :: GLIB_015:40

for F1, F2, F3 being Graph-yielding Function st F1,F2 are_Disomorphic & F2,F3 are_Disomorphic holds
F1,F3 are_Disomorphic