:: deftheorem defines ModelSP MODELC_1:def 40 :
for S being non empty set holds ModelSP S = Funcs (S,BOOLEAN);