defpred S1[ object , object ] means $2 is PRIM:Labeling of G;
A1: now :: thesis: for i being object st i in NAT holds
ex r being object st S1[i,r]
let i be object ; :: thesis: ( i in NAT implies ex r being object st S1[i,r] )
assume i in NAT ; :: thesis: ex r being object st S1[i,r]
reconsider r = [{},{}] as object ;
take r = r; :: thesis: S1[i,r]
( {} c= the_Vertices_of G & {} c= the_Edges_of G ) ;
hence S1[i,r] by ZFMISC_1:def 2; :: thesis: verum
end;
consider s being ManySortedSet of NAT such that
A2: for i being object st i in NAT holds
S1[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