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