for V being set
for C being finite set
for a being Element of PFuncs (V,C)
for u, v being Element of SubstitutionSet (V,C) st ( for c being set st c in u holds
ex b being set st
( b in v & b c= c \/ a ) ) holds
ex b being set st
( b in u =>> v & b c= a )