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 A1: r is transitive ; :: thesis: chi (r,[:X,X:]) is transitive
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]
r is_transitive_in field r by A1, RELAT_2:def 16;
then 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 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:15 ;
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;