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 4
.= 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 4
.= (min R,(converse R)) . y,x ; :: thesis: verum