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 object ; :: 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) and
i > 0 and
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;
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
A3: f in { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } and
A4: 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) and
A6: i > 0 and
j > 0 by A3;
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 ;
hence b <<= (TrCl R) . c by A4, LFUZZY_0:3; :: thesis: verum
end;
then (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;
then A8: "\/" ((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;
((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 ;
hence ((TrCl R) (#) (TrCl R)) . c <= (TrCl R) . c by A8, LFUZZY_0:3; :: thesis: verum
end;
then TrCl R c= ;
hence TrCl R is transitive ; :: thesis: verum