theorem Th15: :: MESFUNC1:15

for X being set
for f being PartFunc of X,ExtREAL
for A being set
for a being ExtReal st A c= dom f holds
A /\ (great_dom (f,a)) = A \ (A /\ (less_eq_dom (f,a)))