for X being non empty set
for f being PartFunc of X,REAL
for a being Real
for x being set holds
( x in less_eq_dom (f,a) iff ( x in dom f & ex y being Real st
( y = f . x & y <= a ) ) )