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 that
A1: S is transitive and
A2: S c= ; :: thesis: S c=
for c being Element of [:X,X:] holds (TrCl R) . c <= (TrCl S) . 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 <= (TrCl S) . 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 <<= (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
A3: f in { (n iter R) where n is Element of NAT : n > 0 } and
A4: b = f . c by CARD_3:def 6;
consider n being Element of NAT such that
A5: f = n iter R and
A6: n > 0 by A3;
A7: TrCl S c= by A6, Th31;
n iter S c= by A2, Th39;
then TrCl S c= by A7, Th5;
then (n iter R) . c <= (TrCl S) . c ;
hence b <<= (TrCl S) . c by A4, A5, LFUZZY_0:3; :: thesis: verum

end;

then (TrCl S) . c is_>=_than pi ( { (n iter R) where n is Element of NAT : n > 0 } ,c) by LATTICE3:def 9;
then A8: "\/" ((pi ( { (n iter R) where n is Element of NAT : n > 0 } ,c)),(RealPoset [.0,1.])) <<= (TrCl S) . c by YELLOW_0:32;
{ (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
A9: 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 A9; :: 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;
hence (TrCl R) . c <= (TrCl S) . c by A8, LFUZZY_0:3; :: thesis: verum

end;

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