let C1, C2 be non empty set ; :: thesis: for f, g being RMembership_Func of C1,C2 holds converse (f \+\ g) = (converse f) \+\ (converse g)
let f, g be RMembership_Func of C1,C2; :: thesis: converse (f \+\ g) = (converse f) \+\ (converse g)
converse (f \+\ g) = max ((converse (min (f,(1_minus g)))),(converse (min ((1_minus f),g)))) by Th7
.= max ((min ((converse f),(converse (1_minus g)))),(converse (min ((1_minus f),g)))) by Th8
.= max ((min ((converse f),(converse (1_minus g)))),(min ((converse (1_minus f)),(converse g)))) by Th8
.= max ((min ((converse f),(1_minus (converse g)))),(min ((converse (1_minus f)),(converse g)))) by Th6
.= max ((min ((converse f),(1_minus (converse g)))),(min ((1_minus (converse f)),(converse g)))) by Th6 ;
hence converse (f \+\ g) = (converse f) \+\ (converse g) ; :: thesis: verum