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:])

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

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

then reconsider Q = { (n iter R) where n is Element of NAT : n > 0 } as Subset of (FuzzyLattice [:X,X:]) ;
let t be object ; :: 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;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

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