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:16; :: thesis: verum