let X be non empty set ; :: thesis: for R, S being RMembership_Func of X,X st R is transitive & S is transitive holds
min R,S c=
let R, S be RMembership_Func of X,X; :: thesis: ( R is transitive & S is transitive implies min R,S c= )
assume that
A1: R is transitive and
A2: S is transitive ; :: thesis: min R,S c=
let x be Element of X; :: according to LFUZZY_1:def 1 :: thesis: for y being Element of X holds ((min R,S) (#) (min R,S)) . x,y <= (min R,S) . x,y
let y be Element of X; :: thesis: ((min R,S) (#) (min R,S)) . x,y <= (min R,S) . x,y
(min (R (#) S),(S (#) S)) . [x,y] = min ((S (#) S) . [x,y]),((R (#) S) . [x,y]) by FUZZY_1:def 4;
then A3: (min (R (#) S),(S (#) S)) . [x,y] <= (S (#) S) . [x,y] by XXREAL_0:17;
S c= by A2, Def6;
then (S (#) S) . x,y <= S . x,y by Def1;
then A4: (min (R (#) S),(S (#) S)) . [x,y] <= S . [x,y] by A3, XXREAL_0:2;
(min (R (#) R),(S (#) R)) . [x,y] = min ((R (#) R) . [x,y]),((S (#) R) . [x,y]) by FUZZY_1:def 4;
then A5: (min (R (#) R),(S (#) R)) . [x,y] <= (R (#) R) . [x,y] by XXREAL_0:17;
R c= by A1, Def6;
then (R (#) R) . x,y <= R . x,y by Def1;
then (min (R (#) R),(S (#) R)) . [x,y] <= R . [x,y] by A5, XXREAL_0:2;
then A6: min ((min (R (#) R),(S (#) R)) . [x,y]),((min (R (#) S),(S (#) S)) . [x,y]) <= min (R . [x,y]),(S . [x,y]) by A4, XXREAL_0:18;
min ((min R,S) (#) R),((min R,S) (#) S) c= by FUZZY_4:15;
then A7: ((min R,S) (#) (min R,S)) . [x,y] <= (min ((min R,S) (#) R),((min R,S) (#) S)) . [x,y] by FUZZY_1:def 3;
min (R (#) S),(S (#) S) c= by FUZZY_4:16;
then A8: ((min R,S) (#) S) . [x,y] <= (min (R (#) S),(S (#) S)) . [x,y] by FUZZY_1:def 3;
min (R (#) R),(S (#) R) c= by FUZZY_4:16;
then ( (min ((min R,S) (#) R),((min R,S) (#) S)) . [x,y] = min (((min R,S) (#) R) . [x,y]),(((min R,S) (#) S) . [x,y]) & ((min R,S) (#) R) . [x,y] <= (min (R (#) R),(S (#) R)) . [x,y] ) by FUZZY_1:def 3, FUZZY_1:def 4;
then (min ((min R,S) (#) R),((min R,S) (#) S)) . [x,y] <= min ((min (R (#) R),(S (#) R)) . [x,y]),((min (R (#) S),(S (#) S)) . [x,y]) by A8, XXREAL_0:18;
then ((min R,S) (#) (min R,S)) . [x,y] <= min ((min (R (#) R),(S (#) R)) . [x,y]),((min (R (#) S),(S (#) S)) . [x,y]) by A7, XXREAL_0:2;
then ((min R,S) (#) (min R,S)) . [x,y] <= min (R . [x,y]),(S . [x,y]) by A6, XXREAL_0:2;
hence ((min R,S) (#) (min R,S)) . x,y <= (min R,S) . x,y by FUZZY_1:def 4; :: thesis: verum