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 ( R is transitive & S is transitive ) ; :: thesis: min R,S c=
then A1: ( R c= & S c= ) by Def6;
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 ((min R,S) (#) R),((min R,S) (#) S) c= by FUZZY_4:15;
then A2: ((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 (#) R),(S (#) R) c= & min (R (#) S),(S (#) S) 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] & ((min R,S) (#) S) . [x,y] <= (min (R (#) S),(S (#) S)) . [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 XXREAL_0:18;
then A3: ((min R,S) (#) (min R,S)) . [x,y] <= min ((min (R (#) R),(S (#) R)) . [x,y]),((min (R (#) S),(S (#) S)) . [x,y]) by A2, XXREAL_0:2;
( (min (R (#) R),(S (#) R)) . [x,y] = min ((R (#) R) . [x,y]),((S (#) R) . [x,y]) & (min (R (#) S),(S (#) S)) . [x,y] = min ((S (#) S) . [x,y]),((R (#) S) . [x,y]) ) by FUZZY_1:def 4;
then ( (min (R (#) R),(S (#) R)) . [x,y] <= (R (#) R) . [x,y] & (min (R (#) S),(S (#) S)) . [x,y] <= (S (#) S) . [x,y] & (R (#) R) . x,y <= R . x,y & (S (#) S) . x,y <= S . x,y ) by A1, Def1, XXREAL_0:17;
then ( (min (R (#) R),(S (#) R)) . [x,y] <= R . [x,y] & (min (R (#) S),(S (#) S)) . [x,y] <= S . [x,y] ) by XXREAL_0:2;
then min ((min (R (#) R),(S (#) R)) . [x,y]),((min (R (#) S),(S (#) S)) . [x,y]) <= min (R . [x,y]),(S . [x,y]) by XXREAL_0:18;
then ((min R,S) (#) (min R,S)) . [x,y] <= min (R . [x,y]),(S . [x,y]) by A3, XXREAL_0:2;
hence ((min R,S) (#) (min R,S)) . x,y <= (min R,S) . x,y by FUZZY_1:def 4; :: thesis: verum