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 n' be natural number ; :: thesis: ( n' > 0 implies TrCl R c= )
assume A1: n' > 0 ; :: thesis: TrCl R c=
for c being Element of [:X,X:] holds (n' iter R) . c <= (TrCl R) . c

proof

let c be Element of [:X,X:]; :: thesis: (n' iter R) . c <= (TrCl R) . c
set Q = { (n iter R) where n is Element of NAT : n > 0 } ;
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;
A3: (TrCl R) . [x,y] = "\/" (pi { (n iter R) where n is Element of NAT : n > 0 } ,[x,y]),(RealPoset [.0 ,1.]) by Th29;
reconsider n' = n' as Element of NAT by ORDINAL1:def 13;
n' iter R in { (n iter R) where n is Element of NAT : n > 0 } by A1;
then (n' iter R) . [x,y] in pi { (n iter R) where n is Element of NAT : n > 0 } ,[x,y] by CARD_3:def 6;
then (n' iter R) . [x,y] <<= (TrCl R) . [x,y] by A3, YELLOW_2:24;
hence (n' 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