let C1, C2 be non empty set ; :: thesis: for x being Element of [:C1,C2:]
for h being RMembership_Func of C1,C2 holds
( (Zmf C1,C2) . x <= h . x & h . x <= (Umf C1,C2) . x )
A1: Umf C1,C2 = UMF [:C1,C2:] ;
Zmf C1,C2 = EMF [:C1,C2:] ;
hence for x being Element of [:C1,C2:]
for h being RMembership_Func of C1,C2 holds
( (Zmf C1,C2) . x <= h . x & h . x <= (Umf C1,C2) . x ) by A1, FUZZY_1:17; :: thesis: verum