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) = min ((converse f),(converse (1_minus g))) by Th8
.= min ((converse f),(1_minus (converse g))) by Th6 ;
hence converse (f \ g) = (converse f) \ (converse g) ; :: thesis: verum