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: K73([:C2,C1:],REAL,(converse f),c) <= K73([:C2,C1:],REAL,(converse g),c)
ex y, x being object 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;
hence K73([:C2,C1:],REAL,(converse f),c) <= K73([:C2,C1:],REAL,(converse g),c) by A2, A3, A4, Th9; :: thesis: verum