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

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