let X be non empty set ; for r being Relation of X st r is transitive holds
chi (r,[:X,X:]) is transitive
let r be Relation of X; ( r is transitive implies chi (r,[:X,X:]) is transitive )
assume A1:
r is transitive
; chi (r,[:X,X:]) is transitive
let x, y, z be Element of X; LFUZZY_1:def 7 ((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
;
((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]
verumproof
per cases
( [y,z] in r or not [y,z] in r )
;
suppose A4:
[y,z] in r
;
((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;
verum end; suppose A5:
not
[y,z] in r
;
((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;
verum end;
end; end; suppose A6:
not
[x,y] in r
;
((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]
verumproof
per cases
( [y,z] in r or not [y,z] in r )
;
suppose A7:
[y,z] in r
;
((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;
verum end; suppose A8:
not
[y,z] in r
;
((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;
verum end;
end; end;