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 that
A1: x in C1 and
A2: y in C2 and
A3: f . [x,y] <= g . [x,y] ; :: thesis: (converse f) . [y,x] <= (converse g) . [y,x]
A4: [y,x] in [:C2,C1:] by A1, A2, ZFMISC_1:87;
then A5: g . (x,y) = (converse g) . (y,x) by Def1;
f . (x,y) = (converse f) . (y,x) by A4, Def1;
hence (converse f) . [y,x] <= (converse g) . [y,x] by A3, A5; :: thesis: verum