theorem :: GLIB_015:43

for F1, F2 being empty Graph-yielding Function holds
( F1,F2 are_Disomorphic & F1,F2 are_isomorphic ) ;