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, FUZZY_1:def 3;
then T . y,x <= R . y,x ;
then A3: T . x,y <= R . y,x by A1, Def5;
T . [x,y] <= R . [x,y] by A2, FUZZY_1:def 3;
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 4; :: thesis: verum