for A being finite Approximation_Space
for X, Y being Subset of A
for x being Element of A st X c= Y holds
(MemberFunc (X,A)) . x <= (MemberFunc (Y,A)) . x