let C be non empty set ; :: thesis: for f, h, g being Membership_Func of C holds min ((min ((max (f,g)),(max (g,h)))),(max (h,f))) = max ((max ((min (f,g)),(min (g,h)))),(min (h,f)))
let f, h, g be Membership_Func of C; :: thesis: min ((min ((max (f,g)),(max (g,h)))),(max (h,f))) = max ((max ((min (f,g)),(min (g,h)))),(min (h,f)))
thus min ((min ((max (f,g)),(max (g,h)))),(max (h,f))) = max ((min ((min ((max (f,g)),(max (g,h)))),h)),(min ((min ((max (f,g)),(max (g,h)))),f))) by Th9
.= max ((min ((max (f,g)),(min ((max (g,h)),h)))),(min ((min ((max (f,g)),(max (g,h)))),f))) by Th7
.= max ((min ((max (f,g)),(min ((max (h,g)),h)))),(min ((min ((max (f,g)),f)),(max (g,h))))) by Th7
.= max ((min ((max (f,g)),h)),(min ((min ((max (f,g)),f)),(max (g,h))))) by Th8
.= max ((min ((max (f,g)),h)),(min (f,(max (g,h))))) by Th8
.= max ((min (h,(max (f,g)))),(max ((min (f,g)),(min (f,h))))) by Th9
.= max ((max ((min (f,g)),(min (f,h)))),(max ((min (h,f)),(min (h,g))))) by Th9
.= max ((max ((max ((min (f,g)),(min (f,h)))),(min (f,h)))),(min (h,g))) by Th7
.= max ((max ((min (f,g)),(max ((min (f,h)),(min (f,h)))))),(min (h,g))) by Th7
.= max ((max ((min (f,g)),(min (g,h)))),(min (h,f))) by Th7 ; :: thesis: verum