let X be non empty set ; :: thesis: for R, R9 being RMembership_Func of X,X st R9 is symmetric & R c= holds
min (R,(converse R)) c=
let R, T be RMembership_Func of X,X; :: thesis: ( T is symmetric & R c= implies min (R,(converse R)) c= )
assume that
A1: T is symmetric and
A2: R c= ; :: thesis: min (R,(converse R)) c=
let x, y be Element of X; :: according to LFUZZY_1:def 1 :: thesis: T . (x,y) <= (min (R,(converse R))) . (x,y)
T . [y,x] <= R . [y,x] by A2;
then T . (y,x) <= R . (y,x) ;
then A3: T . (x,y) <= R . (y,x) by A1;
T . [x,y] <= R . [x,y] by A2;
then T . (x,y) <= min ((R . (x,y)),(R . (y,x))) by A3, XXREAL_0:20;
then T . (x,y) <= min ((R . (x,y)),((converse R) . (x,y))) by FUZZY_4:26;
then T . [x,y] <= min ((R . [x,y]),((converse R) . [x,y])) ;
hence T . (x,y) <= (min (R,(converse R))) . (x,y) by FUZZY_1:def 3; :: thesis: verum