let X be non empty set ; :: thesis: for R being RMembership_Func of X,X
for n being Nat st n > 0 holds
TrCl R c=
let R be RMembership_Func of X,X; :: thesis: for n being Nat st n > 0 holds
TrCl R c=
let n9 be Nat; :: thesis: ( n9 > 0 implies TrCl R c= )
assume A1: n9 > 0 ; :: thesis: TrCl R c=
for c being Element of [:X,X:] holds (n9 iter R) . c <= (TrCl R) . c

proof

reconsider n9 = n9 as Element of NAT by ORDINAL1:def 12;
set Q = { (n iter R) where n is Element of NAT : n > 0 } ;
let c be Element of [:X,X:]; :: thesis: (n9 iter R) . c <= (TrCl R) . c
consider x, y being object such that
A2: [x,y] = c by RELAT_1:def 1;
reconsider x = x, y = y as Element of X by A2, ZFMISC_1:87;
n9 iter R in { (n iter R) where n is Element of NAT : n > 0 } by A1;
then A3: (n9 iter R) . [x,y] in pi ( { (n iter R) where n is Element of NAT : n > 0 } ,[x,y]) by CARD_3:def 6;
(TrCl R) . [x,y] = "\/" ((pi ( { (n iter R) where n is Element of NAT : n > 0 } ,[x,y])),(RealPoset [.0,1.])) by Th29;
then (n9 iter R) . [x,y] <<= (TrCl R) . [x,y] by A3, YELLOW_2:22;
hence (n9 iter R) . c <= (TrCl R) . c by A2, LFUZZY_0:3; :: thesis: verum

end;

hence TrCl R c= ; :: thesis: verum