set Q = { (n iter R) where n is Element of NAT : n > 0 } ;
set RP = RealPoset [.0,1.];
let c be Element of [:X,X:]; :: thesis:
for b being Element of (RealPoset [.0,1.]) st b in pi ( { (n iter R) where n is Element of NAT : n > 0 } ,c) holds
b <<= R . c

let b be Element of (RealPoset [.0,1.]); :: thesis:
assume b in pi ( { (n iter R) where n is Element of NAT : n > 0 } ,c) ; :: thesis:
then consider f being Function such that
A2: f in { (n iter R) where n is Element of NAT : n > 0 } and
A3: b = f . c by CARD_3:def 6;
consider n being Element of NAT such that
A4: f = n iter R and
A5: n > 0 by A2;
R c= by A1, A5, Th37;
then (n iter R) . c <= R . c ;
hence b <<= R . c by A3, A4, LFUZZY_0:3; :: thesis:

end;

then A6: R . c is_>=_than pi ( { (n iter R) where n is Element of NAT : n > 0 } ,c) by LATTICE3:def 9;
{ (n iter R) where n is Element of NAT : n > 0 } c= the carrier of (FuzzyLattice [:X,X:])

let t be object ; :: according to TARSKI:def 3 :: thesis:
assume t in { (n iter R) where n is Element of NAT : n > 0 } ; :: thesis:
then consider i being Element of NAT such that
A7: t = i iter R and
i > 0 ;
([:X,X:],(i iter R)) @ = i iter R by LFUZZY_0:def 6;
hence t in the carrier of (FuzzyLattice [:X,X:]) by A7; :: thesis:

end;

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

end;