let X be non empty set ; :: thesis: for R, R' being RMembership_Func of X,X st R' is symmetric & R' c= holds
R' c=
let R, T be RMembership_Func of X,X; :: thesis: ( T is symmetric & T c= implies T c= )
assume A1: ( T is symmetric & 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
A2: ( R . [x,y] <= T . [x,y] & R . [y,x] <= T . [y,x] ) by A1, FUZZY_1:def 3;
then ( R . x,y <= T . x,y & R . y,x <= T . y,x ) ;
then R . y,x <= T . x,y by A1, Def5;
then max (R . x,y),(R . y,x) <= T . x,y by A2, 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 5; :: thesis: verum