let X be non empty set ; :: thesis: for R being RMembership_Func of X,X holds TrCl R c=

let R be RMembership_Func of X,X; :: thesis: TrCl R c=

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

let R be RMembership_Func of X,X; :: thesis: TrCl R c=

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

proof

hence
TrCl R c=
; :: thesis: verum
set Q = { (n iter R) where n is Element of NAT : n > 0 } ;

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

consider x, y being object such that

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

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

R = 1 iter R by Th25;

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

then A2: 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 R . [x,y] <<= (TrCl R) . [x,y] by A2, YELLOW_2:22;

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

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

consider x, y being object such that

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

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

R = 1 iter R by Th25;

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

then A2: 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 R . [x,y] <<= (TrCl R) . [x,y] by A2, YELLOW_2:22;

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