let X be non empty set ; :: thesis: for R being RMembership_Func of X,X holds min (R,(converse R)) is symmetric
let R be RMembership_Func of X,X; :: thesis: min (R,(converse R)) is symmetric
set S = min (R,(converse R));
let x, y be Element of X; :: according to LFUZZY_1:def 5 :: thesis: (min (R,(converse R))) . (x,y) = (min (R,(converse R))) . (y,x)
thus (min (R,(converse R))) . (x,y) = (min (R,(converse R))) . [x,y]
.= min ((R . (x,y)),((converse R) . (x,y))) by FUZZY_1:def 3
.= min ((R . (x,y)),(R . (y,x))) by FUZZY_4:26
.= min (((converse R) . (y,x)),(R . (y,x))) by FUZZY_4:26
.= (min (R,(converse R))) . [y,x] by FUZZY_1:def 3
.= (min (R,(converse R))) . (y,x) ; :: thesis: verum