let X be non empty set ; :: thesis: for r being Relation of X st r is transitive holds
chi r,[:X,X:] is transitive
let r be Relation of X; :: thesis: ( r is transitive implies chi r,[:X,X:] is transitive )
assume r is transitive ; :: thesis: chi r,[:X,X:] is transitive
then A1: r is_transitive_in field r by RELAT_2:def 16;
let x, y, z be Element of X; :: according to LFUZZY_1:def 7 :: thesis: ((chi r,[:X,X:]) . [x,y]) "/\" ((chi r,[:X,X:]) . [y,z]) <<= (chi r,[:X,X:]) . [x,z]
A2: ( x in field r & y in field r & z in field r & [x,y] in r & [y,z] in r implies [x,z] in r ) by A1, RELAT_2:def 8;

per cases ( [x,y] in r or not [x,y] in r ) ;

suppose A3: [x,y] in r ; :: thesis: ((chi r,[:X,X:]) . [x,y]) "/\" ((chi r,[:X,X:]) . [y,z]) <<= (chi r,[:X,X:]) . [x,z]

thus ((chi r,[:X,X:]) . [x,y]) "/\" ((chi r,[:X,X:]) . [y,z]) <<= (chi r,[:X,X:]) . [x,z] :: thesis: verum

proof

per cases ( [y,z] in r or not [y,z] in r ) ;

suppose A4: [y,z] in r ; :: thesis: ((chi r,[:X,X:]) . [x,y]) "/\" ((chi r,[:X,X:]) . [y,z]) <<= (chi r,[:X,X:]) . [x,z]

((chi r,[:X,X:]) . [x,y]) "/\" ((chi r,[:X,X:]) . [y,z]) = min 1,((chi r,[:X,X:]) . [y,z]) by A3, FUNCT_3:def 3
.= min 1,1 by A4, FUNCT_3:def 3
.= (chi r,[:X,X:]) . [x,z] by A2, A3, A4, FUNCT_3:def 3, RELAT_1:30 ;
hence ((chi r,[:X,X:]) . [x,y]) "/\" ((chi r,[:X,X:]) . [y,z]) <<= (chi r,[:X,X:]) . [x,z] by LFUZZY_0:3; :: thesis: verum

end;

suppose A5: not [y,z] in r ; :: thesis: ((chi r,[:X,X:]) . [x,y]) "/\" ((chi r,[:X,X:]) . [y,z]) <<= (chi r,[:X,X:]) . [x,z]

((chi r,[:X,X:]) . [x,y]) "/\" ((chi r,[:X,X:]) . [y,z]) = min 1,((chi r,[:X,X:]) . [y,z]) by A3, FUNCT_3:def 3
.= min 1,0 by A5, FUNCT_3:def 3
.= 0 by XXREAL_0:def 9 ;
then ((chi r,[:X,X:]) . [x,y]) "/\" ((chi r,[:X,X:]) . [y,z]) <= (chi r,[:X,X:]) . [x,z] by FUZZY_2:1;
hence ((chi r,[:X,X:]) . [x,y]) "/\" ((chi r,[:X,X:]) . [y,z]) <<= (chi r,[:X,X:]) . [x,z] by LFUZZY_0:3; :: thesis: verum

end;

end;

end;

end;

suppose A6: not [x,y] in r ; :: thesis: ((chi r,[:X,X:]) . [x,y]) "/\" ((chi r,[:X,X:]) . [y,z]) <<= (chi r,[:X,X:]) . [x,z]

thus ((chi r,[:X,X:]) . [x,y]) "/\" ((chi r,[:X,X:]) . [y,z]) <<= (chi r,[:X,X:]) . [x,z] :: thesis: verum

proof

per cases ( [y,z] in r or not [y,z] in r ) ;

suppose A7: [y,z] in r ; :: thesis: ((chi r,[:X,X:]) . [x,y]) "/\" ((chi r,[:X,X:]) . [y,z]) <<= (chi r,[:X,X:]) . [x,z]

((chi r,[:X,X:]) . [x,y]) "/\" ((chi r,[:X,X:]) . [y,z]) = min 0 ,((chi r,[:X,X:]) . [y,z]) by A6, FUNCT_3:def 3
.= min 0 ,1 by A7, FUNCT_3:def 3
.= 0 by XXREAL_0:def 9 ;
then ((chi r,[:X,X:]) . [x,y]) "/\" ((chi r,[:X,X:]) . [y,z]) <= (chi r,[:X,X:]) . [x,z] by FUZZY_2:1;
hence ((chi r,[:X,X:]) . [x,y]) "/\" ((chi r,[:X,X:]) . [y,z]) <<= (chi r,[:X,X:]) . [x,z] by LFUZZY_0:3; :: thesis: verum

end;

suppose A8: not [y,z] in r ; :: thesis: ((chi r,[:X,X:]) . [x,y]) "/\" ((chi r,[:X,X:]) . [y,z]) <<= (chi r,[:X,X:]) . [x,z]

((chi r,[:X,X:]) . [x,y]) "/\" ((chi r,[:X,X:]) . [y,z]) = min 0 ,((chi r,[:X,X:]) . [y,z]) by A6, FUNCT_3:def 3
.= min 0 ,0 by A8, FUNCT_3:def 3
.= 0 ;
then ((chi r,[:X,X:]) . [x,y]) "/\" ((chi r,[:X,X:]) . [y,z]) <= (chi r,[:X,X:]) . [x,z] by FUZZY_2:1;
hence ((chi r,[:X,X:]) . [x,y]) "/\" ((chi r,[:X,X:]) . [y,z]) <<= (chi r,[:X,X:]) . [x,z] by LFUZZY_0:3; :: thesis: verum

end;

end;

end;

end;

end;