:: deftheorem defines Foax MODELC_1:def 71 :
for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for f, g, h being Assign of (BASSModel (R,BASSIGN)) holds Foax (g,f,h) = g 'or' (Fax (f,h));