let S1, S2 be Graph-membered set ; :: thesis: ( S1,S2 are_Disomorphic implies S1,S2 are_isomorphic )
assume S1,S2 are_Disomorphic ; :: thesis: S1,S2 are_isomorphic
then consider f being one-to-one Function such that
A1: ( dom f = S1 & rng f = S2 ) and
A2: for G being _Graph st G in S1 holds
f . G is b₁ -Disomorphic _Graph ;
take f ; :: according to GLIB_015:def 13 :: thesis: ( dom f = S1 & rng f = S2 & ( for G being _Graph st G in S1 holds
f . G is b₁ -isomorphic _Graph ) )
thus ( dom f = S1 & rng f = S2 & ( for G being _Graph st G in S1 holds
f . G is b₁ -isomorphic _Graph ) ) by A1, A2; :: thesis: verum