:: deftheorem Def55 defines F_LABEL MODELC_1:def 55 :
for S being non empty set
for X being non empty Subset of (ModelSP S)
for s being object
for b₄ being Subset of X holds
( b₄ = F_LABEL (s,X) iff for x being object holds
( x in b₄ iff ( x in X & ex f being Function of S,BOOLEAN st
( f = x & f . s = TRUE ) ) ) );