:: deftheorem Def56 defines Label_ MODELC_1:def 56 :
for S being non empty set
for X being non empty Subset of (ModelSP S)
for b₃ being Function of S,(bool X) holds
( b₃ = Label_ X iff for x being object st x in S holds
b₃ . x = F_LABEL (x,X) );