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 3;
then A3: (min ((R (#) S),(S (#) S))) . [x,y] <= (S (#) S) . [x,y] by XXREAL_0:17;
S c= by A2;
then (S (#) S) . (x,y) <= S . (x,y) ;
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 3;
then A5: (min ((R (#) R),(S (#) R))) . [x,y] <= (R (#) R) . [x,y] by XXREAL_0:17;
R c= by A1;
then (R (#) R) . (x,y) <= R . (x,y) ;
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] ;
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] ;
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;
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 3; :: thesis: verum