let X be non empty set ; :: thesis: for R being RMembership_Func of X,X holds TrCl R c=
let R be RMembership_Func of X,X; :: thesis: TrCl R c=
for c being Element of [:X,X:] holds R . c <= (TrCl R) . c

proof

set Q = { (n iter R) where n is Element of NAT : n > 0 } ;
let c be Element of [:X,X:]; :: thesis: R . c <= (TrCl R) . c
consider x, y being object such that
A1: [x,y] = c by RELAT_1:def 1;
reconsider x = x, y = y as Element of X by A1, ZFMISC_1:87;
R = 1 iter R by Th25;
then R in { (n iter R) where n is Element of NAT : n > 0 } ;
then A2: 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 R . [x,y] <<= (TrCl R) . [x,y] by A2, YELLOW_2:22;
hence R . c <= (TrCl R) . c by A1, LFUZZY_0:3; :: thesis: verum

end;

hence TrCl R c= ; :: thesis: verum