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:
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 ;
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])),()) by Th29;
then (n9 iter R) . [x,y] <<= (TrCl R) . [x,y] by ;
hence (n9 iter R) . c <= (TrCl R) . c by ; :: thesis: verum
end;
hence TrCl R c= ; :: thesis: verum