thus
( R is transitive iff for x, y, z being Element of X holds (R . [x,y]) "/\" (R . [y,z]) <<= R . [x,z] )
verumproof
hereby ( ( 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
;
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]
verumproof
let x,
y,
z be
Element of
X;
(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;
verum
end;
end;
assume A3:
for
x,
y,
z being
Element of
X holds
(R . [x,y]) "/\" (R . [y,z]) <<= R . [x,z]
;
R is transitive
thus
R c=
LFUZZY_1:def 6 verumproof
let x,
z be
Element of
X;
LFUZZY_1:def 1 (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;
( r in rng (min (R,R,x,z)) implies r <= R . [x,z] )
assume
r in rng (min (R,R,x,z))
;
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;
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;
verum
end;
end;