let C be non empty set ; :: thesis: for f, g being Membership_Func of C holds f \ (min (f,g)) c=

let f, g be Membership_Func of C; :: thesis: f \ (min (f,g)) c=

f \ (min (f,g)) = min (f,(max ((1_minus f),(1_minus g)))) by FUZZY_1:11

.= max ((min (f,(1_minus f))),(f \ g)) by FUZZY_1:9 ;

hence f \ (min (f,g)) c= by FUZZY_1:17; :: thesis: verum

let f, g be Membership_Func of C; :: thesis: f \ (min (f,g)) c=

f \ (min (f,g)) = min (f,(max ((1_minus f),(1_minus g)))) by FUZZY_1:11

.= max ((min (f,(1_minus f))),(f \ g)) by FUZZY_1:9 ;

hence f \ (min (f,g)) c= by FUZZY_1:17; :: thesis: verum