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