let X be non empty set ; 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; for n being Nat st n > 0 holds
TrCl R c=
let n9 be Nat; ( n9 > 0 implies TrCl R c= )
assume A1:
n9 > 0
; TrCl R c=
for c being Element of [:X,X:] holds (n9 iter R) . c <= (TrCl R) . c
proof
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:];
(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;
verum
end;
hence
TrCl R c=
; verum