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

proof

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: (TrCl R) . c <= R . c
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

proof

let b be Element of (RealPoset [.0,1.]); :: thesis: ( b in pi ( { (n iter R) where n is Element of NAT : n > 0 } ,c) implies b <<= R . c )
assume b in pi ( { (n iter R) where n is Element of NAT : n > 0 } ,c) ; :: thesis: b <<= R . c
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: verum

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:])

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in { (n iter R) where n is Element of NAT : n > 0 } or t in the carrier of (FuzzyLattice [:X,X:]) )
assume t in { (n iter R) where n is Element of NAT : n > 0 } ; :: thesis: t in the carrier of (FuzzyLattice [:X,X:])
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: verum

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: verum

end;

then A8: R c= ;
TrCl R c= by Th30;
hence R = TrCl R by A8, Th3; :: thesis: verum