thus ( R is transitive iff for x, y, z being Element of X holds (R . [x,y]) "/\" (R . [y,z]) <<= R . [x,z] ) :: thesis: verum

proof

hereby :: thesis: ( ( for x, y, z being Element of X holds (R . [x,y]) "/\" (R . [y,z]) <<= R . [x,z] ) implies R is transitive )

assume R is transitive ; :: thesis: for x, y, z being Element of X holds (R . [x,y]) "/\" (R . [y,z]) <<= R . [x,z]
then A1: R c= by Def6;
thus for x, y, z being Element of X holds (R . [x,y]) "/\" (R . [y,z]) <<= R . [x,z] :: thesis: verum

proof

let x, y, z be Element of X; :: thesis: (R . [x,y]) "/\" (R . [y,z]) <<= R . [x,z]
(R . x,y) "/\" (R . y,z) in { ((R . x,y') "/\" (R . y',z)) where y' is Element of X : verum } ;
then (R . x,y) "/\" (R . y,z) <<= "\/" { ((R . x,y') "/\" (R . y',z)) where y' is Element of X : verum } ,(RealPoset [.0 ,1.]) by YELLOW_2:24;
then (R . x,y) "/\" (R . y,z) <<= (R (#) R) . x,z by LFUZZY_0:22;
then ( (R . x,y) "/\" (R . y,z) <= (R (#) R) . x,z & (R (#) R) . x,z <= R . x,z ) by A1, Def1, LFUZZY_0:3;
then (R . [x,y]) "/\" (R . [y,z]) <= R . [x,z] by XXREAL_0:2;
hence (R . [x,y]) "/\" (R . [y,z]) <<= R . [x,z] by LFUZZY_0:3; :: thesis: verum

end;

end;

assume A2: for x, y, z being Element of X holds (R . [x,y]) "/\" (R . [y,z]) <<= R . [x,z] ; :: thesis: R is transitive
thus R c= :: according to LFUZZY_1:def 6 :: thesis: verum

proof

let x, z be Element of X; :: according to LFUZZY_1:def 1 :: thesis: (R (#) R) . x,z <= R . x,z
set W = rng (min R,R,x,z);
for r being real number st r in rng (min R,R,x,z) holds
r <= R . [x,z]

proof

let r be real number ; :: thesis: ( r in rng (min R,R,x,z) implies r <= R . [x,z] )
assume r in rng (min R,R,x,z) ; :: thesis: r <= R . [x,z]
then r in { ((R . [x,y']) "/\" (R . [y',z])) where y' is Element of X : verum } by Lm1;
then consider y being Element of X such that
A4: r = (R . [x,y]) "/\" (R . [y,z]) ;
(R . [x,y]) "/\" (R . [y,z]) <<= R . [x,z] by A2;
hence r <= R . [x,z] by A4, LFUZZY_0:3; :: thesis: verum

end;

then upper_bound (rng (min R,R,x,z)) <= R . [x,z] by TOPMETR3:1;
hence (R (#) R) . x,z <= R . x,z by FUZZY_4:def 3; :: thesis: verum

end;

end;