let C be non empty set ; :: thesis: for x being Element of C
for h being Membership_Func of C holds
( 0 <= h . x & h . x <= 1 )
let x be Element of C; :: thesis: for h being Membership_Func of C holds
( 0 <= h . x & h . x <= 1 )
let h be Membership_Func of C; :: thesis: ( 0 <= h . x & h . x <= 1 )
(EMF C) . x = 0 by FUNCT_3:def 3;
hence 0 <= h . x by FUZZY_1:16; :: thesis: h . x <= 1
(UMF C) . x = 1 by FUNCT_3:def 3;
hence h . x <= 1 by FUZZY_1:16; :: thesis: verum