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:9
.= min ((max (f,g)),h) by A1, FUZZY_1:22 ; :: thesis: verum