let X be non empty set ; :: thesis: for R, R9 being RMembership_Func of X,X st R9 is symmetric & R9 c= holds

R9 c=

let R, T be RMembership_Func of X,X; :: thesis: ( T is symmetric & T c= implies T c= )

assume that

A1: T is symmetric and

A2: T c= ; :: thesis: T c=

let x, y be Element of X; :: according to LFUZZY_1:def 1 :: thesis: (max (R,(converse R))) . (x,y) <= T . (x,y)

R . [y,x] <= T . [y,x] by A2;

then R . (y,x) <= T . (y,x) ;

then A3: R . (y,x) <= T . (x,y) by A1;

R . [x,y] <= T . [x,y] by A2;

then max ((R . (x,y)),(R . (y,x))) <= T . (x,y) by A3, XXREAL_0:28;

then max ((R . (x,y)),((converse R) . (x,y))) <= T . (x,y) by FUZZY_4:26;

then max ((R . [x,y]),((converse R) . [x,y])) <= T . [x,y] ;

hence (max (R,(converse R))) . (x,y) <= T . (x,y) by FUZZY_1:def 4; :: thesis: verum

R9 c=

let R, T be RMembership_Func of X,X; :: thesis: ( T is symmetric & T c= implies T c= )

assume that

A1: T is symmetric and

A2: T c= ; :: thesis: T c=

let x, y be Element of X; :: according to LFUZZY_1:def 1 :: thesis: (max (R,(converse R))) . (x,y) <= T . (x,y)

R . [y,x] <= T . [y,x] by A2;

then R . (y,x) <= T . (y,x) ;

then A3: R . (y,x) <= T . (x,y) by A1;

R . [x,y] <= T . [x,y] by A2;

then max ((R . (x,y)),(R . (y,x))) <= T . (x,y) by A3, XXREAL_0:28;

then max ((R . (x,y)),((converse R) . (x,y))) <= T . (x,y) by FUZZY_4:26;

then max ((R . [x,y]),((converse R) . [x,y])) <= T . [x,y] ;

hence (max (R,(converse R))) . (x,y) <= T . (x,y) by FUZZY_1:def 4; :: thesis: verum