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= ;
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,y9)) "/\" (R . (y9,z))) where y9 is Element of X : verum } ;
then (R . (x,y)) "/\" (R . (y,z)) <<= "\/" ( { ((R . (x,y9)) "/\" (R . (y9,z))) where y9 is Element of X : verum } ,(RealPoset [.0,1.])) by YELLOW_2:22;
then (R . (x,y)) "/\" (R . (y,z)) <<= (R (#) R) . (x,z) by LFUZZY_0:22;
then A2: (R . (x,y)) "/\" (R . (y,z)) <= (R (#) R) . (x,z) by LFUZZY_0:3;
(R (#) R) . (x,z) <= R . (x,z) by A1;
then (R . [x,y]) "/\" (R . [y,z]) <= R . [x,z] by A2, XXREAL_0:2;
hence (R . [x,y]) "/\" (R . [y,z]) <<= R . [x,z] by LFUZZY_0:3; :: thesis: verum

end;

end;

assume A3: 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 st r in rng (min (R,R,x,z)) holds
r <= R . [x,z]

proof

let r be Real; :: 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,y9]) "/\" (R . [y9,z])) where y9 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 A3;
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 SEQ_4:144;
hence (R (#) R) . (x,z) <= R . (x,z) by FUZZY_4:def 3; :: thesis: verum

end;

end;