theorem Th46: :: MODELC_1:46

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 being Assign of (BASSModel (R,BASSIGN))
for s being Element of S holds
( s |= f EU g iff s |= Foax (g,f,(f EU g)) )