let C be non empty set ; 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; 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
; verum