set FL = FuzzyLattice [:X,X:];
set RP = RealPoset [.0 ,1.];
set A = { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } ;
for c being Element of [:X,X:] holds ((TrCl R) (#) (TrCl R)) . c <= (TrCl R) . c

proof

let c be Element of [:X,X:]; :: thesis: ((TrCl R) (#) (TrCl R)) . c <= (TrCl R) . c
A1: { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } c= the carrier of (FuzzyLattice [:X,X:])

proof

let t be set ; :: according to TARSKI:def 3 :: thesis: ( not t in { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } or t in the carrier of (FuzzyLattice [:X,X:]) )
assume t in { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } ; :: thesis: t in the carrier of (FuzzyLattice [:X,X:])
then consider i, j being Element of NAT such that
A2: ( t = (i iter R) (#) (j iter R) & i > 0 & j > 0 ) ;
[:X,X:],((i iter R) (#) (j iter R)) @ = (i iter R) (#) (j iter R) by LFUZZY_0:def 6;
hence t in the carrier of (FuzzyLattice [:X,X:]) by A2; :: thesis: verum

end;

A3: ((TrCl R) (#) (TrCl R)) . c = ("\/" { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } ,(FuzzyLattice [:X,X:])) . c by Th36
.= "\/" (pi { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } ,c),(RealPoset [.0 ,1.]) by A1, Th32 ;
(TrCl R) . c is_>=_than pi { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } ,c

proof

for b being Element of (RealPoset [.0 ,1.]) st b in pi { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } ,c holds
b <<= (TrCl R) . c

proof

let b be Element of (RealPoset [.0 ,1.]); :: thesis: ( b in pi { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } ,c implies b <<= (TrCl R) . c )
assume b in pi { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } ,c ; :: thesis: b <<= (TrCl R) . c
then consider f being Function such that
A4: ( f in { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } & b = f . c ) by CARD_3:def 6;
consider i, j being Element of NAT such that
A5: ( f = (i iter R) (#) (j iter R) & i > 0 & j > 0 ) by A4;
A6: i + j > 0 by A5;
A7: f = (i + j) iter R by A5, Th27;
reconsider f = f as RMembership_Func of X,X by A5;
TrCl R c= by A6, A7, Th31;
then f . c <= (TrCl R) . c by FUZZY_1:def 3;
hence b <<= (TrCl R) . c by A4, LFUZZY_0:3; :: thesis: verum

end;

hence (TrCl R) . c is_>=_than pi { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } ,c by LATTICE3:def 9; :: thesis: verum

end;

then "\/" (pi { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } ,c),(RealPoset [.0 ,1.]) <<= (TrCl R) . c by YELLOW_0:32;
hence ((TrCl R) (#) (TrCl R)) . c <= (TrCl R) . c by A3, LFUZZY_0:3; :: thesis: verum

end;

then TrCl R c= by FUZZY_1:def 3;
hence TrCl R is transitive by Def6; :: thesis: verum