let C be non empty set ; :: thesis: for f, h, g being Membership_Func of C st h c= holds
max f,(min g,h) = min (max f,g),h
let f, h, g be Membership_Func of C; :: thesis: ( h c= implies max f,(min g,h) = min (max f,g),h )
assume A1: h c= ; :: thesis: max f,(min g,h) = min (max f,g),h
thus max f,(min g,h) = min (max f,g),(max f,h) by FUZZY_1:10
.= min (max f,g),h by A1, FUZZY_1:23 ; :: thesis: verum