set G = the _Graph;
set f = canGFDistinction (X --> the _Graph);
A1: dom (canGFDistinction (X --> the _Graph)) = dom (X --> the _Graph) by Def25
.= X ;
then reconsider f = canGFDistinction (X --> the _Graph) as X -defined Function by RELAT_1:def 18;
reconsider f = f as Graph-yielding ManySortedSet of X by A1, PARTFUN1:def 2;
take f ; :: thesis: ( not f is empty & f is vertex-disjoint & f is edge-disjoint )
thus ( not f is empty & f is vertex-disjoint & f is edge-disjoint ) ; :: thesis: verum