let X be non empty set ; 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; ( T is symmetric & T c= implies T c= )
assume that
A1:
T is symmetric
and
A2:
T c=
; T c=
let x, y be Element of X; LFUZZY_1:def 1 (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; verum