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

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