let X be non empty set ; :: thesis: for R being RMembership_Func of X,X
for n being natural number st n > 0 holds
TrCl R c=
let R be RMembership_Func of X,X; :: thesis: for n being natural number st n > 0 holds
TrCl R c=
let n9 be natural number ; :: 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 13;
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 set such that
A2: [x,y] = c by RELAT_1:def 1;
reconsider x = x, y = y as Element of X by A2, ZFMISC_1:106;
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:24;
hence (n9 iter R) . c <= (TrCl R) . c by A2, LFUZZY_0:3; :: thesis: verum

end;

hence TrCl R c= by FUZZY_1:def 3; :: thesis: verum