let X be non empty set ; for R being RMembership_Func of X,X
for x, y being Element of X holds (TrCl R) . [x,y] = "\/" ((pi ( { (n iter R) where n is Element of NAT : n > 0 } ,[x,y])),(RealPoset [.0,1.]))
let R be RMembership_Func of X,X; for x, y being Element of X holds (TrCl R) . [x,y] = "\/" ((pi ( { (n iter R) where n is Element of NAT : n > 0 } ,[x,y])),(RealPoset [.0,1.]))
set Q = { (n iter R) where n is Element of NAT : n > 0 } ;
{ (n iter R) where n is Element of NAT : n > 0 } c= the carrier of (FuzzyLattice [:X,X:])
then reconsider Q = { (n iter R) where n is Element of NAT : n > 0 } as Subset of (FuzzyLattice [:X,X:]) ;
let x, z be Element of X; (TrCl R) . [x,z] = "\/" ((pi ( { (n iter R) where n is Element of NAT : n > 0 } ,[x,z])),(RealPoset [.0,1.]))
reconsider i = [x,z] as Element of [:X,X:] ;
A1:
for a being Element of [:X,X:] holds ([:X,X:] --> (RealPoset [.0,1.])) . a is complete LATTICE
by FUNCOP_1:7;
FuzzyLattice [:X,X:] =
(RealPoset [.0,1.]) |^ [:X,X:]
by LFUZZY_0:def 4
.=
product ([:X,X:] --> (RealPoset [.0,1.]))
by YELLOW_1:def 5
;
then
(sup Q) . i = "\/" ((pi (Q,i)),(([:X,X:] --> (RealPoset [.0,1.])) . i))
by A1, WAYBEL_3:32;
hence
(TrCl R) . [x,z] = "\/" ((pi ( { (n iter R) where n is Element of NAT : n > 0 } ,[x,z])),(RealPoset [.0,1.]))
by FUNCOP_1:7; verum