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

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