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