let C1, C2 be non empty set ; :: thesis: for f, g being RMembership_Func of C1,C2 st g c= holds
converse g c=
let f, g be RMembership_Func of C1,C2; :: thesis: ( g c= implies converse g c= )
assume A1: g c= ; :: thesis: converse g c=
let c be Element of [:C2,C1:]; :: according to FUZZY_1:def 3 :: thesis: (converse f) . c <= (converse g) . c
ex y, x being set st
( y in C2 & x in C1 & c = [y,x] ) by ZFMISC_1:def 2;
then consider x, y being set such that
A2: ( x in C1 & y in C2 & c = [y,x] ) ;
[x,y] in [:C1,C2:] by A2, ZFMISC_1:106;
then f . [x,y] <= g . [x,y] by A1, FUZZY_1:def 3;
hence (converse f) . c <= (converse g) . c by A2, Th9; :: thesis: verum