let X be non empty set ; :: thesis: 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; :: thesis: 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:])

proof

let t be set ; :: according to TARSKI:def 3 :: thesis: ( not t in { (n iter R) where n is Element of NAT : n > 0 } or t in the carrier of (FuzzyLattice [:X,X:]) )
assume t in { (n iter R) where n is Element of NAT : n > 0 } ; :: thesis: t in the carrier of (FuzzyLattice [:X,X:])
then ex n being Element of NAT st
( t = n iter R & n > 0 ) ;
then reconsider t = t as Membership_Func of [:X,X:] ;
[:X,X:],t @ is Element of (FuzzyLattice [:X,X:]) ;
then reconsider t = t as Element of (FuzzyLattice [:X,X:]) by LFUZZY_0:def 6;
t in the carrier of (FuzzyLattice [:X,X:]) ;
hence t in the carrier of (FuzzyLattice [:X,X:]) ; :: thesis: verum

end;

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; :: thesis: (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:13;
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:13; :: thesis: verum