let C1, C2 be non empty set ; 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; 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)
; verum