let X be non empty set ; :: thesis: for R, S being RMembership_Func of X,X st S is transitive & S c= holds
S c=
let R, S be RMembership_Func of X,X; :: thesis: ( S is transitive & S c= implies S c= )
assume A1: ( S is transitive & S c= ) ; :: thesis: S c=
TrCl S c=

proof

for c being Element of [:X,X:] holds (TrCl R) . c <= (TrCl S) . c

proof

let c be Element of [:X,X:]; :: thesis: (TrCl R) . c <= (TrCl S) . c
set Q = { (n iter R) where n is Element of NAT : n > 0 } ;
set RP = RealPoset [.0 ,1.];
{ (n iter R) where n is Element of NAT : n > 0 } c= the carrier of (FuzzyLattice [:X,X:])

proof

let t be set ; :: 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
A2: ( t = i iter R & 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 A2; :: thesis: verum

end;

then A3: (TrCl R) . c = "\/" (pi { (n iter R) where n is Element of NAT : n > 0 } ,c),(RealPoset [.0 ,1.]) by Th32;
(TrCl S) . c is_>=_than pi { (n iter R) where n is Element of NAT : n > 0 } ,c

proof

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 <<= (TrCl S) . 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 <<= (TrCl S) . c )
assume b in pi { (n iter R) where n is Element of NAT : n > 0 } ,c ; :: thesis: b <<= (TrCl S) . c
then consider f being Function such that
A4: ( f in { (n iter R) where n is Element of NAT : n > 0 } & b = f . c ) by CARD_3:def 6;
consider n being Element of NAT such that
A5: ( f = n iter R & n > 0 ) by A4;
( n iter S c= & TrCl S c= ) by A1, A5, Th31, Th39;
then TrCl S c= by Th5;
then (n iter R) . c <= (TrCl S) . c by FUZZY_1:def 3;
hence b <<= (TrCl S) . c by A4, A5, LFUZZY_0:3; :: thesis: verum

end;

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

end;

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

end;

hence TrCl S c= by FUZZY_1:def 3; :: thesis: verum

end;

hence S c= by A1, Th38; :: thesis: verum