let X be non empty set ; :: thesis: for R being RMembership_Func of X,X

for n being Nat st n > 0 holds

TrCl R c=

let R be RMembership_Func of X,X; :: thesis: for n being Nat st n > 0 holds

TrCl R c=

let n9 be Nat; :: thesis: ( n9 > 0 implies TrCl R c= )

assume A1: n9 > 0 ; :: thesis: TrCl R c=

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

for n being Nat st n > 0 holds

TrCl R c=

let R be RMembership_Func of X,X; :: thesis: for n being Nat st n > 0 holds

TrCl R c=

let n9 be Nat; :: thesis: ( n9 > 0 implies TrCl R c= )

assume A1: n9 > 0 ; :: thesis: TrCl R c=

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

proof

hence
TrCl R c=
; :: thesis: verum
reconsider n9 = n9 as Element of NAT by ORDINAL1:def 12;

set Q = { (n iter R) where n is Element of NAT : n > 0 } ;

let c be Element of [:X,X:]; :: thesis: (n9 iter R) . c <= (TrCl R) . c

consider x, y being object such that

A2: [x,y] = c by RELAT_1:def 1;

reconsider x = x, y = y as Element of X by A2, ZFMISC_1:87;

n9 iter R in { (n iter R) where n is Element of NAT : n > 0 } by A1;

then A3: (n9 iter R) . [x,y] in pi ( { (n iter R) where n is Element of NAT : n > 0 } ,[x,y]) by CARD_3:def 6;

(TrCl R) . [x,y] = "\/" ((pi ( { (n iter R) where n is Element of NAT : n > 0 } ,[x,y])),(RealPoset [.0,1.])) by Th29;

then (n9 iter R) . [x,y] <<= (TrCl R) . [x,y] by A3, YELLOW_2:22;

hence (n9 iter R) . c <= (TrCl R) . c by A2, LFUZZY_0:3; :: thesis: verum

end;set Q = { (n iter R) where n is Element of NAT : n > 0 } ;

let c be Element of [:X,X:]; :: thesis: (n9 iter R) . c <= (TrCl R) . c

consider x, y being object such that

A2: [x,y] = c by RELAT_1:def 1;

reconsider x = x, y = y as Element of X by A2, ZFMISC_1:87;

n9 iter R in { (n iter R) where n is Element of NAT : n > 0 } by A1;

then A3: (n9 iter R) . [x,y] in pi ( { (n iter R) where n is Element of NAT : n > 0 } ,[x,y]) by CARD_3:def 6;

(TrCl R) . [x,y] = "\/" ((pi ( { (n iter R) where n is Element of NAT : n > 0 } ,[x,y])),(RealPoset [.0,1.])) by Th29;

then (n9 iter R) . [x,y] <<= (TrCl R) . [x,y] by A3, YELLOW_2:22;

hence (n9 iter R) . c <= (TrCl R) . c by A2, LFUZZY_0:3; :: thesis: verum