for C being non empty set
for x being Element of C
for h being Membership_Func of C holds
( (EMF C) . x <= h . x & h . x <= (UMF C) . x ) by Th13, Th14, Def2;