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