defpred S₁[ set , set ] means $2 is PRIM:Labeling of G;

A1: now

let i be set ; :: thesis: ( i in NAT implies ex r being set st S₁[i,r] )
assume i in NAT ; :: thesis: ex r being set st S₁[i,r]
take r = [{},{}]; :: thesis: S₁[i,r]
( {} c= the_Vertices_of G & {} c= the_Edges_of G ) by XBOOLE_1:2;
hence S₁[i,r] by ZFMISC_1:def 2; :: thesis: verum

end;

consider s being ManySortedSet of NAT such that
A2: for i being set st i in NAT holds
S₁[i,s . i] from PBOOLE:sch 3(A1);
take s ; :: thesis: for n being Nat holds s . n is PRIM:Labeling of G
let i be Nat; :: thesis: s . i is PRIM:Labeling of G
i in NAT by ORDINAL1:def 12;
hence s . i is PRIM:Labeling of G by A2; :: thesis: verum