let S be Graph-membered set ; :: thesis: ex f being one-to-one Function st
( dom f = S & rng f = S & ( for G being _Graph st G in S holds
f . G is b₂ -isomorphic _Graph ) )
take id S ; :: thesis: ( dom (id S) = S & rng (id S) = S & ( for G being _Graph st G in S holds
(id S) . G is b₁ -isomorphic _Graph ) )
thus ( dom (id S) = S & rng (id S) = S ) ; :: thesis: for G being _Graph st G in S holds
(id S) . G is b₁ -isomorphic _Graph
let G be _Graph; :: thesis: ( G in S implies (id S) . G is G -isomorphic _Graph )
assume G in S ; :: thesis: (id S) . G is G -isomorphic _Graph
then (id S) . G = G by FUNCT_1:18;
hence (id S) . G is G -isomorphic _Graph by GLIB_010:53; :: thesis: verum