### The Mizar article:

### Transitive Closure of Fuzzy Relations

**by****Takashi Mitsuishi, and****Grzegorz Bancerek**

- Received November 23, 2003
Copyright (c) 2003 Association of Mizar Users

- MML identifier: LFUZZY_1
- [ MML identifier index ]

environ vocabulary LFUZZY_0, ARYTM, RELAT_2, LATTICES, RCOMP_1, FUNCT_1, RELAT_1, QC_LANG1, FUZZY_3, SEQ_1, FUZZY_1, GROUP_1, LATTICE2, LATTICE3, WAYBEL_0, SQUARE_1, BOOLE, SEQ_4, BHSP_3, ORDINAL2, FUNCT_2, PARTFUN1, FUNCT_4, CARD_3, WAYBEL_1, FUNCOP_1, FUZZY_4, FUNCT_3, LFUZZY_1; notation TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, FUNCT_1, FUNCT_2, ORDINAL1, ORDINAL2, NUMBERS, XCMPLX_0, DOMAIN_1, PARTFUN1, CARD_3, RELAT_2, FUNCT_3, RFUNCT_1, SUBSET_1, XREAL_0, NAT_1, SQUARE_1, SEQ_1, SEQ_4, RCOMP_1, RELSET_1, STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, WAYBEL_1, WAYBEL_3, FUZZY_1, FUZZY_3, FUZZY_4, PRE_CIRC, LFUZZY_0; constructors NAT_1, WAYBEL_2, PSCOMP_1, WAYBEL_3, FUZZY_4, DOMAIN_1, ORDERS_3, PRE_CIRC, FUZZY_3, MONOID_0, LFUZZY_0, RFUNCT_1, REAL_1; clusters SUBSET_1, LATTICE3, RELSET_1, STRUCT_0, MONOID_0, SEQ_1, NAT_1, ORDINAL2, WAYBEL_2, WAYBEL10, WAYBEL17, LFUZZY_0, INT_1, MEMBERED, BINARITH; requirements BOOLE, SUBSET, NUMERALS, REAL, ARITHM; definitions TARSKI, XBOOLE_0; theorems ZFMISC_1, WAYBEL_1, AXIOMS, RELAT_1, LATTICE3, SQUARE_1, YELLOW_0, XREAL_0, TARSKI, TOPMETR3, YELLOW_2, WAYBEL_3, CARD_3, YELLOW_1, FUNCOP_1, FUZZY_2, FUZZY_4, FUNCT_3, FUZZY_1, PARTFUN1, LFUZZY_0, RELAT_2, ORDINAL2, XCMPLX_1, ANALOAF; schemes FRAENKEL, RECDEF_1, NAT_1, LFUZZY_0, BINARITH; begin :: Inclusion of fuzzy relations reserve X, Y, Z for non empty set; Th7: for a,b,c,d being real number st a <= b & c <= d holds min(a,c) <= min(b,d) proof let a,b,c,d be real number; assume A1:a <= b & c <= d; reconsider a,b,c,d as Element of REAL by XREAL_0:def 1; a <= b & c <= d by A1; hence thesis by FUZZY_1:44; end; definition let X be non empty set; cluster -> real-yielding Membership_Func of X; coherence; end; definition let f,g be real-yielding Function; pred f is_less_than g means:Def0: dom f c= dom g & for x being set st x in dom f holds f.x <= g.x; end; definition let X be non empty set; let f,g be Membership_Func of X; redefine pred f is_less_than g means :Def1: for x being Element of X holds f.x <= g.x; compatibility proof thus f is_less_than g iff for x being Element of X holds f.x <= g.x proof hereby assume AA: f is_less_than g; thus for x being Element of X holds f.x <= g.x proof let x be Element of X; dom f = X by FUZZY_1:def 1; hence thesis by AA,Def0; end; end; assume A4: for x being Element of X holds f.x <= g.x; A3: dom f = X & dom g = X by FUZZY_1:def 1; for x being set st x in dom f holds f.x <= g.x by A4; hence f is_less_than g by A3,Def0; end; end; synonym f c= g; end; definition let X,Y be non empty set; let f,g be RMembership_Func of X,Y; redefine pred f is_less_than g means :Def2: for x being Element of X, y being Element of Y holds f. [x,y] <= g. [x,y]; compatibility proof thus f is_less_than g iff for x being Element of X, y being Element of Y holds f. [x,y] <= g. [x,y] proof hereby assume AA: f is_less_than g; thus for x being Element of X, y being Element of Y holds f. [x,y] <= g. [x,y] proof let x be Element of X, y be Element of Y; dom f = [:X,Y:] & [x,y] in [:X,Y:] by FUZZY_1:def 1; hence thesis by AA,Def0; end; end; assume A4: for x being Element of X, y being Element of Y holds f. [x,y] <= g. [x,y]; A3: dom f = [:X,Y:] & dom g = [:X,Y:] by FUZZY_1:def 1; for c being set st c in dom f holds f.c <= g.c proof let c be set; assume A: c in dom f; consider x,y being set such that A6: [x,y] = c by A, ZFMISC_1:102; reconsider x as Element of X by ZFMISC_1:106,A6,A; reconsider y as Element of Y by ZFMISC_1:106,A6,A; f. [x,y] <= g. [x,y] by A4; hence thesis by A6; end; hence f is_less_than g by Def0,A3; end; end; end; theorem Th1_0: for R,S being Membership_Func of X st for x being Element of X holds R.x = S.x holds R = S proof let R,S be Membership_Func of X; assume A5: for x being Element of X holds R.x = S.x; A4: dom R = X & dom S = X by FUZZY_1:def 1; for x being Element of X st x in dom R holds R.x = S.x by A5; hence R = S by A4,PARTFUN1:34; end; theorem Th1: for R,S being RMembership_Func of X,Y st for x being Element of X, y being Element of Y holds R. [x,y] = S. [x,y] holds R = S proof let R,S be RMembership_Func of X,Y; assume A5:for x being Element of X, y being Element of Y holds R. [x,y] = S. [x,y]; A4:dom R = [:X,Y:] & dom S = [:X,Y:] by FUZZY_1:def 1; for x,y being set st [x,y] in dom R holds R. [x,y] = S. [x,y] proof let x,y be set; assume Z1: [x,y] in dom R; reconsider x as Element of X by Z1, ZFMISC_1:106; reconsider y as Element of Y by Z1, ZFMISC_1:106; R. [x,y] = S. [x,y] by A5; hence thesis; end; hence R = S by A4,PARTFUN1:35; end; theorem FUZZY13: for R,S being Membership_Func of X holds R = S iff R c= S & S c= R proof let R,S be Membership_Func of X; hereby assume R=S;then for x being Element of X holds R.x <= S.x & S.x <= R.x; hence R c= S & S c= R by Def1; end; assume AS: R c= S & S c= R; for x being Element of X holds R.x = S.x proof let x be Element of X; R.x <R= S.x & S.x <R= R.x by AS,Def1; hence thesis by AXIOMS:21; end; hence R=S by Th1_0; end; theorem FUZZY14: for R being Membership_Func of X holds R c= R proof let R be Membership_Func of X; for x being Element of X holds R.x <= R.x; hence thesis by Def1; end; theorem FUZZY15: for R,S,T being Membership_Func of X holds R c= S & S c= T implies R c= T proof let R,S,T be Membership_Func of X; assume A1: R c= S & S c= T; for x being Element of X holds R.x <= T.x proof let x be Element of X; R.x <R= S.x & S.x <R= T.x by A1,Def1; hence thesis by AXIOMS:22; end; hence thesis by Def1; end; theorem FUZZY430: for X,Y,Z being non empty set, R,S being RMembership_Func of X,Y, T,U being RMembership_Func of Y,Z holds R c= S & T c= U implies R(#)T c= S(#)U proof let X,Y,Z be non empty set; let R,S be RMembership_Func of X,Y; let T,U be RMembership_Func of Y,Z; assume AS: R c= S & T c= U; for c being Element of [:X,Z:] holds (R(#)T).c <= (S(#)U).c proof let c be Element of [:X,Z:]; consider x,z being set such that A3: [x,z] = c by ZFMISC_1:102; A1: x in X & z in Z by ZFMISC_1:106,A3; for y be set st y in Y holds R. [x,y] <= S. [x,y] & T. [y,z] <= U. [y,z] proof let y be set; assume y in Y; then [x,y] in [:X,Y:] & [y,z] in [:Y,Z:] by A1,ZFMISC_1:106; hence thesis by AS,Def1; end; hence thesis by A3,FUZZY_4:29,A1; end; hence thesis by Def1; end; definition let X be non empty set; let f,g be Membership_Func of X; redefine func min(f,g); commutativity by FUZZY_1:7; redefine func max(f,g); commutativity by FUZZY_1:7; end; theorem for f,g being Membership_Func of X holds min(f,g) c= f proof let f,g be Membership_Func of X; let x be Element of X; min(f,g).x = min(f.x,g.x) by FUZZY_1:def 5; hence min(f,g).x <= f.x by SQUARE_1:35; end; theorem for f,g being Membership_Func of X holds f c= max(f,g) proof let f,g be Membership_Func of X; let x be Element of X; max(f,g).x = max(f.x,g.x) by FUZZY_1:def 6; hence thesis by SQUARE_1:46; end; begin :: Properties of fuzzy relations definition let X be non empty set; let R be RMembership_Func of X,X; attr R is reflexive means:Def3: Imf(X,X) c= R; end; definition let X be non empty set; let R be RMembership_Func of X,X; redefine attr R is reflexive means :Def4: for x being Element of X holds R. [x,x] = 1; compatibility proof thus R is reflexive iff for x being Element of X holds R. [x,x] = 1 proof hereby assume R is reflexive;then A3: Imf(X,X) c= R by Def3; thus for x being Element of X holds R. [x,x] = 1 proof let x be Element of X; Imf(X,X). [x,x] <= R. [x,x] & Imf(X,X). [x,x] = 1 by Def2,A3,FUZZY_4:def 6; then R. [x,x] <= 1 & R. [x,x] >= 1 by FUZZY_4:4; hence thesis by AXIOMS:21; end; end; assume A0: for x being Element of X holds R. [x,x] = 1; for x,y being Element of X holds Imf(X,X). [x,y] <= R. [x,y] proof let x,y be Element of X; per cases; suppose A1: x = y; A2: Imf(X,X). [x,y] = 1 by A1,FUZZY_4:def 6; thus thesis by A1,A2,A0; suppose not x=y;then Imf(X,X). [x,y] = 0 by FUZZY_4:def 6; hence thesis by FUZZY_4:4; end; then Imf(X,X) c= R by Def2; hence R is reflexive by Def3; end; end; end; definition let X be non empty set; let R be RMembership_Func of X,X; attr R is symmetric means :Def5: converse R = R; end; definition let X be non empty set; let R be RMembership_Func of X,X; redefine attr R is symmetric means :Def6: for x,y being Element of X holds R. [x,y] = R. [y,x]; compatibility proof thus R is symmetric iff for x,y being Element of X holds R. [x,y] = R. [y,x] proof hereby assume R is symmetric;then converse R = R by Def5; hence for x,y being Element of X holds R. [x,y] = R. [y,x] by FUZZY_4:def 1; end; assume A3:for x,y being Element of X holds R. [x,y] = R. [y,x]; A4:dom converse R = [:X,X:] & dom R = [:X,X:] by FUZZY_1:def 1; for x,y being set st [x,y] in dom R holds (converse R). [x,y] = R. [x,y] proof let x,y be set; assume [x,y] in dom R;then reconsider x,y as Element of X by ZFMISC_1:106; R. [x,y] = R. [y,x] by A3; hence thesis by FUZZY_4:def 1; end; then converse R = R by PARTFUN1:35,A4; hence R is symmetric by Def5; end; end; end; definition let X be non empty set; let R be RMembership_Func of X,X; attr R is transitive means :Def7: R (#) R c= R; end; Th2: for X,Y,Z being non empty set for R being RMembership_Func of X,Y for S being RMembership_Func of Y,Z for x being Element of X, z being Element of Z holds rng min(R,S,x,z) = {R. [x,y] "/\" S. [y,z] where y is Element of Y: not contradiction} & rng min(R,S,x,z) <> {} proof let X,Y,Z be non empty set; let R be RMembership_Func of X,Y; let S be RMembership_Func of Y,Z; let x be Element of X, z being Element of Z; C2: Y = dom min(R,S,x,z) & min(R,S,x,z) is PartFunc of dom min(R,S,x,z), rng min(R,S,x,z) by FUZZY_1:def 1, PARTFUN1:24; set L = {R. [x,y] "/\" S. [y,z] where y is Element of Y: not contradiction}; for c be set holds c in L iff c in rng min(R,S,x,z) proof let c be set; hereby assume c in L;then consider y being Element of Y such that C9: c = R. [x,y] "/\" S. [y,z]; c = min(R. [x,y], S. [y,z] qua real number) by LFUZZY_0:5,C9 .= min(R,S,x,z).y by FUZZY_4:def 3; hence c in rng min(R,S,x,z) by C2,PARTFUN1:27; end; assume c in rng min(R,S,x,z);then consider y being Element of Y such that C3: y in dom min(R,S,x,z) & c = min(R,S,x,z).y by PARTFUN1:26; c = min(R. [x,y], S. [y,z] qua real number) by FUZZY_4:def 3,C3 .= R. [x,y] "/\" S. [y,z] by LFUZZY_0:5; hence c in L; end; hence rng min(R,S,x,z) = L by TARSKI:2; thus rng min(R,S,x,z) <> {} proof ex d be set st d in rng min(R,S,x,z) proof consider y being Element of Y; take d = min(R,S,x,z).y; thus d in rng min(R,S,x,z) by C2,PARTFUN1:27; end; hence thesis; end; end; definition let X be non empty set; let R be RMembership_Func of X,X; redefine attr R is transitive means for x,y,z being Element of X holds R. [x,y] "/\" R. [y,z] <<= R. [x,z]; compatibility proof thus R is transitive iff for x,y,z being Element of X holds R. [x,y] "/\" R. [y,z] <<= R. [x,z] proof hereby assume R is transitive;then AS: R (#) R c= R by Def7; thus for x,y,z being Element of X holds R. [x,y] "/\" R. [y,z] <<= R. [x,z] proof let x,y,z be Element of X; R. [x,y] "/\" R. [y,z] in {R. [x,y'] "/\" R. [y',z] where y' is Element of X: not contradiction};then R. [x,y] "/\" R. [y,z] <<= "\/"({R. [x,y'] "/\" R. [y',z] where y' is Element of X: not contradiction}, RealPoset [. 0,1 .]) by YELLOW_2:24; then R. [x,y] "/\" R. [y,z] <<= (R (#) R). [x,z] by LFUZZY_0:22; then R. [x,y] "/\" R. [y,z] <= (R (#) R). [x,z] & (R (#) R). [x,z] <= R. [x,z] by LFUZZY_0:3,AS,Def2; then R. [x,y] "/\" R. [y,z] <= R. [x,z] by AXIOMS:22; hence thesis by LFUZZY_0:3; end; end; assume A2: for x,y,z being Element of X holds R. [x,y] "/\" R. [y,z] <<= R. [x,z]; thus R (#) R c= R proof let x,z be Element of X; set W = rng min(R,R,x,z); A3: W <> {} & W = {R. [x,y'] "/\" R. [y',z] where y' is Element of X: not contradiction} by Th2; for r being real number st r in W holds r <= R. [x,z] proof let r be real number; assume r in W;then r in {R. [x,y'] "/\" R. [y',z] where y' is Element of X: not contradiction} by Th2; then consider y being Element of X such that A4: r = R. [x,y] "/\" R. [y,z]; R. [x,y] "/\" R. [y,z] <<= R. [x,z] by A2; hence thesis by A4,LFUZZY_0:3; end; then upper_bound W <= R. [x,z] by A3,TOPMETR3:1; hence thesis by FUZZY_4:def 4; end; end; end; end; definition let X be non empty set; let R be RMembership_Func of X,X; attr R is antisymmetric means :Def9: for x,y being Element of X holds R. [x,y] <> 0 & R. [y,x] <> 0 implies x = y; end; definition let X be non empty set; let R be RMembership_Func of X,X; redefine attr R is antisymmetric means for x,y being Element of X holds R. [x,y] <> 0 & x <> y implies R. [y,x] = 0; compatibility proof (for x,y being Element of X holds R. [x,y] <> 0 & x <> y implies R. [y,x] = 0) implies for x,y being Element of X holds R. [x,y] <> 0 & R. [y,x] <> 0 implies x = y; hence thesis by Def9; end; end; definition let X; cluster Imf(X,X) -> symmetric transitive reflexive antisymmetric; coherence proof thus Imf(X,X) is symmetric proof let x,y be Element of X; per cases; suppose A1: x=y; thus Imf(X,X). [x,y] = Imf(X,X). [y,x] by A1; suppose A2: not x=y; thus Imf(X,X). [x,y] = 0 by FUZZY_4:def 6,A2 .= Imf(X,X). [y,x] by A2,FUZZY_4:def 6; end; thus Imf(X,X) is transitive proof let x,y,z be Element of X; per cases; suppose A1: x = z; thus thesis proof per cases; suppose A11: x = y; Imf(X,X). [x,y] "/\" Imf(X,X). [y,z] = min(Imf(X,X). [x,y], Imf(X,X). [y,z]) by LFUZZY_0:5 .= 1 by FUZZY_4:def 6, A11, A1;then Imf(X,X). [x,y] "/\" Imf(X,X). [y,z] <= Imf(X,X). [x,z] by FUZZY_4:def 6,A1; hence thesis by LFUZZY_0:3; suppose A12: not x=y; Imf(X,X). [x,y] "/\" Imf(X,X). [y,z] = min(Imf(X,X). [x,y],Imf(X,X). [y,z]) by LFUZZY_0:5 .= min(Imf(X,X). [x,y],0) by FUZZY_4:def 6,A12,A1 .= min(0,0) by FUZZY_4:def 6,A12 .= 0;then Imf(X,X). [x,y] "/\" Imf(X,X). [y,z] <= 1;then Imf(X,X). [x,y] "/\" Imf(X,X). [y,z] <= Imf(X,X). [x,z] by FUZZY_4:def 6,A1; hence thesis by LFUZZY_0:3; end; suppose A2: not x=z; thus thesis proof per cases; suppose A21: x=y; Imf(X,X). [x,y] "/\" Imf(X,X). [y,z] = min(Imf(X,X). [x,y],Imf(X,X). [y,z]) by LFUZZY_0:5 .= min(Imf(X,X). [x,y],0) by FUZZY_4:def 6,A21,A2 .= min(1,0) by FUZZY_4:def 6,A21 .= 0 by SQUARE_1:def 1;then Imf(X,X). [x,y] "/\" Imf(X,X). [y,z] <= Imf(X,X). [x,z] by FUZZY_4:def 6,A2; hence thesis by LFUZZY_0:3; suppose A22: x <> y; thus thesis proof per cases; suppose A221: y=z; Imf(X,X). [x,y] "/\" Imf(X,X). [y,z] = min(Imf(X,X). [x,y],Imf(X,X). [y,z]) by LFUZZY_0:5 .= min(Imf(X,X). [x,y],1) by FUZZY_4:def 6,A221 .= min(0,1) by FUZZY_4:def 6,A22 .= 0 by SQUARE_1:def 1;then Imf(X,X). [x,y] "/\" Imf(X,X). [y,z] <= Imf(X,X). [x,z] by FUZZY_4:def 6,A2; hence thesis by LFUZZY_0:3; suppose A222: y <> z; Imf(X,X). [x,y] "/\" Imf(X,X). [y,z] = min(Imf(X,X). [x,y],Imf(X,X). [y,z]) by LFUZZY_0:5 .= min(Imf(X,X). [x,y],0) by FUZZY_4:def 6,A222 .= min(0,0) by FUZZY_4:def 6,A22 .= 0;then Imf(X,X). [x,y] "/\" Imf(X,X). [y,z] <= Imf(X,X). [x,z] by FUZZY_4:def 6,A2; hence thesis by LFUZZY_0:3; end; end; end; thus Imf(X,X) is reflexive proof thus for x being Element of X holds Imf(X,X). [x,x] = 1 by FUZZY_4:def 6; end; thus for x,y being Element of X holds Imf(X,X). [x,y] <> 0 & x <> y implies Imf(X,X). [y,x] = 0 by FUZZY_4:def 6; end; end; definition let X; cluster reflexive transitive symmetric antisymmetric RMembership_Func of X,X; existence proof take Imf(X,X); thus thesis; end; end; theorem Th4: for R,S being RMembership_Func of X,X holds R is symmetric & S is symmetric implies converse min(R,S) = min(R,S) proof let R,S be RMembership_Func of X,X; assume R is symmetric & S is symmetric;then A1:converse R = R & converse S =S by Def5; thus thesis by A1,FUZZY_4:11; end; theorem Th5: for R,S being RMembership_Func of X,X holds R is symmetric & S is symmetric implies converse max(R,S) = max(R,S) proof let R,S be RMembership_Func of X,X; assume R is symmetric & S is symmetric;then A1:converse R = R & converse S =S by Def5; thus thesis by FUZZY_4:9,A1; end; definition let X; let R,S be symmetric RMembership_Func of X,X; cluster min(R,S) -> symmetric; coherence proof converse min(R,S) = min(R,S) by Th4; hence thesis by Def5; end; cluster max(R,S) -> symmetric; coherence proof converse max(R,S) = max(R,S) by Th5; hence thesis by Def5; end; end; theorem Th6: for R,S being RMembership_Func of X,X holds R is transitive & S is transitive implies min(R,S) (#) min(R,S) c= min(R,S) proof let R,S be RMembership_Func of X,X; assume R is transitive & S is transitive; then Z1: R(#)R c= R & S(#)S c= S by Def7; let x be Element of X, y be Element of X; A2: (min(R,S) (#) min(R,S)). [x,y] <= min(min(R,S) (#) R, min(R,S) (#) S). [x,y] by FUZZY_4:23; min(min(R,S) (#) R, min(R,S) (#) S). [x,y] = min((min(R,S) (#) R). [x,y], (min(R,S) (#) S). [x,y]) & (min(R,S) (#) R). [x,y] <= min(R(#)R, S(#)R). [x,y] & (min(R,S) (#) S). [x,y] <= min(R(#)S, S(#)S). [x,y] by FUZZY_1:def 5,FUZZY_4:25; then min(min(R,S) (#) R, min(R,S) (#) S). [x,y] <= min(min(R(#)R, S(#)R). [x,y],min(R(#)S, S(#)S). [x,y]) by Th7; then A4: (min(R,S) (#) min(R,S)). [x,y] <= min(min(R(#)R, S(#)R). [x,y],min(R(#)S, S(#)S). [x,y]) by A2,AXIOMS:22; min(R(#)R, S(#)R). [x,y] = min((R(#)R). [x,y], (S(#)R). [x,y]) & min(R(#)S, S(#)S). [x,y] = min((S(#)S). [x,y], (R(#)S). [x,y]) by FUZZY_1:def 5; then min(R(#)R, S(#)R). [x,y] <= (R(#)R). [x,y] & min(R(#)S, S(#)S). [x,y] <= (S(#)S). [x,y] & (R(#)R). [x,y] <= R. [x,y] & (S(#)S). [x,y] <= S. [x,y] by Z1,Def2,SQUARE_1:35; then min(R(#)R, S(#)R). [x,y] <= R. [x,y] & min(R(#)S, S(#)S). [x,y] <= S. [x,y] by AXIOMS:22; then min(min(R(#)R, S(#)R). [x,y],min(R(#)S, S(#)S). [x,y]) <= min(R. [x,y], S. [x,y]) by Th7; then (min(R,S) (#) min(R,S)). [x,y] <= min(R. [x,y], S. [x,y]) by A4,AXIOMS:22; hence thesis by FUZZY_1:def 5; end; definition let X; let R,S be transitive RMembership_Func of X,X; cluster min(R,S) -> transitive; coherence proof min(R,S) (#) min(R,S) c= min(R,S) by Th6; hence thesis by Def7; end; end; definition let A be set, X be non empty set; redefine func chi(A,X) -> Membership_Func of X; coherence proof dom chi(A,X) = X & rng chi(A,X) c= [. 0,1 .] by FUZZY_1:1,FUNCT_3:def 3; hence chi(A,X) is Membership_Func of X by FUZZY_1:def 1; end; end; theorem for r being Relation of X st r is_reflexive_in X holds chi(r,[:X,X:]) is reflexive proof let r be Relation of X; assume A1:r is_reflexive_in X; for x being Element of X holds chi(r,[:X,X:]). [x,x] = 1 proof let x be Element of X; [x,x] in r by RELAT_2:def 1,A1; hence thesis by FUNCT_3:def 3; end; hence thesis by Def4; end; theorem for r being Relation of X st r is antisymmetric holds chi(r,[:X,X:]) is antisymmetric proof let r be Relation of X; assume r is antisymmetric;then A1:r is_antisymmetric_in field r by RELAT_2:def 12; for x,y being Element of X holds chi(r,[:X,X:]). [x,y] <> 0 & chi(r,[:X,X:]). [y,x] <> 0 implies x = y proof let x,y be Element of X; assume chi(r,[:X,X:]). [x,y] <> 0 & chi(r,[:X,X:]). [y,x] <> 0;then A2: [x,y] in r & [y,x] in r by FUNCT_3:def 3; x in field r & y in field r & [x,y] in r & [y,x] in r implies x = y by RELAT_2:def 4,A1; hence thesis by A2,RELAT_1:30; end; hence thesis by Def9; end; theorem for r being Relation of X st r is symmetric holds chi(r,[:X,X:]) is symmetric proof let r be Relation of X; assume r is symmetric;then A1:r is_symmetric_in field r by RELAT_2:def 11; let x,y be Element of X; A2: (x in field r & y in field r & [x,y] in r implies [y,x] in r) & (x in field r & y in field r & [y,x] in r implies [x,y] in r) by RELAT_2:def 3,A1; per cases; suppose A3: [x,y] in r; chi(r,[:X,X:]). [x,y] = 1 & chi(r,[:X,X:]). [y,x] = 1 by A2, RELAT_1:30,A3,FUNCT_3:def 3; hence thesis; suppose A4: not [x,y] in r; not [y,x] in r by A2,RELAT_1:30,A4; then chi(r,[:X,X:]). [x,y] = 0 & chi(r,[:X,X:]). [y,x] = 0 by A4,FUNCT_3:def 3; hence thesis; end; theorem for r being Relation of X st r is transitive holds chi(r,[:X,X:]) is transitive proof let r be Relation of X; assume r is transitive;then A1:r is_transitive_in field r by RELAT_2:def 16; let x,y,z be Element of X; A2: x in field r & y in field r & z in field r & [x,y] in r & [y,z] in r implies [x,z] in r by RELAT_2:def 8,A1; per cases; suppose B1: [x,y] in r; thus thesis proof per cases; suppose B2: [y,z] in r; chi(r,[:X,X:]). [x,y] "/\" chi(r,[:X,X:]). [y,z] = min(chi(r,[:X,X:]). [x,y] , chi(r,[:X,X:]). [y,z]) by LFUZZY_0:5 .= min(1,chi(r,[:X,X:]). [y,z]) by B1,FUNCT_3:def 3 .= min(1,1) by B2,FUNCT_3:def 3 .= chi(r,[:X,X:]). [x,z] by RELAT_1:30,B1,B2,A2,FUNCT_3:def 3; hence thesis by LFUZZY_0:3; suppose B3: not [y,z] in r; chi(r,[:X,X:]). [x,y] "/\" chi(r,[:X,X:]). [y,z] = min(chi(r,[:X,X:]). [x,y] , chi(r,[:X,X:]). [y,z]) by LFUZZY_0:5 .= min(1,chi(r,[:X,X:]). [y,z]) by B1,FUNCT_3:def 3 .= min(1,0) by B3,FUNCT_3:def 3 .= 0 by SQUARE_1:def 1; then chi(r,[:X,X:]). [x,y] "/\" chi(r,[:X,X:]). [y,z] <= chi(r,[:X,X:]). [x,z] by FUZZY_2:1; hence thesis by LFUZZY_0:3; end; suppose B4: not [x,y] in r; thus thesis proof per cases; suppose B5: [y,z] in r; chi(r,[:X,X:]). [x,y] "/\" chi(r,[:X,X:]). [y,z] = min(chi(r,[:X,X:]). [x,y] , chi(r,[:X,X:]). [y,z]) by LFUZZY_0:5 .= min(0,chi(r,[:X,X:]). [y,z]) by B4,FUNCT_3:def 3 .= min(0,1) by B5,FUNCT_3:def 3 .= 0 by SQUARE_1:def 1; then chi(r,[:X,X:]). [x,y] "/\" chi(r,[:X,X:]). [y,z] <= chi(r,[:X,X:]). [x,z] by FUZZY_2:1; hence thesis by LFUZZY_0:3; suppose B6: not [y,z] in r; chi(r,[:X,X:]). [x,y] "/\" chi(r,[:X,X:]). [y,z] = min(chi(r,[:X,X:]). [x,y] , chi(r,[:X,X:]). [y,z]) by LFUZZY_0:5 .= min(0,chi(r,[:X,X:]). [y,z]) by B4,FUNCT_3:def 3 .= min(0,0) by B6,FUNCT_3:def 3 .= 0; then chi(r,[:X,X:]). [x,y] "/\" chi(r,[:X,X:]). [y,z] <= chi(r,[:X,X:]). [x,z] by FUZZY_2:1; hence thesis by LFUZZY_0:3; end; end; theorem Zmf(X,X) is symmetric antisymmetric transitive proof thus Zmf(X,X) is symmetric proof let x,y be Element of X; Zmf(X,X). [x,y] = 0 & Zmf(X,X). [y,x] = 0 by FUZZY_4:32; hence thesis; end; thus Zmf(X,X) is antisymmetric proof let x,y be Element of X; thus thesis by FUZZY_4:32; end; thus Zmf(X,X) is transitive proof let x,y,z be Element of X; A1: Zmf(X,X). [x,y] "/\" Zmf(X,X). [y,z] = min(Zmf(X,X). [x,y], Zmf(X,X). [y,z]) by LFUZZY_0:5 .= min(0, Zmf(X,X). [y,z]) by FUZZY_4:32 .= min(0,0) by FUZZY_4:32 .= 0; Zmf(X,X). [x,z] = 0 by FUZZY_4:32; hence thesis by LFUZZY_0:3,A1; end; end; theorem Umf(X,X) is symmetric transitive reflexive proof thus Umf(X,X) is symmetric proof let x,y be Element of X; thus Umf(X,X). [x,y] = 1 by FUZZY_4:31 .= Umf(X,X). [y,x] by FUZZY_4:31; end; thus Umf(X,X) is transitive proof let x,y,z be Element of X; Umf(X,X). [x,y] "/\" Umf(X,X). [y,z] = min(Umf(X,X). [x,y], Umf(X,X). [y,z]) by LFUZZY_0:5 .= min(1,Umf(X,X). [y,z]) by FUZZY_4:31 .= min(1,1) by FUZZY_4:31 .= 1;then Umf(X,X). [x,y] "/\" Umf(X,X). [y,z] <= Umf(X,X). [x,z] by FUZZY_4:31; hence thesis by LFUZZY_0:3; end; thus Umf(X,X) is reflexive proof let x be Element of X; thus thesis by FUZZY_4:31; end; end; theorem for R being RMembership_Func of X,X holds max(R,converse R) is symmetric proof let R be RMembership_Func of X,X; set S = max(R,converse R); let x,y be Element of X; thus S. [x,y] = max(R. [x,y], (converse R). [x,y]) by FUZZY_1:def 6 .= max(R. [x,y], R. [y,x]) by FUZZY_4:def 1 .= max((converse R). [y,x], R. [y,x]) by FUZZY_4:def 1 .= S. [y,x] by FUZZY_1:def 6; end; theorem for R being RMembership_Func of X,X holds min(R,converse R) is symmetric proof let R be RMembership_Func of X,X; set S = min(R,converse R); let x,y be Element of X; thus S. [x,y] = min(R. [x,y], (converse R). [x,y]) by FUZZY_1:def 5 .= min(R. [x,y], R. [y,x]) by FUZZY_4:def 1 .= min((converse R). [y,x], R. [y,x]) by FUZZY_4:def 1 .= S. [y,x] by FUZZY_1:def 5; end; theorem for R being RMembership_Func of X,X for R' being RMembership_Func of X,X st R' is symmetric & R c= R' holds max(R, converse R) c= R' proof let R be RMembership_Func of X,X; let T be RMembership_Func of X,X; assume AB0: T is symmetric & R c= T; let x,y be Element of X; A6: R. [x,y] <= T. [x,y] & R. [y,x] <= T. [y,x] by AB0,Def1; then R. [y,x] <= T. [x,y] by AB0,Def6; then max(R. [x,y], R. [y,x]) <= T. [x,y] by A6,SQUARE_1:50; then max(R. [x,y], (converse R). [x,y]) <= T. [x,y] by FUZZY_4:def 1; hence thesis by FUZZY_1:def 6; end; theorem for R being RMembership_Func of X,X for R' being RMembership_Func of X,X st R' is symmetric & R' c= R holds R' c= min(R, converse R) proof let R be RMembership_Func of X,X; let T be RMembership_Func of X,X; assume AB0: T is symmetric & T c= R; let x,y be Element of X; A6: T. [x,y] <= R. [x,y] & T. [y,x] <= R. [y,x] by AB0,Def1; then T. [x,y] <= R. [y,x] by AB0,Def6; then T. [x,y] <= min(R. [x,y], R. [y,x]) by A6,SQUARE_1:39; then T. [x,y] <= min(R. [x,y], (converse R). [x,y]) by FUZZY_4:def 1; hence thesis by FUZZY_1:def 5; end; begin :: Transitive closure of a fuzzy relation definition let X be non empty set; let R be RMembership_Func of X,X; let n be natural number; func n iter R -> RMembership_Func of X,X means :Def11: ex F being Function of NAT,Funcs([:X,X:],[. 0,1 .]) st it = F.n & F.0 = Imf(X,X) & for k being natural number ex Q being RMembership_Func of X,X st F.k = Q & F.(k + 1) = Q (#) R; existence proof set D = the carrier of FuzzyLattice [:X,X:]; defpred P[set,set,set] means ex Q being Element of D st $2 = Q & $3 = @Q (#) R; A1: for k being Element of NAT for x being Element of D ex y being Element of D st P[k,x,y] proof let k be Element of NAT; let Q be Element of D; set y = @Q (#) R; reconsider y' = ([:X,X:],y)@ as Element of D; take y'; y' = @Q (#) R by LFUZZY_0:def 6; hence P[k,Q,y']; end; consider F being Function of NAT,D such that A2: F.0 = ([:X,X:],Imf(X,X))@ & for k being Element of NAT holds P[k,F.k,F.(k+1)] from RecExD(A1); Funcs([:X,X:],[. 0,1 .]) = the carrier of FuzzyLattice [:X,X:] by LFUZZY_0:14;then reconsider F as Function of NAT,Funcs([:X,X:],[. 0,1 .]); reconsider n' = n as Element of NAT by ORDINAL2:def 21; reconsider IT = F.n' as Element of FuzzyLattice [:X,X:] by LFUZZY_0:14; reconsider IT' = @(IT) as RMembership_Func of X,X; take IT'; thus ex F being Function of NAT,Funcs([:X,X:],[. 0,1 .]) st IT' = F.n & F.0 = Imf(X,X) & for k being natural number ex Q being RMembership_Func of X,X st F.k = Q & F.(k + 1) = Q (#) R proof take F; thus IT' = F.n by LFUZZY_0:def 5; thus F.0 = Imf(X,X) by A2,LFUZZY_0:def 6; thus for k being natural number ex Q being RMembership_Func of X,X st F.k = Q & F.(k + 1) = Q (#) R proof let k be natural number; reconsider n=k as Element of NAT by ORDINAL2:def 21; reconsider Q' = F.n as Element of D by LFUZZY_0:14; reconsider Q = @Q' as RMembership_Func of X,X; take Q; thus F.k = Q by LFUZZY_0:def 5; P[n,F.n,F.(n+1)] by A2; hence F.(k + 1) = Q (#) R; end; end; end; uniqueness proof let S,T be RMembership_Func of X,X; given F being Function of NAT,Funcs([:X,X:],[. 0,1 .]) such that A3: S = F.n & F.0 = Imf(X,X) & for k being natural number ex Q being RMembership_Func of X,X st F.k = Q & F.(k + 1) = Q (#) R; given G being Function of NAT,Funcs([:X,X:],[. 0,1 .]) such that A4: T = G.n & G.0 = Imf(X,X) & for k being natural number ex Q being RMembership_Func of X,X st G.k = Q & G.(k + 1) = Q (#) R; defpred P[natural number] means F.$1 = G.$1; A1: P[0] by A3,A4; A2: for k being natural number st P[k] holds P[k+1] proof let k be natural number; assume A5: F.k = G.k; consider Q being RMembership_Func of X,X such that A6: G.k = Q & G.(k + 1) = Q (#) R by A4; consider Q' being RMembership_Func of X,X such that A7: F.k = Q' & F.(k + 1) = Q' (#) R by A3; thus F.(k + 1) = G.(k+1) by A6,A7,A5; end; for k being natural number holds P[k] from Nat_Ind(A1,A2); hence S=T by A3,A4; end; end; reserve X for non empty set; reserve R for RMembership_Func of X,X; theorem th15: Imf(X,X) (#) R = R proof A1: dom (Imf(X,X) (#) R) = [:X,X:] by FUZZY_1:def 1 .= dom R by FUZZY_1:def 1; for x,y being set st [x,y] in dom (Imf(X,X) (#) R) holds (Imf(X,X) (#) R). [x,y] = R. [x,y] proof let x,y be set; assume [x,y] in dom (Imf(X,X) (#) R);then reconsider x,y as Element of X by ZFMISC_1:106; A2: (Imf(X,X) (#) R). [x,y] = "\/"({Imf(X,X). [x,z] "/\" R. [z,y] where z is Element of X: not contradiction}, RealPoset [. 0,1 .]) by LFUZZY_0:22; set S = {Imf(X,X). [x,z] "/\" R. [z,y] where z is Element of X: not contradiction}; A3: R. [x,y] is_>=_than S proof for c being Element of RealPoset [. 0,1 .] st c in S holds c <<= R. [x,y] proof let c be Element of RealPoset [. 0,1 .]; assume c in S;then consider z being Element of X such that A4: c = Imf(X,X). [x,z] "/\" R. [z,y]; per cases; suppose A5: x = z; A6: R. [z,y] <= 1 by FUZZY_4:4; c = min(Imf(X,X). [x,z],R. [z,y]) by LFUZZY_0:5,A4 .= min(R. [z,y],1) by A5,FUZZY_4:def 6 .= R. [x,y] by A5,SQUARE_1:def 1,A6; hence thesis by LFUZZY_0:3; suppose A7: x <> z; A8: 0 <= R. [z,y] by FUZZY_4:4; c = min(Imf(X,X). [x,z],R. [z,y]) by LFUZZY_0:5,A4 .= min(R. [z,y],0) by A7,FUZZY_4:def 6 .= 0 by SQUARE_1:def 1,A8; then c <= R. [x,y] by FUZZY_4:4; hence thesis by LFUZZY_0:3; end; hence thesis by LATTICE3:def 9; end; for b being Element of RealPoset [. 0,1 .] st b is_>=_than S holds R. [x,y] <<= b proof let b be Element of RealPoset [. 0,1 .]; assume AB:b is_>=_than S; A10: R. [x,y] <= 1 by FUZZY_4:4; Imf(X,X). [x,x] "/\" R. [x,y] = min(Imf(X,X). [x,x], R. [x,y]) by LFUZZY_0:5 .= min(1, R. [x,y]) by FUZZY_4:def 6 .= R. [x,y] by SQUARE_1:def 1,A10; then R. [x,y] in S; hence thesis by AB,LATTICE3:def 9; end; hence thesis by A3,YELLOW_0:32,A2; end; hence thesis by PARTFUN1:35,A1; end; theorem th16: R (#) Imf(X,X) = R proof A1: dom (R (#) Imf(X,X)) = [:X,X:] by FUZZY_1:def 1 .= dom R by FUZZY_1:def 1; for x,y being set st [x,y] in dom (R (#) Imf(X,X)) holds (R (#) Imf(X,X)). [x,y] = R. [x,y] proof let x,y be set; assume [x,y] in dom (R (#) Imf(X,X));then reconsider x,y as Element of X by ZFMISC_1:106; A2: (R (#) Imf(X,X)). [x,y] = "\/"({R. [x,z] "/\" Imf(X,X). [z,y] where z is Element of X: not contradiction}, RealPoset [. 0,1 .]) by LFUZZY_0:22; set S = {R. [x,z] "/\" Imf(X,X). [z,y] where z is Element of X: not contradiction}; A3: R. [x,y] is_>=_than S proof for c being Element of RealPoset [. 0,1 .] st c in S holds c <<= R. [x,y] proof let c be Element of RealPoset [. 0,1 .]; assume c in S;then consider z being Element of X such that A4: c = R. [x,z] "/\" Imf(X,X). [z,y]; per cases; suppose A5: y = z; A6: R. [x,z] <= 1 by FUZZY_4:4; c = min(R. [x,z],Imf(X,X). [z,y]) by LFUZZY_0:5 ,A4 .= min(R. [x,z],1) by A5,FUZZY_4:def 6 .= R. [x,y] by SQUARE_1:def 1,A6,A5; hence thesis by LFUZZY_0:3; suppose A7: not y = z; A8: 0 <= R. [x,z] by FUZZY_4:4; c = min(R. [x,z],Imf(X,X). [z,y]) by LFUZZY_0:5,A4 .= min(R. [x,z],0) by A7,FUZZY_4:def 6 .= 0 by SQUARE_1:def 1,A8; then c <= R. [x,y] by FUZZY_4:4; hence thesis by LFUZZY_0:3; end; hence thesis by LATTICE3:def 9; end; for b being Element of RealPoset [. 0,1 .] st b is_>=_than S holds R. [x,y] <<= b proof let b be Element of RealPoset [. 0,1 .]; assume AA:b is_>=_than S; A10: R. [x,y] <= 1 by FUZZY_4:4; R. [x,y] "/\" Imf(X,X). [y,y] = min(R. [x,y],Imf(X,X). [y,y]) by LFUZZY_0:5 .= min( R. [x,y],1) by FUZZY_4:def 6 .= R. [x,y] by SQUARE_1:def 1,A10; then R. [x,y] in S; hence thesis by AA,LATTICE3:def 9; end; hence thesis by A3,YELLOW_0:32,A2; end; hence thesis by PARTFUN1:35,A1; end; theorem th18: 0 iter R = Imf(X,X) proof consider F being Function of NAT,Funcs([:X,X:],[. 0,1 .]) such that A1:0 iter R = F.0 & F.0 = Imf(X,X) & for k being natural number ex Q being RMembership_Func of X,X st F.k = Q & F.(k + 1) = Q (#) R by Def11; thus thesis by A1; end; theorem th20: 1 iter R = R proof consider F being Function of NAT,Funcs([:X,X:],[. 0,1 .]) such that A1:1 iter R = F.1 & F.0 = Imf(X,X) & for k being natural number ex Q being RMembership_Func of X,X st F.k = Q & F.(k + 1) = Q (#) R by Def11; consider Q being RMembership_Func of X,X such that A2:F.0 = Q & F.(0 + 1) = Q (#) R by A1; thus 1 iter R = R by A1,A2,th15; end; theorem th17: for n being natural number holds (n+1) iter R = (n iter R) (#) R proof let n be natural number; consider f being Function of NAT,Funcs([:X,X:],[. 0,1 .]) such that A1: (n+1) iter R = f.(n+1) & f.0 = Imf(X,X) and A2: for k being natural number ex Q being RMembership_Func of X,X st f.k = Q & f.(k + 1) = Q (#) R by Def11; ex Q being RMembership_Func of X,X st f.n = Q & f.(n + 1) = Q(#)R by A2; hence thesis by A1,A2,Def11; end; theorem th19: for m,n being natural number holds (m+n) iter R = (m iter R) (#) (n iter R) proof let m,n be natural number; defpred P[natural number] means (m+ $1) iter R = (m iter R) (#) ($1 iter R); (m iter R) (#) (0 iter R) = (m iter R) (#) Imf(X,X) by th18 .= m iter R by th16;then A2: P[0]; A3: for n being natural number st P[n] holds P[n+1] proof let n be natural number; assume A1: (m+n) iter R = (m iter R) (#) (n iter R); thus ((m) iter R) (#) ((n+1) iter R) = (m iter R) (#) ((n iter R) (#)R ) by th17 .= ((m+n) iter R) (#) R by A1,LFUZZY_0:23 .= ((m+n)+1) iter R by th17 .= (m+(n+1)) iter R by XCMPLX_1:1; end; for m being natural number holds P[m] from Nat_Ind(A2,A3); hence thesis; end; theorem for m,n being natural number holds (m*n) iter R = m iter (n iter R) proof let m,n be natural number; defpred P[natural number] means ($1 * n) iter R = $1 iter (n iter R); (0*n) iter R = Imf(X,X) by th18 .= 0 iter (n iter R) by th18; then A1: P[0]; A2: for m being natural number st P[m] holds P[m+1] proof let m be natural number; assume A3: (m*n) iter R = m iter (n iter R); A4: ((m+1)*n) iter R = (m*n + 1*n) iter R by XCMPLX_1:8 .= (m iter (n iter R)) (#) (n iter R) by A3,th19; (m+1) iter (n iter R) = (m iter (n iter R)) (#) (1 iter (n iter R)) by th19 .= (m iter (n iter R)) (#) (n iter R) by th20; hence thesis by A4; end; for m being natural number holds P[m] from Nat_Ind(A1,A2); hence thesis; end; definition let X be non empty set; let R be RMembership_Func of X,X; func TrCl R -> RMembership_Func of X,X equals :Def12: "\/"({n iter R where n is Nat : n > 0},FuzzyLattice [:X,X:]); coherence proof set S = "\/"({n iter R where n is Nat : n > 0},FuzzyLattice [:X,X:]); S = @S by LFUZZY_0:def 5; hence S is RMembership_Func of X,X; end; end; theorem lemma: for x,y being Element of X holds (TrCl R). [x,y] = "\/"(pi({n iter R where n is Nat : n > 0}, [x,y]), RealPoset [. 0,1 .]) proof let x,z be Element of X; set Q = {n iter R where n is Nat : n > 0}; A1: FuzzyLattice [:X,X:] = (RealPoset [. 0,1 .]) |^ [:X,X:] by LFUZZY_0:def 4 .= product ([:X,X:] --> RealPoset [. 0,1 .]) by YELLOW_1:def 5; Q c= the carrier of FuzzyLattice [:X,X:] proof let t be set; assume t in Q;then consider n being Nat such that A4: t = n iter R & n > 0; reconsider t as Membership_Func of [:X,X:] by A4; ([:X,X:],t)@ is Element of FuzzyLattice [:X,X:]; then reconsider t as Element of FuzzyLattice [:X,X:] by LFUZZY_0:def 6; t in the carrier of FuzzyLattice [:X,X:]; hence thesis; end;then reconsider Q as Subset of FuzzyLattice [:X,X:]; reconsider i = [x,z] as Element of [:X,X:]; A2: for a being Element of [:X,X:] holds ([:X,X:] --> RealPoset [. 0,1 .]).a is complete LATTICE by FUNCOP_1:13; (sup Q).i = "\/"(pi(Q,i), ([:X,X:] --> RealPoset [. 0,1 .]).i) by A1,A2,WAYBEL_3:32; then ("\/"(Q,FuzzyLattice [:X,X:])). [x,z] = "\/"(pi(Q, [x,z]), RealPoset [. 0,1 .]) by FUNCOP_1:13; hence thesis by Def12; end; theorem th35: R c= TrCl R proof for c being Element of [: X,X :] holds R.c <= (TrCl R).c proof let c be Element of [: X,X :]; set Q = {n iter R where n is Nat : n > 0}; consider x,y being set such that A3: [x,y] = c by ZFMISC_1:102; reconsider x,y as Element of X by ZFMISC_1:106,A3; A4: (TrCl R). [x,y] = "\/"(pi(Q, [x,y]), RealPoset [. 0,1 .]) by lemma; R = 1 iter R by th20;then R in Q;then R. [x,y] in pi(Q, [x,y]) by CARD_3:def 6; then R. [x,y] <<= (TrCl R). [x,y] by A4,YELLOW_2:24; hence thesis by LFUZZY_0:3,A3; end; hence thesis by Def1; end; theorem th33: for n being natural number st n > 0 holds n iter R c= TrCl R proof let n' be natural number; assume A1: n' > 0; for c being Element of [: X,X :] holds (n' iter R).c <= (TrCl R).c proof let c be Element of [: X,X :]; set Q = {n iter R where n is Nat : n > 0}; consider x,y being set such that A3: [x,y] = c by ZFMISC_1:102; reconsider x,y as Element of X by ZFMISC_1:106,A3; A4: (TrCl R). [x,y] = "\/"(pi(Q, [x,y]), RealPoset [. 0,1 .]) by lemma; reconsider n' as Nat by ORDINAL2:def 21; n' iter R in Q by A1;then (n' iter R). [x,y] in pi(Q, [x,y]) by CARD_3:def 6; then (n' iter R). [x,y] <<= (TrCl R). [x,y] by A4,YELLOW_2:24; hence thesis by LFUZZY_0:3,A3; end; hence thesis by Def1; end; theorem th22: for Q being Subset of FuzzyLattice X, x being Element of X holds ("\/"(Q,FuzzyLattice X)). x = "\/"(pi(Q, x), RealPoset [. 0,1 .]) proof let Q be Subset of FuzzyLattice X; let x be Element of X; A1: FuzzyLattice X = (RealPoset [. 0,1 .]) |^ X by LFUZZY_0:def 4 .= product (X --> RealPoset [. 0,1 .]) by YELLOW_1:def 5; A2: for a being Element of X holds (X --> RealPoset [. 0,1 .]).a is complete LATTICE by FUNCOP_1:13; (sup Q).x = "\/"(pi(Q,x), (X --> RealPoset [. 0,1 .]).x) by A1,A2,WAYBEL_3:32; hence ("\/"(Q,FuzzyLattice X)). x = "\/"(pi(Q, x), RealPoset [. 0,1 .]) by FUNCOP_1:13; end; th23: for R being RMembership_Func of X,X, Q being Subset of FuzzyLattice [:X,X:], x,z being Element of X holds {R. [x,y] "/\" (@("\/"(Q,FuzzyLattice [:X,X:]))). [y,z] where y is Element of X: not contradiction} = {R. [x,y] "/\" "\/"(pi(Q, [y,z]), RealPoset [. 0,1 .]) where y is Element of X:not contradiction} proof let R be RMembership_Func of X,X; let Q be Subset of FuzzyLattice [:X,X:]; let x,z be Element of X; defpred P[Element of X] means not contradiction; deffunc F(Element of X) = R. [x,$1] "/\" (@("\/"(Q,FuzzyLattice [:X,X:]))). [$1,z]; deffunc G(Element of X) = R. [x,$1] "/\" "\/"(pi(Q, [$1,z]), RealPoset [. 0,1 .]); for y being Element of X holds R. [x,y] "/\" (@("\/"(Q,FuzzyLattice [:X,X:]))). [y,z] = R. [x,y] "/\" "\/"(pi(Q, [y,z]), RealPoset [. 0,1 .]) proof let y be Element of X; (@("\/"(Q,FuzzyLattice [:X,X:]))). [y,z] = (("\/"(Q,FuzzyLattice [:X,X:]))). [y,z] by LFUZZY_0:def 5 .= "\/"(pi(Q, [y,z]), RealPoset [. 0,1 .]) by th22; hence thesis; end; then A1: for y being Element of X holds F(y) = G(y); thus {F(y) where y is Element of X: P[y]} = {G(y') where y' is Element of X: P[y']} from FraenkelF'(A1); end; theorem LFUZZY015: for R being complete Heyting LATTICE, X being Subset of R, y be Element of R holds y "/\" "\/"(X,R) = "\/"({y "/\" x where x is Element of R: x in X},R) proof let R be complete Heyting LATTICE, X be Subset of R, y be Element of R; for z being Element of R holds z "/\" has_an_upper_adjoint by WAYBEL_1:def 19; hence thesis by WAYBEL_1:67; end; th24: for R being RMembership_Func of X,X, Q being Subset of FuzzyLattice [:X,X:], x,z being Element of X holds {R. [x,y] "/\" "\/"(pi(Q, [y,z]), RealPoset [. 0,1 .]) where y is Element of X:not contradiction} = {"\/"({R. [x,y'] "/\" b where b is Element of RealPoset [. 0,1 .]: b in pi(Q,[y',z])} ,RealPoset [. 0,1 .]) where y' is Element of X:not contradiction} proof let R be RMembership_Func of X,X; let Q be Subset of FuzzyLattice [:X,X:]; let x,z be Element of X; defpred P[Element of X] means not contradiction; deffunc F(Element of X) = R. [x,$1] "/\" "\/"(pi(Q, [$1,z]), RealPoset [. 0,1 .]); deffunc G(Element of X) = "\/"({R. [x,$1] "/\" b where b is Element of RealPoset [. 0,1 .]: b in pi(Q,[$1,z])} ,RealPoset [. 0,1 .]); for y being Element of X holds R. [x,y] "/\" "\/"(pi(Q, [y,z]), RealPoset [. 0,1 .]) = "\/"({R. [x,y] "/\" b where b is Element of RealPoset [. 0,1 .]: b in pi(Q,[y,z])} ,RealPoset [. 0,1 .]) proof let y be Element of X; A1: FuzzyLattice [:X,X:] = (RealPoset [. 0,1 .]) |^ [:X,X:] by LFUZZY_0:def 4 .= product ([:X,X:] --> RealPoset [. 0,1 .]) by YELLOW_1:def 5; reconsider Q as Subset of product ([:X,X:] --> RealPoset [. 0,1 .]) by A1; pi(Q, [y,z]) is Subset of RealPoset [. 0,1 .] by FUNCOP_1:13; hence thesis by LFUZZY015; end; then A1: for y being Element of X holds F(y) = G (y); {F(y) where y is Element of X:P[y]} = {G(y) where y is Element of X:P[y]} from FraenkelF'(A1); hence thesis; end; th25: for R being RMembership_Func of X,X, Q being Subset of FuzzyLattice [:X,X:], x,z being Element of X holds {"\/"({R. [x,y] "/\" b where b is Element of RealPoset [. 0,1 .]: b in pi(Q,[y,z])} ,RealPoset [. 0,1 .]) where y is Element of X:not contradiction} = {"\/"({R. [x,y'] "/\" r. [y',z] where r is Element of FuzzyLattice [:X,X:]: r in Q} ,RealPoset [. 0,1 .]) where y' is Element of X:not contradiction} proof let R be RMembership_Func of X,X; let Q be Subset of FuzzyLattice [:X,X:]; let x,z be Element of X; set RP = RealPoset [. 0,1 .], FL = FuzzyLattice [:X,X:]; defpred P[Element of X] means not contradiction; deffunc F(Element of X) = "\/"({R. [x,$1] "/\" b where b is Element of RP: b in pi(Q,[$1,z])} ,RP); deffunc G(Element of X) = "\/"({R. [x,$1] "/\" r. [$1,z] where r is Element of FL: r in Q} ,RP); for y being Element of X holds "\/"({R. [x,y] "/\" b where b is Element of RP: b in pi(Q,[y,z])} ,RP) = "\/"({R. [x,y] "/\" r. [y,z] where r is Element of FL: r in Q} ,RP) proof let y be Element of X; set A = {R. [x,y] "/\" b where b is Element of RP: b in pi(Q,[y,z])}, B = {R. [x,y] "/\" r. [y,z] where r is Element of FL: r in Q}; A = B proof thus A c= B proof let a be set; assume a in A;then consider b be Element of RP such that A2: a = R. [x,y] "/\" b & b in pi(Q,[y,z]); consider f be Function such that A3: f in Q & b = f. [y,z] by CARD_3:def 6,A2; thus thesis by A2,A3; end; thus B c= A proof let a be set; assume a in B;then consider r being Element of FL such that A4: a = R. [x,y] "/\" r. [y,z] & r in Q; r. [y,z] in pi(Q,[y,z]) by CARD_3:def 6,A4; hence thesis by A4; end; end; hence thesis; end;then A1: for y being Element of X holds F(y) = G (y); thus {F(y) where y is Element of X:P[y]} = {G(y) where y is Element of X:P[y]} from FraenkelF'(A1); end; th26: for R being RMembership_Func of X,X, Q being Subset of FuzzyLattice [:X,X:], x,z being Element of X holds {"\/"({R. [x,y] "/\" r. [y,z] where y is Element of X:not contradiction} ,RealPoset [. 0,1 .]) where r is Element of FuzzyLattice [:X,X:]: r in Q} = {"\/"({R. [x,y] "/\" @(r'). [y,z] where y is Element of X:not contradiction} ,RealPoset [. 0,1 .]) where r' is Element of FuzzyLattice [:X,X:]: r' in Q} proof let R be RMembership_Func of X,X; let Q be Subset of FuzzyLattice [:X,X:]; let x,z be Element of X; set FL = FuzzyLattice [:X,X:]; defpred P[Element of FL] means $1 in Q; deffunc F(Element of FL) = "\/"({R. [x,y] "/\" $1. [y,z] where y is Element of X:not contradiction} ,RealPoset [. 0,1 .]); deffunc G(Element of FL) = "\/"({R. [x,y] "/\" @($1). [y,z] where y is Element of X:not contradiction} ,RealPoset [. 0,1 .]); for r being Element of FL st r in Q holds "\/"({R. [x,y] "/\" r. [y,z] where y is Element of X:not contradiction} ,RealPoset [. 0,1 .]) = "\/"({R. [x,y] "/\" @(r). [y,z] where y is Element of X:not contradiction} ,RealPoset [. 0,1 .]) proof let r be Element of FL; assume r in Q; {R. [x,y] "/\" r. [y,z] where y is Element of X:not contradiction} ={R. [x,y] "/\" @r. [y,z] where y is Element of X:not contradiction} proof defpred P[Element of X] means not contradiction; deffunc f(Element of X) = R. [x,$1] "/\" r. [$1,z]; deffunc g(Element of X) = R. [x,$1] "/\" @r. [$1,z]; A2: for y being Element of X holds f(y) = g(y) by LFUZZY_0:def 5; thus {f(y) where y is Element of X:P[y]} ={g(y) where y is Element of X:P[y]} from FraenkelF'(A2); end; hence thesis; end; then A1: for r being Element of FL st P[r] holds F(r) = G(r); thus {F(r) where r is Element of FuzzyLattice [:X,X:]: P[r] } = {G(r) where r is Element of FuzzyLattice [:X,X:]: P[r]} from FraenkelF'R(A1); end; th27: for R being RMembership_Func of X,X, Q being Subset of FuzzyLattice [:X,X:], x,z being Element of X holds {"\/"({R. [x,y] "/\" @(r). [y,z] where y is Element of X:not contradiction} ,RealPoset [. 0,1 .]) where r is Element of FuzzyLattice [:X,X:]: r in Q} = {(R(#)@r). [x,z] where r is Element of FuzzyLattice [:X,X:]: r in Q} proof let R be RMembership_Func of X,X; let Q be Subset of FuzzyLattice [:X,X:]; let x,z be Element of X; set FL = FuzzyLattice [:X,X:]; defpred P[Element of FL] means $1 in Q; deffunc F(Element of FL) = "\/"({R. [x,y] "/\" @($1). [y,z] where y is Element of X:not contradiction} ,RealPoset [. 0,1 .]); deffunc G(Element of FL) = (R (#) @($1)). [x,z]; A1: for r being Element of FL st P[r] holds F(r) = G(r) by LFUZZY_0:22; thus {F(r) where r is Element of FuzzyLattice [:X,X:]:P[r]} = {G(r) where r is Element of FuzzyLattice [:X,X:]: P[r]} from FraenkelF'R(A1); end; th28: for R being RMembership_Func of X,X, Q being Subset of FuzzyLattice [:X,X:], x,z being Element of X holds {(R(#)@r). [x,z] where r is Element of FuzzyLattice [:X,X:]: r in Q} = pi({(R(#)@r) where r is Element of FuzzyLattice [:X,X:]: r in Q}, [x,z]) proof let R be RMembership_Func of X,X; let Q be Subset of FuzzyLattice [:X,X:]; let x,z be Element of X; set FL = FuzzyLattice [:X,X:], A= {(R(#)@r). [x,z] where r is Element of FuzzyLattice [:X,X:]: r in Q}, B= pi({(R(#)@r) where r is Element of FL: r in Q}, [x,z]); thus A c= B proof let a be set; assume a in A;then consider r being Element of FL such that A1: a = (R(#)@r). [x,z] & r in Q; (R(#)@r) in {(R(#)@r') where r' is Element of FL: r' in Q} by A1; hence thesis by CARD_3:def 6,A1; end; thus B c= A proof let b be set; assume b in B;then consider f be Function such that A2: f in {(R(#)@r') where r' is Element of FL: r' in Q} & b = f. [x,z] by CARD_3:def 6; consider r being Element of FL such that A3: f = R (#) @r & r in Q by A2; thus b in A by A2,A3; end; end; th29: for R being RMembership_Func of X,X, Q being Subset of FuzzyLattice [:X,X:], x,z being Element of X holds "\/"({"\/"({R. [x,y] "/\" r. [y,z] where r is Element of FuzzyLattice [:X,X:]: r in Q} ,RealPoset [. 0,1 .]) where y is Element of X:not contradiction},RealPoset [. 0,1 .]) = "\/"({"\/"({R. [x,y] "/\" r'. [y,z] where y is Element of X:not contradiction} ,RealPoset [. 0,1 .]) where r' is Element of FuzzyLattice [:X,X:]: r' in Q},RealPoset [. 0,1 .]) proof let R be RMembership_Func of X,X; let Q be Subset of FuzzyLattice [:X,X:]; let x,z be Element of X; set FL = FuzzyLattice [:X,X:], RP = RealPoset [. 0,1 .]; defpred P[Element of X] means not contradiction; defpred Q[Element of FuzzyLattice [:X,X:]] means $1 in Q; deffunc F1(Element of X,Element of FuzzyLattice [:X,X:]) = R. [x,$1] "/\" $2. [$1,z]; deffunc F2(Element of X,Element of FuzzyLattice [:X,X:]) = R. [x,$1] "/\" $2. [$1,z]; A1: for y being Element of X, r being Element of FL st P[y] & Q[r] holds F1(y,r) = F2(y,r); thus "\/"({ "\/"({F1(y,r) where r is Element of FL: Q[r]}, RP) where y is Element of X: P[y] }, RP) = "\/"({ "\/"({F2(y',r') where y' is Element of X: P[y']}, RP) where r' is Element of FL: Q[r'] }, RP) from SupCommutativity(A1); end; theorem th30: for R being RMembership_Func of X,X, Q being Subset of FuzzyLattice [:X,X:] holds R (#) @("\/"(Q,FuzzyLattice [:X,X:])) = "\/"({R (#) @r where r is Element of FuzzyLattice [:X,X:]:r in Q}, FuzzyLattice [:X,X:]) proof let R be RMembership_Func of X,X; let Q be Subset of FuzzyLattice [:X,X:]; set FL = FuzzyLattice [:X,X:], RP = RealPoset [. 0,1 .]; ("\/"({R (#) @r where r is Element of FL:r in Q},FL)) = @("\/"({R (#) @r where r is Element of FL:r in Q},FL)) by LFUZZY_0:def 5;then reconsider F = ("\/"({R (#) @r where r is Element of FL:r in Q},FL)) as RMembership_Func of X,X; for x,z being Element of X holds (R (#) @("\/"(Q,FL))). [x,z] = F. [x,z] proof let x,z be Element of X; AA: {(R(#)@r) where r is Element of FL: r in Q} c= the carrier of FuzzyLattice [:X,X:] proof let t be set; assume t in {(R(#)@r) where r is Element of FL: r in Q};then consider r being Element of FuzzyLattice [:X,X:] such that A4: t = (R(#)@r) & r in Q; ([:X,X:],(R(#)@r))@ = (R(#)@r) by LFUZZY_0:def 6; hence t in the carrier of FuzzyLattice [:X,X:] by A4; end; thus (R (#) @("\/"(Q,FL))). [x,z] = "\/"({R. [x,y] "/\" (@("\/"(Q,FL))). [y,z] where y is Element of X: not contradiction},RP) by LFUZZY_0:22 .= "\/"({R. [x,y] "/\" "\/"(pi(Q, [y,z]), RP) where y is Element of X: not contradiction},RP) by th23 .= "\/"( {"\/"({R. [x,y] "/\" b where b is Element of RP:b in pi(Q,[y,z])} ,RP) where y is Element of X:not contradiction},RP) by th24 .= "\/"( {"\/"({R. [x,y] "/\" r. [y,z] where r is Element of FL: r in Q} ,RP) where y is Element of X:not contradiction},RP) by th25 .= "\/"( {"\/"({R. [x,y] "/\" r. [y,z] where y is Element of X:not contradiction} ,RP) where r is Element of FL: r in Q},RP) by th29 .= "\/"( {"\/"({R. [x,y] "/\" @r. [y,z] where y is Element of X:not contradiction} ,RP) where r is Element of FL: r in Q},RP) by th26 .= "\/"({(R(#)@r). [x,z] where r is Element of FL: r in Q},RP) by th27 .= "\/"(pi({(R(#)@r) where r is Element of FL: r in Q}, [x,z]),RP) by th28 .= F. [x,z] by th22,AA; end; hence thesis by Th1; end; theorem th31: for R being RMembership_Func of X,X, Q being Subset of FuzzyLattice [:X,X:] holds @("\/"(Q,FuzzyLattice [:X,X:])) (#) R = "\/"({@r (#) R where r is Element of FuzzyLattice [:X,X:]:r in Q}, FuzzyLattice [:X,X:]) proof let R be RMembership_Func of X,X; let Q be Subset of FuzzyLattice [:X,X:]; set FL = FuzzyLattice [:X,X:], RP = RealPoset [. 0,1 .]; ("\/"({@r (#) R where r is Element of FL:r in Q},FL)) = @("\/"({@r (#) R where r is Element of FL:r in Q},FL)) by LFUZZY_0:def 5;then reconsider F = ("\/"({@r (#) R where r is Element of FL:r in Q},FL)) as RMembership_Func of X,X; for x,z being Element of X holds (@("\/"(Q,FL)) (#) R). [x,z] = F. [x,z] proof let x,z be Element of X; ZZ: {(@r(#)R) where r is Element of FL: r in Q} c= the carrier of FuzzyLattice [:X,X:] proof let t be set; assume t in {(@r(#)R) where r is Element of FL: r in Q};then consider r being Element of FuzzyLattice [:X,X:] such that A4: t = (@r(#)R) & r in Q; ([:X,X:],(@r(#)R))@ = (@r(#)R) by LFUZZY_0:def 6; hence t in the carrier of FuzzyLattice [:X,X:] by A4; end; B1: {(@("\/"(Q,FL))). [x,y] "/\" R. [y,z] where y is Element of X: not contradiction} = {"\/"(pi(Q, [x,y]), RP) "/\" R. [y,z] where y is Element of X: not contradiction} proof defpred P[Element of X] means not contradiction; deffunc F(Element of X) = (@("\/"(Q,FL))). [x,$1] "/\" R. [$1,z]; deffunc G(Element of X) = "\/"(pi(Q, [x,$1]), RP) "/\" R. [$1,z]; for y being Element of X holds (@("\/"(Q,FuzzyLattice [:X,X:]))). [x,y] "/\" R. [y,z] = "\/"(pi(Q, [x,y]), RealPoset [. 0,1 .]) "/\" R. [y,z] proof let y be Element of X; (@("\/"(Q,FuzzyLattice [:X,X:]))). [x,y] = (("\/"(Q,FuzzyLattice [:X,X:]))). [x,y] by LFUZZY_0:def 5 .= "\/"(pi(Q, [x,y]), RealPoset [. 0,1 .]) by th22; hence thesis; end; then B11: for y being Element of X holds F(y) = G(y); thus {F(y) where y is Element of X: P[y]} = {G(y') where y' is Element of X: P[y']} from FraenkelF'(B11); end; B2: {"\/"(pi(Q, [x,y]), RP) "/\" R. [y,z] where y is Element of X:not contradiction} = {"\/"({b "/\" R. [y',z] where b is Element of RP:b in pi(Q,[x,y])} ,RP) where y' is Element of X:not contradiction} proof defpred P[Element of X] means not contradiction; deffunc F(Element of X) = "\/"(pi(Q, [x,$1]),RP) "/\" R. [$1,z]; deffunc G(Element of X) = "\/"({b "/\" R. [$1,z] where b is Element of RP: b in pi(Q,[x,$1])} ,RP); for y being Element of X holds "\/"(pi(Q, [x,y]), RealPoset [. 0,1 .]) "/\" R. [y,z] = "\/"({b "/\" R. [y,z] where b is Element of RP:b in pi(Q,[x,y])} ,RP) proof let y be Element of X; B21: FuzzyLattice [:X,X:] = (RealPoset [. 0,1 .]) |^ [:X,X:] by LFUZZY_0:def 4 .= product ([:X,X:] --> RealPoset [. 0,1 .]) by YELLOW_1:def 5; reconsider Q as Subset of product ([:X,X:] --> RealPoset [. 0,1 .]) by B21; pi(Q, [x,y]) is Subset of RealPoset [. 0,1 .] by FUNCOP_1:13; hence thesis by LFUZZY_0:15; end; then B22: for y being Element of X holds F(y) = G (y); {F(y) where y is Element of X:P[y]} = {G(y') where y' is Element of X:P[y']} from FraenkelF'(B22); hence thesis; end; B3: {"\/"({b "/\" R. [y,z] where b is Element of RP:b in pi(Q,[x,y])} ,RP) where y is Element of X:not contradiction} = {"\/"({r. [x,y'] "/\" R. [y',z] where r is Element of FL: r in Q} ,RP) where y' is Element of X:not contradiction} proof defpred P[Element of X] means not contradiction; deffunc F(Element of X) = "\/"({b "/\" R. [$1,z] where b is Element of RP: b in pi(Q,[x,$1])} ,RP); deffunc G(Element of X) = "\/"({r. [x,$1] "/\" R. [$1,z] where r is Element of FL: r in Q} ,RP); for y being Element of X holds "\/"({b "/\" R. [y,z] where b is Element of RP: b in pi(Q,[x,y])} ,RP) = "\/"({r. [x,y] "/\" R. [y,z] where r is Element of FL: r in Q} ,RP) proof let y be Element of X; set A = {b "/\" R. [y,z] where b is Element of RP: b in pi(Q,[x,y])}, B = {r. [x,y] "/\" R. [y,z] where r is Element of FL: r in Q}; A = B proof thus A c= B proof let a be set; assume a in A;then consider b be Element of RP such that B3A2: a = b "/\" R. [y,z] & b in pi(Q,[x,y]); consider f be Function such that B3A3: f in Q & b = f. [x,y] by CARD_3:def 6,B3A2; thus thesis by B3A2,B3A3; end; thus B c= A proof let a be set; assume a in B;then consider r being Element of FL such that A4: a = r. [x,y] "/\" R. [y,z] & r in Q; r. [x,y] in pi(Q,[x,y]) by CARD_3:def 6,A4; hence thesis by A4; end; end; hence thesis; end;then A1: for y being Element of X holds F(y) = G (y); thus {F(y) where y is Element of X:P[y]} = {G(y) where y is Element of X:P[y]} from FraenkelF'(A1); end; B4: "\/"({"\/"({r. [x,y] "/\" R. [y,z] where r is Element of FL: r in Q} ,RP) where y is Element of X:not contradiction},RP) = "\/"({"\/"({r'. [x,y] "/\" R. [y,z] where y is Element of X:not contradiction} ,RP) where r' is Element of FL: r' in Q},RP) proof defpred P[Element of X] means not contradiction; defpred Q[Element of FuzzyLattice [:X,X:]] means $1 in Q; deffunc F1(Element of X,Element of FuzzyLattice [:X,X:]) = $2. [x,$1] "/\" R. [$1,z]; deffunc F2(Element of X,Element of FuzzyLattice [:X,X:]) = $2. [x,$1] "/\" R. [$1,z]; A1: for y being Element of X, r being Element of FL st P[y] & Q[r] holds F1(y,r) = F2(y,r); thus "\/"({ "\/"({F1(y,r) where r is Element of FL: Q[r]}, RP) where y is Element of X: P[y] }, RP) = "\/"({ "\/"({F2(y',r') where y' is Element of X: P[y']}, RP) where r' is Element of FL: Q[r'] }, RP) from SupCommutativity(A1); end; B5: {"\/"({r. [x,y] "/\" R. [y,z] where y is Element of X:not contradiction} ,RP) where r is Element of FL: r in Q} = {"\/"({@r'. [x,y] "/\" R. [y,z] where y is Element of X:not contradiction} ,RP) where r' is Element of FL: r' in Q} proof defpred P[Element of FL] means $1 in Q; deffunc F(Element of FL) = "\/"({$1. [x,y] "/\" R. [y,z] where y is Element of X:not contradiction} ,RealPoset [. 0,1 .]); deffunc G(Element of FL) = "\/"({@($1). [x,y] "/\" R. [y,z] where y is Element of X:not contradiction} ,RealPoset [. 0,1 .]); for r being Element of FL st r in Q holds "\/"({r. [x,y] "/\" R. [y,z] where y is Element of X:not contradiction} ,RealPoset [. 0,1 .]) = "\/"({@r. [x,y] "/\" R. [y,z] where y is Element of X:not contradiction} ,RealPoset [. 0,1 .]) proof let r be Element of FL; assume r in Q; {r. [x,y] "/\" R. [y,z] where y is Element of X:not contradiction} ={@r. [x,y] "/\" R. [y,z] where y is Element of X:not contradiction} proof defpred P[Element of X] means not contradiction; deffunc f(Element of X) = r. [x,$1] "/\" R. [$1,z]; deffunc g(Element of X) = @r. [x,$1] "/\" R. [$1,z]; A2: for y being Element of X holds f(y) = g(y) by LFUZZY_0:def 5; thus {f(y) where y is Element of X:P[y]} ={g(y) where y is Element of X:P[y]} from FraenkelF'(A2); end; hence thesis; end; then A1: for r being Element of FL st P[r] holds F(r) = G(r); thus {F(r) where r is Element of FuzzyLattice [:X,X:]: P[r] } = {G(r) where r is Element of FuzzyLattice [:X,X:]: P[r]} from FraenkelF'R(A1); end; B6: {"\/"({@r. [x,y] "/\" R. [y,z] where y is Element of X:not contradiction} ,RP) where r is Element of FL: r in Q} = {(@r'(#)R). [x,z] where r' is Element of FL: r' in Q} proof defpred P[Element of FL] means $1 in Q; deffunc F(Element of FL) = "\/"({@($1). [x,y] "/\" R. [y,z] where y is Element of X:not contradiction} ,RealPoset [. 0,1 .]); deffunc G(Element of FL) = (@($1)(#)R). [x,z]; A1: for r being Element of FL st P[r] holds F(r) = G(r) by LFUZZY_0:22; thus {F(r) where r is Element of FuzzyLattice [:X,X:]:P[r]} = {G(r) where r is Element of FuzzyLattice [:X,X:]: P[r]} from FraenkelF'R(A1); end; B7: {(@r(#)R). [x,z] where r is Element of FL: r in Q} = pi({(@r(#)R) where r is Element of FL: r in Q}, [x,z]) proof set A= {(@r(#)R). [x,z] where r is Element of FL: r in Q}, B= pi({(@r(#)R) where r is Element of FL: r in Q}, [x,z]); thus A c= B proof let a be set; assume a in A;then consider r being Element of FL such that A1: a = (@r(#)R). [x,z] & r in Q; (@r(#)R) in {(@r'(#)R) where r' is Element of FL: r' in Q} by A1; hence thesis by CARD_3:def 6,A1; end; thus B c= A proof let b be set; assume b in B;then consider f be Function such that A2: f in {(@r'(#)R) where r' is Element of FL: r' in Q} & b = f. [x,z] by CARD_3:def 6; consider r being Element of FL such that A3: f = (@r(#)R) & r in Q by A2; thus b in A by A2,A3; end; end; thus (@("\/"(Q,FL)) (#) R). [x,z] = "\/"({(@("\/"(Q,FL))). [x,y] "/\" R. [y,z] where y is Element of X: not contradiction},RP) by LFUZZY_0:22 .= F. [x,z] by B1,B2,B3,B4,B5,B6,B7,th22,ZZ; end; hence thesis by Th1; end; theorem th32: for R being RMembership_Func of X,X holds (TrCl R)(#)(TrCl R) = "\/"({(i iter R) (#) (j iter R) where i is Nat, j is Nat:i > 0 & j > 0},FuzzyLattice [:X,X:]) proof let R be RMembership_Func of X,X; set Q = {n iter R where n is Nat : n > 0}, FL = FuzzyLattice [:X,X:]; A1: "\/"(Q,FL) = @"\/"(Q,FL) by LFUZZY_0:def 5; AA: Q c= the carrier of FL proof let q be set; assume q in Q; then consider i being Nat such that A4: q = (i iter R) & i > 0; ([:X,X:],(i iter R) )@ = i iter R by LFUZZY_0:def 6; hence q in the carrier of FuzzyLattice [:X,X:] by A4; end; A3: {@r (#) (TrCl R) where r is Element of FL:r in Q} = {"\/"({@r' (#) @s where s is Element of FL:s in Q},FL) where r' is Element of FL : r' in Q} proof set A = {@r (#) (TrCl R) where r is Element of FL:r in Q}, B = {"\/"({@r' (#) @s where s is Element of FL:s in Q},FL) where r' is Element of FL : r' in Q}; thus A c= B proof let a be set; assume a in A; then consider r being Element of FL such that A31: a = @r (#) (TrCl R) & r in Q; a = @r (#) @"\/"(Q,FL) by A1,Def12,A31 .= "\/"({@r (#) @s where s is Element of FL:s in Q},FL) by AA,th30; hence thesis by A31; end; thus B c= A proof let a be set; assume a in B; then consider r being Element of FL such that A32: a = "\/"({@r (#) @s where s is Element of FL:s in Q},FL) & r in Q; a = @r (#) @"\/"(Q,FL) by AA,th30,A32 .= @r (#) (TrCl R) by A1,Def12; hence thesis by A32; end; end; A5: {@r (#) @s where r is Element of FL,s is Element of FL:r in Q & s in Q} = {(i iter R) (#) (j iter R) where i is Nat, j is Nat:i > 0 & j > 0} proof set A = {@r (#) @s where r is Element of FL,s is Element of FL:r in Q & s in Q}, B = {(i iter R) (#) (j iter R) where i is Nat, j is Nat:i > 0 & j > 0}; thus A c= B proof let a be set; assume a in A; then consider r,s being Element of FL such that A51: a = @r (#) @s & r in Q & s in Q; consider i being Nat such that A52: r = i iter R & i > 0 by A51; consider j being Nat such that A53: s = j iter R & j > 0 by A51; A54: r = @r & s = @s by LFUZZY_0:def 5; thus thesis by A51,A54,A52,A53; end; thus B c= A proof let b be set; assume b in B; then consider i,j being Nat such that A55: b = (i iter R) (#) (j iter R) & i > 0 & j > 0; A56: (i iter R) in Q & (j iter R) in Q by A55; A57: (i iter R) = ([:X,X:],(i iter R))@ & (j iter R) = ([:X,X:],(j iter R))@ by LFUZZY_0:def 6; reconsider r = i iter R as Element of FL by A57; reconsider s = j iter R as Element of FL by A57; @r = r & @s = s by LFUZZY_0:def 5; hence thesis by A56,A55; end; end; deffunc f(Element of FL,Element of FL) = ([:X,X:],@$1 (#) @$2)@; defpred P[Element of FL] means $1 in Q; defpred R[Element of FL] means $1 in Q; A6: {"\/"({@r (#) @s where s is Element of FL : s in Q},FL) where r is Element of FL : r in Q} = {"\/"({([:X,X:],@r' (#) @s')@ where s' is Element of FL : s' in Q},FL) where r' is Element of FL : r' in Q} proof defpred P[Element of FL] means $1 in Q; deffunc F(Element of FL) = "\/"({@$1 (#) @s where s is Element of FL : s in Q},FL); deffunc G(Element of FL) = "\/"({([:X,X:],@$1 (#) @s)@ where s is Element of FL : s in Q},FL); for r being Element of FL holds "\/"({@r (#) @s where s is Element of FL : s in Q},FL) = "\/"({([:X,X:],@r (#) @s)@ where s is Element of FL : s in Q},FL) proof let r be Element of FL; {@r (#) @s where s is Element of FL : s in Q} = {([:X,X:],@r (#) @s)@ where s is Element of FL : s in Q} proof defpred P[Element of FL] means $1 in Q; deffunc f(Element of FL) = @r (#) @$1; deffunc g(Element of FL) = ([:X,X:],@r (#) @$1)@; A62: for s being Element of FL holds f(s) = g(s) by LFUZZY_0:def 6; {f(s) where s is Element of FL : P[s]} = {g(s) where s is Element of FL : P[s]} from FraenkelF'(A62); hence thesis; end; hence thesis; end;then A61: for r being Element of FL holds F(r) = G(r); {F(r) where r is Element of FL : P[r]} = {G(r) where r is Element of FL : P[r]} from FraenkelF'(A61); hence thesis; end; A7: {([:X,X:],@r (#) @s)@ where r is Element of FL, s is Element of FL:r in Q & s in Q} = {@r (#) @s where r is Element of FL, s is Element of FL:r in Q & s in Q} proof defpred P[Element of FL,Element of FL] means $1 in Q & $2 in Q; deffunc F(Element of FL,Element of FL) = ([:X,X:],@$1 (#) @$2)@; deffunc G(Element of FL,Element of FL) = @$1 (#) @$2; A71: for r being Element of FL, s being Element of FL holds F(r,s) = G(r,s) by LFUZZY_0:def 6; {F(r,s) where r is Element of FL,s is Element of FL:P[r,s]} ={G(r,s) where r is Element of FL,s is Element of FL:P[r,s]} from FraenkelF''(A71); hence thesis; end; thus (TrCl R)(#)(TrCl R) = @"\/"(Q,FL) (#) (TrCl R) by A1,Def12 .= "\/"({"\/"({f(r,s) where s is Element of FL:R[s]},FL) where r is Element of FL :P[r]},FL) by A6,A3,AA,th31 .= "\/"({f(r,s) where r is Element of FL, s is Element of FL: P[r] & R[s]},FL) from SupDistributivity .= "\/"({(i iter R) (#) (j iter R) where i is Nat, j is Nat: i > 0 & j > 0},FL) by A5,A7; end; definition let X be non empty set; let R be RMembership_Func of X,X; cluster TrCl R -> transitive; coherence proof set FL = FuzzyLattice [:X,X:], RP = RealPoset [. 0,1 .], A = {(i iter R) (#) (j iter R) where i is Nat, j is 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:]; AA: A c= the carrier of FuzzyLattice [:X,X:] proof let t be set; assume t in A;then consider i,j being Nat such that A4: t = (i iter R) (#) (j iter R) & i > 0 & 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 A4; end; B2: ((TrCl R)(#)(TrCl R)).c = "\/"(A,FL).c by th32 .= "\/"(pi(A,c),RP) by AA,th22; (TrCl R).c is_>=_than pi(A,c) proof for b being Element of RP st b in pi(A,c) holds b <<= (TrCl R).c proof let b be Element of RP; assume b in pi(A,c);then consider f be Function such that C1: f in A & b = f.c by CARD_3:def 6; consider i,j being Nat such that C2: f = (i iter R) (#) (j iter R) & i > 0 & j > 0 by C1; C3: i+j > 0 by ANALOAF:2,C2; C4: f = (i+j) iter R by C2,th19; reconsider f as RMembership_Func of X,X by C2; f c= TrCl R by th33,C3,C4;then f.c <= (TrCl R).c by Def1; hence thesis by C1,LFUZZY_0:3; end; hence thesis by LATTICE3:def 9; end; then "\/"(pi(A,c),RP) <<= (TrCl R).c by YELLOW_0:32; hence thesis by B2,LFUZZY_0:3; end; then (TrCl R)(#)(TrCl R) c= (TrCl R) by Def1; hence thesis by Def7; end; end; theorem th36: for R being RMembership_Func of X,X, n being natural number st R is transitive & n > 0 holds n iter R c= R proof let R be RMembership_Func of X,X; let n be natural number; assume A1: R is transitive & n > 0; then A6: R (#) R c= R by Def7; defpred P[Nat] means $1 iter R c= R; reconsider n as non empty Nat by A1,ORDINAL2:def 21; 1 iter R = R by th20;then A2: P[1] by FUZZY14; A3: for k being non empty Nat st P[k] holds P[k+1] proof let k be non empty Nat; assume A4: P[k]; R c= R by FUZZY14;then k iter R (#) R c= R(#)R by A4,FUZZY430;then (k+1) iter R c= R(#)R by th17; hence thesis by A6,FUZZY15; end; for k being non empty Nat holds P[k] from Ind_from_1(A2,A3); then P[n]; hence thesis; end; theorem th34: for R being RMembership_Func of X,X st R is transitive holds R = TrCl R proof let R be RMembership_Func of X,X; assume A0: R is transitive; A1: R c= TrCl R by th35; TrCl R c= R proof for c being Element of [:X,X:] holds (TrCl R).c <= R.c proof let c be Element of [:X,X:]; set Q = {n iter R where n is Nat : n > 0}, FL = FuzzyLattice [:X,X:], RP = RealPoset [. 0,1 .]; AS: Q c= the carrier of FuzzyLattice [:X,X:] proof let t be set; assume t in Q;then consider i being Nat such that A4: t = (i iter R) & 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 A4; end; A5: (TrCl R).c = "\/"(Q,FL).c by Def12 .= "\/"(pi(Q,c),RP) by AS,th22; for b being Element of RP st b in pi(Q,c) holds b <<= R.c proof let b be Element of RP; assume b in pi(Q,c); then consider f being Function such that A2: f in Q & b = f.c by CARD_3:def 6; consider n be Nat such that A3: f = n iter R & n>0 by A2; n iter R c= R by A0,A3,th36;then (n iter R).c <= R.c by Def1; hence thesis by LFUZZY_0:3,A2,A3; end;then R.c is_>=_than pi(Q,c) by LATTICE3:def 9;then (TrCl R).c <<= R.c by YELLOW_0:32,A5; hence thesis by LFUZZY_0:3; end; hence thesis by Def1; end; hence thesis by FUZZY13,A1; end; theorem th36: for R,S being RMembership_Func of X,X, n being natural number st R c= S holds n iter R c= n iter S proof let R,S be RMembership_Func of X,X; let n be natural number; assume A0: R c= S; defpred P[natural number] means $1 iter R c= $1 iter S; 0 iter R = Imf(X,X) by th18 .= 0 iter S by th18;then A1: P[0] by FUZZY13; A3: for k being natural number st P[k] holds P[k+1] proof let k be natural number; assume AA: P[k]; (k iter R) (#) R = (k+1) iter R & (k iter S) (#) S = (k+1) iter S by th17; hence thesis by AA,FUZZY430,A0; end; for k being natural number holds P[k] from Nat_Ind(A1,A3); hence thesis; end; theorem for R,S being RMembership_Func of X,X st S is transitive & R c= S holds TrCl R c= S proof let R,S be RMembership_Func of X,X; assume A0: S is transitive & R c= S; TrCl R c= TrCl S proof for c being Element of [:X,X:] holds (TrCl R).c <= (TrCl S).c proof let c be Element of [:X,X:]; set Q = {n iter R where n is Nat : n > 0}, FL = FuzzyLattice [:X,X:], RP = RealPoset [. 0,1 .]; AS: Q c= the carrier of FuzzyLattice [:X,X:] proof let t be set; assume t in Q;then consider i being Nat such that A4: t = (i iter R) & 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 A4; end; A1: (TrCl R).c = "\/"(Q,FL).c by Def12 .= "\/"(pi(Q,c),RP) by AS,th22; (TrCl S).c is_>=_than pi(Q,c) proof for b being Element of RP st b in pi(Q,c) holds b <<= (TrCl S).c proof let b be Element of RP; assume b in pi(Q,c);then consider f being Function such that A2: f in Q & b = f.c by CARD_3:def 6; consider n be Nat such that A3: f = n iter R & n>0 by A2; n iter R c= n iter S & n iter S c= TrCl S by A0,th36,th33,A3; then n iter R c= TrCl S by FUZZY15; then (n iter R).c <= (TrCl S).c by Def1; hence thesis by LFUZZY_0:3,A3,A2; end; hence thesis by LATTICE3:def 9; end; then "\/"(pi(Q,c),RP) <<= (TrCl S).c by YELLOW_0:32; hence thesis by LFUZZY_0:3,A1; end; hence thesis by Def1; end; hence thesis by th34,A0; end;

Back to top