let C1, C2 be non empty set ; :: thesis: for f, g being RMembership_Func of C1,C2
for x, y being set st x in C1 & y in C2 & f . [x,y] <= g . [x,y] holds
(converse f) . [y,x] <= (converse g) . [y,x]
let f, g be RMembership_Func of C1,C2; :: thesis: for x, y being set st x in C1 & y in C2 & f . [x,y] <= g . [x,y] holds
(converse f) . [y,x] <= (converse g) . [y,x]
let x, y be set ; :: thesis: ( x in C1 & y in C2 & f . [x,y] <= g . [x,y] implies (converse f) . [y,x] <= (converse g) . [y,x] )
assume A1: ( x in C1 & y in C2 & f . [x,y] <= g . [x,y] ) ; :: thesis: (converse f) . [y,x] <= (converse g) . [y,x]
then [y,x] in [:C2,C1:] by ZFMISC_1:106;
then ( f . x,y = (converse f) . y,x & g . x,y = (converse g) . y,x ) by Def1;
hence (converse f) . [y,x] <= (converse g) . [y,x] by A1; :: thesis: verum