let C be non empty set ; :: thesis: for f, g, h 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, g, h 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 Th10
.= max (min (max f,g),(min (max g,h),h)),(min (min (max f,g),(max g,h)),f) by Th8
.= max (min (max f,g),(min (max h,g),h)),(min (min (max f,g),f),(max g,h)) by Th8
.= max (min (max f,g),h),(min (min (max f,g),f),(max g,h)) by Th9
.= max (min (max f,g),h),(min f,(max g,h)) by Th9
.= max (min h,(max f,g)),(max (min f,g),(min f,h)) by Th10
.= max (max (min f,g),(min f,h)),(max (min h,f),(min h,g)) by Th10
.= max (max (max (min f,g),(min f,h)),(min f,h)),(min h,g) by Th8
.= max (max (min f,g),(max (min f,h),(min f,h))),(min h,g) by Th8
.= max (max (min f,g),(min g,h)),(min h,f) by Th8 ; :: thesis: verum