theorem Th17: :: MESFUNC1:17

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 /\ (less_dom (f,a)) = A \ (A /\ (great_eq_dom (f,a)))