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])),())

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])),())
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 ()
proof
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 () )
assume t in { (n iter R) where n is Element of NAT : n > 0 } ; :: thesis: t in the carrier of ()
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 () ;
then reconsider t = t as Element of () by LFUZZY_0:def 6;
t in the carrier of () ;
hence t in the carrier of () ; :: thesis: verum
end;
then reconsider Q = { (n iter R) where n is Element of NAT : n > 0 } as Subset of () ;
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])),())
reconsider i = [x,z] as Element of [:X,X:] ;
A1: for a being Element of [:X,X:] holds ([:X,X:] --> ()) . a is complete LATTICE by FUNCOP_1:7;
FuzzyLattice [:X,X:] = () |^ [:X,X:] by LFUZZY_0:def 4
.= product ([:X,X:] --> ()) by YELLOW_1:def 5 ;
then (sup Q) . i = "\/" ((pi (Q,i)),(([:X,X:] --> ()) . i)) by ;
hence (TrCl R) . [x,z] = "\/" ((pi ( { (n iter R) where n is Element of NAT : n > 0 } ,[x,z])),()) by FUNCOP_1:7; :: thesis: verum