:: LFUZZY_1 semantic presentation begin registration let X be non empty set ; cluster[.0,1.] -valued Function-like quasi_total -> real-valued for Element of bool [:X,REAL:]; coherence for b1 being Membership_Func of X holds b1 is real-valued ; end; definition let X, Y be non empty set ; let f, g be RMembership_Func of X,Y; :: original: is_less_than redefine predf is_less_than g means :Def1: :: LFUZZY_1:def 1 for x being Element of X for y being Element of Y holds f . (x,y) <= g . (x,y); compatibility ( f is_less_than g iff for x being Element of X for y being Element of Y holds f . (x,y) <= g . (x,y) ) proof thus ( f is_less_than g iff for x being Element of X for y being Element of Y holds f . (x,y) <= g . (x,y) ) ::_thesis: verum proof hereby ::_thesis: ( ( for x being Element of X for y being Element of Y holds f . (x,y) <= g . (x,y) ) implies f is_less_than g ) assume A1: f is_less_than g ; ::_thesis: for x being Element of X for y being Element of Y holds f . (x,y) <= g . (x,y) thus for x being Element of X for y being Element of Y holds f . (x,y) <= g . (x,y) ::_thesis: verum proof let x be Element of X; ::_thesis: for y being Element of Y holds f . (x,y) <= g . (x,y) let y be Element of Y; ::_thesis: f . (x,y) <= g . (x,y) ( dom f = [:X,Y:] & [x,y] in [:X,Y:] ) by FUNCT_2:def_1; hence f . (x,y) <= g . (x,y) by A1, FUZZY_1:def_1; ::_thesis: verum end; end; assume A2: for x being Element of X for y being Element of Y holds f . (x,y) <= g . (x,y) ; ::_thesis: f is_less_than g A3: for c being set st c in dom f holds f . c <= g . c proof let c be set ; ::_thesis: ( c in dom f implies f . c <= g . c ) assume A4: c in dom f ; ::_thesis: f . c <= g . c then consider x, y being set such that A5: [x,y] = c by RELAT_1:def_1; reconsider y = y as Element of Y by A4, A5, ZFMISC_1:87; reconsider x = x as Element of X by A4, A5, ZFMISC_1:87; f . (x,y) <= g . (x,y) by A2; hence f . c <= g . c by A5; ::_thesis: verum end; dom g = [:X,Y:] by FUNCT_2:def_1; hence f is_less_than g by A3, FUZZY_1:def_1; ::_thesis: verum end; end; end; :: deftheorem Def1 defines is_less_than LFUZZY_1:def_1_:_ for X, Y being non empty set for f, g being RMembership_Func of X,Y holds ( f is_less_than g iff for x being Element of X for y being Element of Y holds f . (x,y) <= g . (x,y) ); theorem Th1: :: LFUZZY_1:1 for X being non empty set 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 X be non empty set ; ::_thesis: for R, S being Membership_Func of X st ( for x being Element of X holds R . x = S . x ) holds R = S let R, S be Membership_Func of X; ::_thesis: ( ( for x being Element of X holds R . x = S . x ) implies R = S ) assume for x being Element of X holds R . x = S . x ; ::_thesis: R = S then A1: for x being Element of X st x in dom R holds R . x = S . x ; ( dom R = X & dom S = X ) by FUNCT_2:def_1; hence R = S by A1, PARTFUN1:5; ::_thesis: verum end; theorem Th2: :: LFUZZY_1:2 for X, Y being non empty set for R, S being RMembership_Func of X,Y st ( for x being Element of X for y being Element of Y holds R . (x,y) = S . (x,y) ) holds R = S proof let X, Y be non empty set ; ::_thesis: for R, S being RMembership_Func of X,Y st ( for x being Element of X for y being Element of Y holds R . (x,y) = S . (x,y) ) holds R = S let R, S be RMembership_Func of X,Y; ::_thesis: ( ( for x being Element of X for y being Element of Y holds R . (x,y) = S . (x,y) ) implies R = S ) assume A1: for x being Element of X for y being Element of Y holds R . (x,y) = S . (x,y) ; ::_thesis: R = S A2: for x, y being set st [x,y] in dom R holds R . (x,y) = S . (x,y) proof let x, y be set ; ::_thesis: ( [x,y] in dom R implies R . (x,y) = S . (x,y) ) assume A3: [x,y] in dom R ; ::_thesis: R . (x,y) = S . (x,y) then reconsider x = x as Element of X by ZFMISC_1:87; reconsider y = y as Element of Y by A3, ZFMISC_1:87; R . (x,y) = S . (x,y) by A1; hence R . (x,y) = S . (x,y) ; ::_thesis: verum end; ( dom R = [:X,Y:] & dom S = [:X,Y:] ) by FUNCT_2:def_1; hence R = S by A2, BINOP_1:20; ::_thesis: verum end; theorem Th3: :: LFUZZY_1:3 for X being non empty set for R, S being Membership_Func of X holds ( R = S iff ( S c= & R c= ) ) proof let X be non empty set ; ::_thesis: for R, S being Membership_Func of X holds ( R = S iff ( S c= & R c= ) ) let R, S be Membership_Func of X; ::_thesis: ( R = S iff ( S c= & R c= ) ) thus ( R = S implies ( S c= & R c= ) ) ; ::_thesis: ( S c= & R c= implies R = S ) assume A1: ( S c= & R c= ) ; ::_thesis: R = S for x being Element of X holds R . x = S . x proof let x be Element of X; ::_thesis: R . x = S . x ( R . x <= S . x & S . x <= R . x ) by A1, FUZZY_1:def_2; hence R . x = S . x by XXREAL_0:1; ::_thesis: verum end; hence R = S by Th1; ::_thesis: verum end; theorem :: LFUZZY_1:4 for X being non empty set for R being Membership_Func of X holds R c= ; theorem Th5: :: LFUZZY_1:5 for X being non empty set for R, S, T being Membership_Func of X st S c= & T c= holds T c= proof let X be non empty set ; ::_thesis: for R, S, T being Membership_Func of X st S c= & T c= holds T c= let R, S, T be Membership_Func of X; ::_thesis: ( S c= & T c= implies T c= ) assume A1: ( S c= & T c= ) ; ::_thesis: T c= for x being Element of X holds R . x <= T . x proof let x be Element of X; ::_thesis: R . x <= T . x ( R . x <= S . x & S . x <= T . x ) by A1, FUZZY_1:def_2; hence R . x <= T . x by XXREAL_0:2; ::_thesis: verum end; hence T c= by FUZZY_1:def_2; ::_thesis: verum end; theorem Th6: :: LFUZZY_1:6 for X, Y, Z being non empty set for R, S being RMembership_Func of X,Y for T, U being RMembership_Func of Y,Z st S c= & U c= holds S (#) U c= proof let X, Y, Z be non empty set ; ::_thesis: for R, S being RMembership_Func of X,Y for T, U being RMembership_Func of Y,Z st S c= & U c= holds S (#) U c= let R, S be RMembership_Func of X,Y; ::_thesis: for T, U being RMembership_Func of Y,Z st S c= & U c= holds S (#) U c= let T, U be RMembership_Func of Y,Z; ::_thesis: ( S c= & U c= implies S (#) U c= ) assume A1: ( S c= & U c= ) ; ::_thesis: S (#) U c= for c being Element of [:X,Z:] holds (R (#) T) . c <= (S (#) U) . c proof let c be Element of [:X,Z:]; ::_thesis: (R (#) T) . c <= (S (#) U) . c consider x, z being set such that A2: [x,z] = c by RELAT_1:def_1; A3: ( x in X & z in Z ) by A2, ZFMISC_1:87; for y being set st y in Y holds ( R . [x,y] <= S . [x,y] & T . [y,z] <= U . [y,z] ) proof let y be set ; ::_thesis: ( y in Y implies ( R . [x,y] <= S . [x,y] & T . [y,z] <= U . [y,z] ) ) assume y in Y ; ::_thesis: ( R . [x,y] <= S . [x,y] & T . [y,z] <= U . [y,z] ) then ( [x,y] in [:X,Y:] & [y,z] in [:Y,Z:] ) by A3, ZFMISC_1:87; hence ( R . [x,y] <= S . [x,y] & T . [y,z] <= U . [y,z] ) by A1, FUZZY_1:def_2; ::_thesis: verum end; hence (R (#) T) . c <= (S (#) U) . c by A2, A3, FUZZY_4:18; ::_thesis: verum end; hence S (#) U c= by FUZZY_1:def_2; ::_thesis: verum end; definition let X be non empty set ; let f, g be Membership_Func of X; :: original: min redefine func min (f,g) -> Element of bool [:X,REAL:]; commutativity for f, g being Membership_Func of X holds min (f,g) = min (g,f) ; :: original: max redefine func max (f,g) -> Element of bool [:X,REAL:]; commutativity for f, g being Membership_Func of X holds max (f,g) = max (g,f) ; end; theorem :: LFUZZY_1:7 for X being non empty set for f, g being Membership_Func of X holds f c= proof let X be non empty set ; ::_thesis: for f, g being Membership_Func of X holds f c= let f, g be Membership_Func of X; ::_thesis: f c= let x be Element of X; :: according to FUZZY_1:def_2 ::_thesis: (min (f,g)) . x <= f . x (min (f,g)) . x = min ((f . x),(g . x)) by FUZZY_1:def_3; hence (min (f,g)) . x <= f . x by XXREAL_0:17; ::_thesis: verum end; theorem :: LFUZZY_1:8 for X being non empty set for f, g being Membership_Func of X holds max (f,g) c= proof let X be non empty set ; ::_thesis: for f, g being Membership_Func of X holds max (f,g) c= let f, g be Membership_Func of X; ::_thesis: max (f,g) c= let x be Element of X; :: according to FUZZY_1:def_2 ::_thesis: f . x <= (max (f,g)) . x (max (f,g)) . x = max ((f . x),(g . x)) by FUZZY_1:def_4; hence f . x <= (max (f,g)) . x by XXREAL_0:25; ::_thesis: verum end; begin definition let X be non empty set ; let R be RMembership_Func of X,X; attrR is reflexive means :Def2: :: LFUZZY_1:def 2 R c= ; end; :: deftheorem Def2 defines reflexive LFUZZY_1:def_2_:_ for X being non empty set for R being RMembership_Func of X,X holds ( R is reflexive iff R c= ); definition let X be non empty set ; let R be RMembership_Func of X,X; redefine attr R is reflexive means :Def3: :: LFUZZY_1:def 3 for x being Element of X holds R . (x,x) = 1; compatibility ( R is reflexive iff for x being Element of X holds R . (x,x) = 1 ) proof hereby ::_thesis: ( ( for x being Element of X holds R . (x,x) = 1 ) implies R is reflexive ) assume R is reflexive ; ::_thesis: for x being Element of X holds R . (x,x) = 1 then A1: R c= by Def2; thus for x being Element of X holds R . (x,x) = 1 ::_thesis: verum proof let x be Element of X; ::_thesis: R . (x,x) = 1 (Imf (X,X)) . (x,x) <= R . (x,x) by A1, Def1; then ( R . (x,x) <= 1 & R . (x,x) >= 1 ) by FUZZY_4:4, FUZZY_4:25; hence R . (x,x) = 1 by XXREAL_0:1; ::_thesis: verum end; end; assume A2: for x being Element of X holds R . (x,x) = 1 ; ::_thesis: R is reflexive let x, y be Element of X; :: according to LFUZZY_1:def_1,LFUZZY_1:def_2 ::_thesis: (Imf (X,X)) . (x,y) <= R . (x,y) percases ( x = y or x <> y ) ; supposeA3: x = y ; ::_thesis: (Imf (X,X)) . (x,y) <= R . (x,y) then (Imf (X,X)) . (x,y) = 1 by FUZZY_4:25; hence (Imf (X,X)) . (x,y) <= R . (x,y) by A2, A3; ::_thesis: verum end; suppose x <> y ; ::_thesis: (Imf (X,X)) . (x,y) <= R . (x,y) then (Imf (X,X)) . (x,y) = 0 by FUZZY_4:25; hence (Imf (X,X)) . (x,y) <= R . (x,y) by FUZZY_4:4; ::_thesis: verum end; end; end; end; :: deftheorem Def3 defines reflexive LFUZZY_1:def_3_:_ for X being non empty set for R being RMembership_Func of X,X holds ( R is reflexive iff for x being Element of X holds R . (x,x) = 1 ); definition let X be non empty set ; let R be RMembership_Func of X,X; attrR is symmetric means :Def4: :: LFUZZY_1:def 4 converse R = R; end; :: deftheorem Def4 defines symmetric LFUZZY_1:def_4_:_ for X being non empty set for R being RMembership_Func of X,X holds ( R is symmetric iff converse R = R ); definition let X be non empty set ; let R be RMembership_Func of X,X; redefine attr R is symmetric means :Def5: :: LFUZZY_1:def 5 for x, y being Element of X holds R . (x,y) = R . (y,x); compatibility ( R is symmetric iff for x, y being Element of X holds R . (x,y) = R . (y,x) ) proof thus ( R is symmetric iff for x, y being Element of X holds R . (x,y) = R . (y,x) ) ::_thesis: verum proof hereby ::_thesis: ( ( for x, y being Element of X holds R . (x,y) = R . (y,x) ) implies R is symmetric ) assume R is symmetric ; ::_thesis: for x, y being Element of X holds R . (x,y) = R . (y,x) then converse R = R by Def4; hence for x, y being Element of X holds R . (x,y) = R . (y,x) by FUZZY_4:26; ::_thesis: verum end; assume A1: for x, y being Element of X holds R . (x,y) = R . (y,x) ; ::_thesis: R is symmetric A2: 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 ; ::_thesis: ( [x,y] in dom R implies (converse R) . (x,y) = R . (x,y) ) assume [x,y] in dom R ; ::_thesis: (converse R) . (x,y) = R . (x,y) then reconsider x = x, y = y as Element of X by ZFMISC_1:87; R . (x,y) = R . (y,x) by A1; hence (converse R) . (x,y) = R . (x,y) by FUZZY_4:26; ::_thesis: verum end; ( dom (converse R) = [:X,X:] & dom R = [:X,X:] ) by FUNCT_2:def_1; then converse R = R by A2, BINOP_1:20; hence R is symmetric by Def4; ::_thesis: verum end; end; end; :: deftheorem Def5 defines symmetric LFUZZY_1:def_5_:_ for X being non empty set for R being RMembership_Func of X,X holds ( R is symmetric iff for x, y being Element of X holds R . (x,y) = R . (y,x) ); definition let X be non empty set ; let R be RMembership_Func of X,X; attrR is transitive means :Def6: :: LFUZZY_1:def 6 R c= ; end; :: deftheorem Def6 defines transitive LFUZZY_1:def_6_:_ for X being non empty set for R being RMembership_Func of X,X holds ( R is transitive iff R c= ); Lm1: 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 for z being Element of Z holds ( rng (min (R,S,x,z)) = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } & rng (min (R,S,x,z)) <> {} ) proof let X, Y, Z be non empty set ; ::_thesis: for R being RMembership_Func of X,Y for S being RMembership_Func of Y,Z for x being Element of X for z being Element of Z holds ( rng (min (R,S,x,z)) = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } & rng (min (R,S,x,z)) <> {} ) let R be RMembership_Func of X,Y; ::_thesis: for S being RMembership_Func of Y,Z for x being Element of X for z being Element of Z holds ( rng (min (R,S,x,z)) = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } & rng (min (R,S,x,z)) <> {} ) let S be RMembership_Func of Y,Z; ::_thesis: for x being Element of X for z being Element of Z holds ( rng (min (R,S,x,z)) = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } & rng (min (R,S,x,z)) <> {} ) let x be Element of X; ::_thesis: for z being Element of Z holds ( rng (min (R,S,x,z)) = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } & rng (min (R,S,x,z)) <> {} ) let z be Element of Z; ::_thesis: ( rng (min (R,S,x,z)) = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } & rng (min (R,S,x,z)) <> {} ) set L = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } ; A1: ( 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 FUNCT_2:def_1, RELSET_1:4; for c being set holds ( c in { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } iff c in rng (min (R,S,x,z)) ) proof let c be set ; ::_thesis: ( c in { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } iff c in rng (min (R,S,x,z)) ) hereby ::_thesis: ( c in rng (min (R,S,x,z)) implies c in { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } ) assume c in { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } ; ::_thesis: c in rng (min (R,S,x,z)) then consider y being Element of Y such that A2: c = (R . [x,y]) "/\" (S . [y,z]) ; c = (min (R,S,x,z)) . y by A2, FUZZY_4:def_2; hence c in rng (min (R,S,x,z)) by A1, PARTFUN1:4; ::_thesis: verum end; assume c in rng (min (R,S,x,z)) ; ::_thesis: c in { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } then consider y being Element of Y such that y in dom (min (R,S,x,z)) and A3: c = (min (R,S,x,z)) . y by PARTFUN1:3; c = (R . [x,y]) "/\" (S . [y,z]) by A3, FUZZY_4:def_2; hence c in { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } ; ::_thesis: verum end; hence rng (min (R,S,x,z)) = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } by TARSKI:1; ::_thesis: rng (min (R,S,x,z)) <> {} thus rng (min (R,S,x,z)) <> {} ; ::_thesis: verum end; definition let X be non empty set ; let R be RMembership_Func of X,X; redefine attr R is transitive means :: LFUZZY_1:def 7 for x, y, z being Element of X holds (R . [x,y]) "/\" (R . [y,z]) <<= R . [x,z]; compatibility ( R is transitive iff for x, y, z being Element of X holds (R . [x,y]) "/\" (R . [y,z]) <<= R . [x,z] ) proof thus ( R is transitive iff for x, y, z being Element of X holds (R . [x,y]) "/\" (R . [y,z]) <<= R . [x,z] ) ::_thesis: verum proof hereby ::_thesis: ( ( for x, y, z being Element of X holds (R . [x,y]) "/\" (R . [y,z]) <<= R . [x,z] ) implies R is transitive ) assume R is transitive ; ::_thesis: for x, y, z being Element of X holds (R . [x,y]) "/\" (R . [y,z]) <<= R . [x,z] then A1: R c= by Def6; thus for x, y, z being Element of X holds (R . [x,y]) "/\" (R . [y,z]) <<= R . [x,z] ::_thesis: verum proof let x, y, z be Element of X; ::_thesis: (R . [x,y]) "/\" (R . [y,z]) <<= R . [x,z] (R . (x,y)) "/\" (R . (y,z)) in { ((R . (x,y9)) "/\" (R . (y9,z))) where y9 is Element of X : verum } ; then (R . (x,y)) "/\" (R . (y,z)) <<= "\/" ( { ((R . (x,y9)) "/\" (R . (y9,z))) where y9 is Element of X : verum } ,(RealPoset [.0,1.])) by YELLOW_2:22; then (R . (x,y)) "/\" (R . (y,z)) <<= (R (#) R) . (x,z) by LFUZZY_0:22; then A2: (R . (x,y)) "/\" (R . (y,z)) <= (R (#) R) . (x,z) by LFUZZY_0:3; (R (#) R) . (x,z) <= R . (x,z) by A1, Def1; then (R . [x,y]) "/\" (R . [y,z]) <= R . [x,z] by A2, XXREAL_0:2; hence (R . [x,y]) "/\" (R . [y,z]) <<= R . [x,z] by LFUZZY_0:3; ::_thesis: verum end; end; assume A3: for x, y, z being Element of X holds (R . [x,y]) "/\" (R . [y,z]) <<= R . [x,z] ; ::_thesis: R is transitive thus R c= :: according to LFUZZY_1:def_6 ::_thesis: verum proof let x, z be Element of X; :: according to LFUZZY_1:def_1 ::_thesis: (R (#) R) . (x,z) <= R . (x,z) set W = rng (min (R,R,x,z)); for r being real number st r in rng (min (R,R,x,z)) holds r <= R . [x,z] proof let r be real number ; ::_thesis: ( r in rng (min (R,R,x,z)) implies r <= R . [x,z] ) assume r in rng (min (R,R,x,z)) ; ::_thesis: r <= R . [x,z] then r in { ((R . [x,y9]) "/\" (R . [y9,z])) where y9 is Element of X : verum } by Lm1; 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 A3; hence r <= R . [x,z] by A4, LFUZZY_0:3; ::_thesis: verum end; then upper_bound (rng (min (R,R,x,z))) <= R . [x,z] by SEQ_4:144; hence (R (#) R) . (x,z) <= R . (x,z) by FUZZY_4:def_3; ::_thesis: verum end; end; end; end; :: deftheorem defines transitive LFUZZY_1:def_7_:_ for X being non empty set for R being RMembership_Func of X,X holds ( R is transitive iff for x, y, z being Element of X holds (R . [x,y]) "/\" (R . [y,z]) <<= R . [x,z] ); definition let X be non empty set ; let R be RMembership_Func of X,X; attrR is antisymmetric means :Def8: :: LFUZZY_1:def 8 for x, y being Element of X st R . (x,y) <> 0 & R . (y,x) <> 0 holds x = y; end; :: deftheorem Def8 defines antisymmetric LFUZZY_1:def_8_:_ for X being non empty set for R being RMembership_Func of X,X holds ( R is antisymmetric iff for x, y being Element of X st R . (x,y) <> 0 & R . (y,x) <> 0 holds x = y ); registration let X be non empty set ; cluster Imf (X,X) -> reflexive symmetric transitive antisymmetric ; coherence ( Imf (X,X) is symmetric & Imf (X,X) is transitive & Imf (X,X) is reflexive & Imf (X,X) is antisymmetric ) proof thus Imf (X,X) is symmetric ::_thesis: ( Imf (X,X) is transitive & Imf (X,X) is reflexive & Imf (X,X) is antisymmetric ) proof let x, y be Element of X; :: according to LFUZZY_1:def_5 ::_thesis: (Imf (X,X)) . (x,y) = (Imf (X,X)) . (y,x) percases ( x = y or not x = y ) ; suppose x = y ; ::_thesis: (Imf (X,X)) . (x,y) = (Imf (X,X)) . (y,x) hence (Imf (X,X)) . (x,y) = (Imf (X,X)) . (y,x) ; ::_thesis: verum end; supposeA1: not x = y ; ::_thesis: (Imf (X,X)) . (x,y) = (Imf (X,X)) . (y,x) hence (Imf (X,X)) . (x,y) = 0 by FUZZY_4:25 .= (Imf (X,X)) . (y,x) by A1, FUZZY_4:25 ; ::_thesis: verum end; end; end; thus Imf (X,X) is transitive ::_thesis: ( Imf (X,X) is reflexive & Imf (X,X) is antisymmetric ) proof let x, y, z be Element of X; :: according to LFUZZY_1:def_7 ::_thesis: ((Imf (X,X)) . [x,y]) "/\" ((Imf (X,X)) . [y,z]) <<= (Imf (X,X)) . [x,z] percases ( x = z or not x = z ) ; supposeA2: x = z ; ::_thesis: ((Imf (X,X)) . [x,y]) "/\" ((Imf (X,X)) . [y,z]) <<= (Imf (X,X)) . [x,z] thus ((Imf (X,X)) . [x,y]) "/\" ((Imf (X,X)) . [y,z]) <<= (Imf (X,X)) . [x,z] ::_thesis: verum proof percases ( x = y or not x = y ) ; supposeA3: x = y ; ::_thesis: ((Imf (X,X)) . [x,y]) "/\" ((Imf (X,X)) . [y,z]) <<= (Imf (X,X)) . [x,z] ((Imf (X,X)) . [x,y]) "/\" ((Imf (X,X)) . [y,z]) = min (((Imf (X,X)) . (x,y)),((Imf (X,X)) . (y,z))) .= 1 by A2, A3, FUZZY_4:25 ; then ((Imf (X,X)) . (x,y)) "/\" ((Imf (X,X)) . (y,z)) <= (Imf (X,X)) . (x,z) by A2, FUZZY_4:25; hence ((Imf (X,X)) . [x,y]) "/\" ((Imf (X,X)) . [y,z]) <<= (Imf (X,X)) . [x,z] by LFUZZY_0:3; ::_thesis: verum end; supposeA4: not x = y ; ::_thesis: ((Imf (X,X)) . [x,y]) "/\" ((Imf (X,X)) . [y,z]) <<= (Imf (X,X)) . [x,z] ((Imf (X,X)) . [x,y]) "/\" ((Imf (X,X)) . [y,z]) = min (((Imf (X,X)) . (x,y)),((Imf (X,X)) . (y,z))) .= min (((Imf (X,X)) . (x,y)),0) by A2, A4, FUZZY_4:25 .= min (0,0) by A4, FUZZY_4:25 .= 0 ; then ((Imf (X,X)) . (x,y)) "/\" ((Imf (X,X)) . (y,z)) <= (Imf (X,X)) . (x,z) by A2, FUZZY_4:25; hence ((Imf (X,X)) . [x,y]) "/\" ((Imf (X,X)) . [y,z]) <<= (Imf (X,X)) . [x,z] by LFUZZY_0:3; ::_thesis: verum end; end; end; end; supposeA5: not x = z ; ::_thesis: ((Imf (X,X)) . [x,y]) "/\" ((Imf (X,X)) . [y,z]) <<= (Imf (X,X)) . [x,z] thus ((Imf (X,X)) . [x,y]) "/\" ((Imf (X,X)) . [y,z]) <<= (Imf (X,X)) . [x,z] ::_thesis: verum proof percases ( x = y or x <> y ) ; supposeA6: x = y ; ::_thesis: ((Imf (X,X)) . [x,y]) "/\" ((Imf (X,X)) . [y,z]) <<= (Imf (X,X)) . [x,z] ((Imf (X,X)) . [x,y]) "/\" ((Imf (X,X)) . [y,z]) = min (((Imf (X,X)) . (x,y)),((Imf (X,X)) . (y,z))) .= min (((Imf (X,X)) . (x,y)),0) by A5, A6, FUZZY_4:25 .= min (1,0) by A6, FUZZY_4:25 .= 0 by XXREAL_0:def_9 ; then ((Imf (X,X)) . (x,y)) "/\" ((Imf (X,X)) . (y,z)) <= (Imf (X,X)) . (x,z) by A5, FUZZY_4:25; hence ((Imf (X,X)) . [x,y]) "/\" ((Imf (X,X)) . [y,z]) <<= (Imf (X,X)) . [x,z] by LFUZZY_0:3; ::_thesis: verum end; supposeA7: x <> y ; ::_thesis: ((Imf (X,X)) . [x,y]) "/\" ((Imf (X,X)) . [y,z]) <<= (Imf (X,X)) . [x,z] thus ((Imf (X,X)) . [x,y]) "/\" ((Imf (X,X)) . [y,z]) <<= (Imf (X,X)) . [x,z] ::_thesis: verum proof percases ( y = z or y <> z ) ; supposeA8: y = z ; ::_thesis: ((Imf (X,X)) . [x,y]) "/\" ((Imf (X,X)) . [y,z]) <<= (Imf (X,X)) . [x,z] ((Imf (X,X)) . [x,y]) "/\" ((Imf (X,X)) . [y,z]) = min (((Imf (X,X)) . (x,y)),((Imf (X,X)) . (y,z))) .= min (((Imf (X,X)) . (x,y)),1) by A8, FUZZY_4:25 .= min (0,1) by A7, FUZZY_4:25 .= 0 by XXREAL_0:def_9 ; then ((Imf (X,X)) . (x,y)) "/\" ((Imf (X,X)) . (y,z)) <= (Imf (X,X)) . (x,z) by A5, FUZZY_4:25; hence ((Imf (X,X)) . [x,y]) "/\" ((Imf (X,X)) . [y,z]) <<= (Imf (X,X)) . [x,z] by LFUZZY_0:3; ::_thesis: verum end; supposeA9: y <> z ; ::_thesis: ((Imf (X,X)) . [x,y]) "/\" ((Imf (X,X)) . [y,z]) <<= (Imf (X,X)) . [x,z] ((Imf (X,X)) . [x,y]) "/\" ((Imf (X,X)) . [y,z]) = min (((Imf (X,X)) . (x,y)),((Imf (X,X)) . (y,z))) .= min (((Imf (X,X)) . (x,y)),0) by A9, FUZZY_4:25 .= min (0,0) by A7, FUZZY_4:25 .= 0 ; then ((Imf (X,X)) . (x,y)) "/\" ((Imf (X,X)) . (y,z)) <= (Imf (X,X)) . (x,z) by A5, FUZZY_4:25; hence ((Imf (X,X)) . [x,y]) "/\" ((Imf (X,X)) . [y,z]) <<= (Imf (X,X)) . [x,z] by LFUZZY_0:3; ::_thesis: verum end; end; end; end; end; end; end; end; end; thus Imf (X,X) is reflexive by Def2; ::_thesis: Imf (X,X) is antisymmetric thus for x, y being Element of X st (Imf (X,X)) . (x,y) <> 0 & (Imf (X,X)) . (y,x) <> 0 holds x = y by FUZZY_4:25; :: according to LFUZZY_1:def_8 ::_thesis: verum end; end; registration let X be non empty set ; cluster non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued reflexive symmetric transitive antisymmetric for Element of bool [:[:X,X:],REAL:]; existence ex b1 being RMembership_Func of X,X st ( b1 is reflexive & b1 is transitive & b1 is symmetric & b1 is antisymmetric ) proof take Imf (X,X) ; ::_thesis: ( Imf (X,X) is reflexive & Imf (X,X) is transitive & Imf (X,X) is symmetric & Imf (X,X) is antisymmetric ) thus ( Imf (X,X) is reflexive & Imf (X,X) is transitive & Imf (X,X) is symmetric & Imf (X,X) is antisymmetric ) ; ::_thesis: verum end; end; theorem Th9: :: LFUZZY_1:9 for X being non empty set for R, S being RMembership_Func of X,X st R is symmetric & S is symmetric holds converse (min (R,S)) = min (R,S) proof let X be non empty set ; ::_thesis: for R, S being RMembership_Func of X,X st R is symmetric & S is symmetric holds converse (min (R,S)) = min (R,S) let R, S be RMembership_Func of X,X; ::_thesis: ( R is symmetric & S is symmetric implies converse (min (R,S)) = min (R,S) ) assume ( R is symmetric & S is symmetric ) ; ::_thesis: converse (min (R,S)) = min (R,S) then ( converse R = R & converse S = S ) by Def4; hence converse (min (R,S)) = min (R,S) by FUZZY_4:8; ::_thesis: verum end; theorem Th10: :: LFUZZY_1:10 for X being non empty set for R, S being RMembership_Func of X,X st R is symmetric & S is symmetric holds converse (max (R,S)) = max (R,S) proof let X be non empty set ; ::_thesis: for R, S being RMembership_Func of X,X st R is symmetric & S is symmetric holds converse (max (R,S)) = max (R,S) let R, S be RMembership_Func of X,X; ::_thesis: ( R is symmetric & S is symmetric implies converse (max (R,S)) = max (R,S) ) assume ( R is symmetric & S is symmetric ) ; ::_thesis: converse (max (R,S)) = max (R,S) then ( converse R = R & converse S = S ) by Def4; hence converse (max (R,S)) = max (R,S) by FUZZY_4:7; ::_thesis: verum end; registration let X be non empty set ; let R, S be symmetric RMembership_Func of X,X; cluster min (R,S) -> symmetric ; coherence min (R,S) is symmetric proof converse (min (R,S)) = min (R,S) by Th9; hence min (R,S) is symmetric by Def4; ::_thesis: verum end; cluster max (R,S) -> symmetric ; coherence max (R,S) is symmetric proof converse (max (R,S)) = max (R,S) by Th10; hence max (R,S) is symmetric by Def4; ::_thesis: verum end; end; theorem Th11: :: LFUZZY_1:11 for X being non empty set for R, S being RMembership_Func of X,X st R is transitive & S is transitive holds min (R,S) c= proof let X be non empty set ; ::_thesis: for R, S being RMembership_Func of X,X st R is transitive & S is transitive holds min (R,S) c= let R, S be RMembership_Func of X,X; ::_thesis: ( R is transitive & S is transitive implies min (R,S) c= ) assume that A1: R is transitive and A2: S is transitive ; ::_thesis: min (R,S) c= let x be Element of X; :: according to LFUZZY_1:def_1 ::_thesis: for y being Element of X holds ((min (R,S)) (#) (min (R,S))) . (x,y) <= (min (R,S)) . (x,y) let y be Element of X; ::_thesis: ((min (R,S)) (#) (min (R,S))) . (x,y) <= (min (R,S)) . (x,y) (min ((R (#) S),(S (#) S))) . [x,y] = min (((S (#) S) . [x,y]),((R (#) S) . [x,y])) by FUZZY_1:def_3; then A3: (min ((R (#) S),(S (#) S))) . [x,y] <= (S (#) S) . [x,y] by XXREAL_0:17; S c= by A2, Def6; then (S (#) S) . (x,y) <= S . (x,y) by Def1; then A4: (min ((R (#) S),(S (#) S))) . [x,y] <= S . [x,y] by A3, XXREAL_0:2; (min ((R (#) R),(S (#) R))) . [x,y] = min (((R (#) R) . [x,y]),((S (#) R) . [x,y])) by FUZZY_1:def_3; then A5: (min ((R (#) R),(S (#) R))) . [x,y] <= (R (#) R) . [x,y] by XXREAL_0:17; R c= by A1, Def6; then (R (#) R) . (x,y) <= R . (x,y) by Def1; then (min ((R (#) R),(S (#) R))) . [x,y] <= R . [x,y] by A5, XXREAL_0:2; then A6: min (((min ((R (#) R),(S (#) R))) . [x,y]),((min ((R (#) S),(S (#) S))) . [x,y])) <= min ((R . [x,y]),(S . [x,y])) by A4, XXREAL_0:18; min (((min (R,S)) (#) R),((min (R,S)) (#) S)) c= by FUZZY_4:15; then A7: ((min (R,S)) (#) (min (R,S))) . [x,y] <= (min (((min (R,S)) (#) R),((min (R,S)) (#) S))) . [x,y] by FUZZY_1:def_2; min ((R (#) S),(S (#) S)) c= by FUZZY_4:16; then A8: ((min (R,S)) (#) S) . [x,y] <= (min ((R (#) S),(S (#) S))) . [x,y] by FUZZY_1:def_2; min ((R (#) R),(S (#) R)) c= by FUZZY_4:16; then ( (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] ) by FUZZY_1:def_2, FUZZY_1:def_3; 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 A8, XXREAL_0:18; then ((min (R,S)) (#) (min (R,S))) . [x,y] <= min (((min ((R (#) R),(S (#) R))) . [x,y]),((min ((R (#) S),(S (#) S))) . [x,y])) by A7, XXREAL_0:2; then ((min (R,S)) (#) (min (R,S))) . [x,y] <= min ((R . [x,y]),(S . [x,y])) by A6, XXREAL_0:2; hence ((min (R,S)) (#) (min (R,S))) . (x,y) <= (min (R,S)) . (x,y) by FUZZY_1:def_3; ::_thesis: verum end; registration let X be non empty set ; let R, S be transitive RMembership_Func of X,X; cluster min (R,S) -> transitive ; coherence min (R,S) is transitive proof min (R,S) c= by Th11; hence min (R,S) is transitive by Def6; ::_thesis: verum end; end; definition let A be set ; let X be non empty set ; :: original: chi redefine func chi (A,X) -> Membership_Func of X; coherence chi (A,X) is Membership_Func of X proof dom (chi (A,X)) = X by FUNCT_3:def_3; hence chi (A,X) is Membership_Func of X by FUNCT_2:def_1; ::_thesis: verum end; end; theorem :: LFUZZY_1:12 for X being non empty set for r being Relation of X st r is_reflexive_in X holds chi (r,[:X,X:]) is reflexive proof let X be non empty set ; ::_thesis: for r being Relation of X st r is_reflexive_in X holds chi (r,[:X,X:]) is reflexive let r be Relation of X; ::_thesis: ( r is_reflexive_in X implies chi (r,[:X,X:]) is reflexive ) assume A1: r is_reflexive_in X ; ::_thesis: chi (r,[:X,X:]) is reflexive for x being Element of X holds (chi (r,[:X,X:])) . (x,x) = 1 proof let x be Element of X; ::_thesis: (chi (r,[:X,X:])) . (x,x) = 1 [x,x] in r by A1, RELAT_2:def_1; hence (chi (r,[:X,X:])) . (x,x) = 1 by FUNCT_3:def_3; ::_thesis: verum end; hence chi (r,[:X,X:]) is reflexive by Def3; ::_thesis: verum end; theorem :: LFUZZY_1:13 for X being non empty set for r being Relation of X st r is antisymmetric holds chi (r,[:X,X:]) is antisymmetric proof let X be non empty set ; ::_thesis: for r being Relation of X st r is antisymmetric holds chi (r,[:X,X:]) is antisymmetric let r be Relation of X; ::_thesis: ( r is antisymmetric implies chi (r,[:X,X:]) is antisymmetric ) assume r is antisymmetric ; ::_thesis: chi (r,[:X,X:]) is antisymmetric then A1: r is_antisymmetric_in field r by RELAT_2:def_12; for x, y being Element of X st (chi (r,[:X,X:])) . (x,y) <> 0 & (chi (r,[:X,X:])) . (y,x) <> 0 holds x = y proof let x, y be Element of X; ::_thesis: ( (chi (r,[:X,X:])) . (x,y) <> 0 & (chi (r,[:X,X:])) . (y,x) <> 0 implies x = y ) assume that A2: (chi (r,[:X,X:])) . (x,y) <> 0 and A3: (chi (r,[:X,X:])) . (y,x) <> 0 ; ::_thesis: x = y A4: ( x in field r & y in field r & [x,y] in r & [y,x] in r implies x = y ) by A1, RELAT_2:def_4; [x,y] in r by A2, FUNCT_3:def_3; hence x = y by A3, A4, FUNCT_3:def_3, RELAT_1:15; ::_thesis: verum end; hence chi (r,[:X,X:]) is antisymmetric by Def8; ::_thesis: verum end; theorem :: LFUZZY_1:14 for X being non empty set for r being Relation of X st r is symmetric holds chi (r,[:X,X:]) is symmetric proof let X be non empty set ; ::_thesis: for r being Relation of X st r is symmetric holds chi (r,[:X,X:]) is symmetric let r be Relation of X; ::_thesis: ( r is symmetric implies chi (r,[:X,X:]) is symmetric ) assume r is symmetric ; ::_thesis: chi (r,[:X,X:]) is symmetric then A1: r is_symmetric_in field r by RELAT_2:def_11; let x, y be Element of X; :: according to LFUZZY_1:def_5 ::_thesis: (chi (r,[:X,X:])) . (x,y) = (chi (r,[:X,X:])) . (y,x) A2: ( x in field r & y in field r & [x,y] in r implies [y,x] in r ) by A1, RELAT_2:def_3; A3: ( x in field r & y in field r & [y,x] in r implies [x,y] in r ) by A1, RELAT_2:def_3; percases ( [x,y] in r or not [x,y] in r ) ; supposeA4: [x,y] in r ; ::_thesis: (chi (r,[:X,X:])) . (x,y) = (chi (r,[:X,X:])) . (y,x) then (chi (r,[:X,X:])) . [x,y] = 1 by FUNCT_3:def_3; hence (chi (r,[:X,X:])) . (x,y) = (chi (r,[:X,X:])) . (y,x) by A2, A4, FUNCT_3:def_3, RELAT_1:15; ::_thesis: verum end; suppose not [x,y] in r ; ::_thesis: (chi (r,[:X,X:])) . (x,y) = (chi (r,[:X,X:])) . (y,x) then ( not [y,x] in r & (chi (r,[:X,X:])) . [x,y] = 0 ) by A3, FUNCT_3:def_3, RELAT_1:15; hence (chi (r,[:X,X:])) . (x,y) = (chi (r,[:X,X:])) . (y,x) by FUNCT_3:def_3; ::_thesis: verum end; end; end; theorem :: LFUZZY_1:15 for X being non empty set for r being Relation of X st r is transitive holds chi (r,[:X,X:]) is transitive proof let X be non empty set ; ::_thesis: for r being Relation of X st r is transitive holds chi (r,[:X,X:]) is transitive let r be Relation of X; ::_thesis: ( r is transitive implies chi (r,[:X,X:]) is transitive ) assume A1: r is transitive ; ::_thesis: chi (r,[:X,X:]) is transitive let x, y, z be Element of X; :: according to LFUZZY_1:def_7 ::_thesis: ((chi (r,[:X,X:])) . [x,y]) "/\" ((chi (r,[:X,X:])) . [y,z]) <<= (chi (r,[:X,X:])) . [x,z] r is_transitive_in field r by A1, RELAT_2:def_16; then 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; percases ( [x,y] in r or not [x,y] in r ) ; supposeA3: [x,y] in r ; ::_thesis: ((chi (r,[:X,X:])) . [x,y]) "/\" ((chi (r,[:X,X:])) . [y,z]) <<= (chi (r,[:X,X:])) . [x,z] thus ((chi (r,[:X,X:])) . [x,y]) "/\" ((chi (r,[:X,X:])) . [y,z]) <<= (chi (r,[:X,X:])) . [x,z] ::_thesis: verum proof percases ( [y,z] in r or not [y,z] in r ) ; supposeA4: [y,z] in r ; ::_thesis: ((chi (r,[:X,X:])) . [x,y]) "/\" ((chi (r,[:X,X:])) . [y,z]) <<= (chi (r,[:X,X:])) . [x,z] ((chi (r,[:X,X:])) . [x,y]) "/\" ((chi (r,[:X,X:])) . [y,z]) = min (1,((chi (r,[:X,X:])) . [y,z])) by A3, FUNCT_3:def_3 .= min (1,1) by A4, FUNCT_3:def_3 .= (chi (r,[:X,X:])) . [x,z] by A2, A3, A4, FUNCT_3:def_3, RELAT_1:15 ; hence ((chi (r,[:X,X:])) . [x,y]) "/\" ((chi (r,[:X,X:])) . [y,z]) <<= (chi (r,[:X,X:])) . [x,z] by LFUZZY_0:3; ::_thesis: verum end; supposeA5: not [y,z] in r ; ::_thesis: ((chi (r,[:X,X:])) . [x,y]) "/\" ((chi (r,[:X,X:])) . [y,z]) <<= (chi (r,[:X,X:])) . [x,z] ((chi (r,[:X,X:])) . [x,y]) "/\" ((chi (r,[:X,X:])) . [y,z]) = min (1,((chi (r,[:X,X:])) . [y,z])) by A3, FUNCT_3:def_3 .= min (1,0) by A5, FUNCT_3:def_3 .= 0 by XXREAL_0:def_9 ; then ((chi (r,[:X,X:])) . [x,y]) "/\" ((chi (r,[:X,X:])) . [y,z]) <= (chi (r,[:X,X:])) . [x,z] by FUZZY_2:1; hence ((chi (r,[:X,X:])) . [x,y]) "/\" ((chi (r,[:X,X:])) . [y,z]) <<= (chi (r,[:X,X:])) . [x,z] by LFUZZY_0:3; ::_thesis: verum end; end; end; end; supposeA6: not [x,y] in r ; ::_thesis: ((chi (r,[:X,X:])) . [x,y]) "/\" ((chi (r,[:X,X:])) . [y,z]) <<= (chi (r,[:X,X:])) . [x,z] thus ((chi (r,[:X,X:])) . [x,y]) "/\" ((chi (r,[:X,X:])) . [y,z]) <<= (chi (r,[:X,X:])) . [x,z] ::_thesis: verum proof percases ( [y,z] in r or not [y,z] in r ) ; supposeA7: [y,z] in r ; ::_thesis: ((chi (r,[:X,X:])) . [x,y]) "/\" ((chi (r,[:X,X:])) . [y,z]) <<= (chi (r,[:X,X:])) . [x,z] ((chi (r,[:X,X:])) . [x,y]) "/\" ((chi (r,[:X,X:])) . [y,z]) = min (0,((chi (r,[:X,X:])) . [y,z])) by A6, FUNCT_3:def_3 .= min (0,1) by A7, FUNCT_3:def_3 .= 0 by XXREAL_0:def_9 ; then ((chi (r,[:X,X:])) . [x,y]) "/\" ((chi (r,[:X,X:])) . [y,z]) <= (chi (r,[:X,X:])) . [x,z] by FUZZY_2:1; hence ((chi (r,[:X,X:])) . [x,y]) "/\" ((chi (r,[:X,X:])) . [y,z]) <<= (chi (r,[:X,X:])) . [x,z] by LFUZZY_0:3; ::_thesis: verum end; supposeA8: not [y,z] in r ; ::_thesis: ((chi (r,[:X,X:])) . [x,y]) "/\" ((chi (r,[:X,X:])) . [y,z]) <<= (chi (r,[:X,X:])) . [x,z] ((chi (r,[:X,X:])) . [x,y]) "/\" ((chi (r,[:X,X:])) . [y,z]) = min (0,((chi (r,[:X,X:])) . [y,z])) by A6, FUNCT_3:def_3 .= min (0,0) by A8, 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 ((chi (r,[:X,X:])) . [x,y]) "/\" ((chi (r,[:X,X:])) . [y,z]) <<= (chi (r,[:X,X:])) . [x,z] by LFUZZY_0:3; ::_thesis: verum end; end; end; end; end; end; theorem :: LFUZZY_1:16 for X being non empty set holds ( Zmf (X,X) is symmetric & Zmf (X,X) is antisymmetric & Zmf (X,X) is transitive ) proof let X be non empty set ; ::_thesis: ( Zmf (X,X) is symmetric & Zmf (X,X) is antisymmetric & Zmf (X,X) is transitive ) thus Zmf (X,X) is symmetric ::_thesis: ( Zmf (X,X) is antisymmetric & Zmf (X,X) is transitive ) proof let x, y be Element of X; :: according to LFUZZY_1:def_5 ::_thesis: (Zmf (X,X)) . (x,y) = (Zmf (X,X)) . (y,x) ( (Zmf (X,X)) . [x,y] = 0 & (Zmf (X,X)) . [y,x] = 0 ) by FUZZY_4:21; hence (Zmf (X,X)) . (x,y) = (Zmf (X,X)) . (y,x) ; ::_thesis: verum end; thus Zmf (X,X) is antisymmetric ::_thesis: Zmf (X,X) is transitive proof let x, y be Element of X; :: according to LFUZZY_1:def_8 ::_thesis: ( (Zmf (X,X)) . (x,y) <> 0 & (Zmf (X,X)) . (y,x) <> 0 implies x = y ) (Zmf (X,X)) . [x,y] = 0 by FUZZY_4:21; hence ( (Zmf (X,X)) . (x,y) <> 0 & (Zmf (X,X)) . (y,x) <> 0 implies x = y ) ; ::_thesis: verum end; thus Zmf (X,X) is transitive ::_thesis: verum proof let x, y, z be Element of X; :: according to LFUZZY_1:def_7 ::_thesis: ((Zmf (X,X)) . [x,y]) "/\" ((Zmf (X,X)) . [y,z]) <<= (Zmf (X,X)) . [x,z] A1: (Zmf (X,X)) . [x,z] = 0 by FUZZY_4:20; ((Zmf (X,X)) . [x,y]) "/\" ((Zmf (X,X)) . [y,z]) = min (0,((Zmf (X,X)) . [y,z])) by FUZZY_4:20 .= min (0,0) by FUZZY_4:20 .= 0 ; hence ((Zmf (X,X)) . [x,y]) "/\" ((Zmf (X,X)) . [y,z]) <<= (Zmf (X,X)) . [x,z] by A1, LFUZZY_0:3; ::_thesis: verum end; end; theorem :: LFUZZY_1:17 for X being non empty set holds ( Umf (X,X) is symmetric & Umf (X,X) is transitive & Umf (X,X) is reflexive ) proof let X be non empty set ; ::_thesis: ( Umf (X,X) is symmetric & Umf (X,X) is transitive & Umf (X,X) is reflexive ) thus Umf (X,X) is symmetric ::_thesis: ( Umf (X,X) is transitive & Umf (X,X) is reflexive ) proof let x, y be Element of X; :: according to LFUZZY_1:def_5 ::_thesis: (Umf (X,X)) . (x,y) = (Umf (X,X)) . (y,x) thus (Umf (X,X)) . (x,y) = (Umf (X,X)) . [x,y] .= 1 by FUZZY_4:21 .= (Umf (X,X)) . [y,x] by FUZZY_4:21 .= (Umf (X,X)) . (y,x) ; ::_thesis: verum end; thus Umf (X,X) is transitive ::_thesis: Umf (X,X) is reflexive proof let x, y, z be Element of X; :: according to LFUZZY_1:def_7 ::_thesis: ((Umf (X,X)) . [x,y]) "/\" ((Umf (X,X)) . [y,z]) <<= (Umf (X,X)) . [x,z] ((Umf (X,X)) . [x,y]) "/\" ((Umf (X,X)) . [y,z]) = min (1,((Umf (X,X)) . [y,z])) by FUZZY_4:20 .= min (1,1) by FUZZY_4:20 .= 1 ; then ((Umf (X,X)) . [x,y]) "/\" ((Umf (X,X)) . [y,z]) <= (Umf (X,X)) . [x,z] by FUZZY_4:20; hence ((Umf (X,X)) . [x,y]) "/\" ((Umf (X,X)) . [y,z]) <<= (Umf (X,X)) . [x,z] by LFUZZY_0:3; ::_thesis: verum end; thus Umf (X,X) is reflexive ::_thesis: verum proof let x be Element of X; :: according to LFUZZY_1:def_3 ::_thesis: (Umf (X,X)) . (x,x) = 1 (Umf (X,X)) . [x,x] = 1 by FUZZY_4:21; hence (Umf (X,X)) . (x,x) = 1 ; ::_thesis: verum end; end; theorem :: LFUZZY_1:18 for X being non empty set for R being RMembership_Func of X,X holds max (R,(converse R)) is symmetric proof let X be non empty set ; ::_thesis: for R being RMembership_Func of X,X holds max (R,(converse R)) is symmetric let R be RMembership_Func of X,X; ::_thesis: max (R,(converse R)) is symmetric set S = max (R,(converse R)); let x, y be Element of X; :: according to LFUZZY_1:def_5 ::_thesis: (max (R,(converse R))) . (x,y) = (max (R,(converse R))) . (y,x) thus (max (R,(converse R))) . (x,y) = (max (R,(converse R))) . [x,y] .= max ((R . (x,y)),((converse R) . (x,y))) by FUZZY_1:def_4 .= max ((R . (x,y)),(R . (y,x))) by FUZZY_4:26 .= max (((converse R) . (y,x)),(R . (y,x))) by FUZZY_4:26 .= (max (R,(converse R))) . [y,x] by FUZZY_1:def_4 .= (max (R,(converse R))) . (y,x) ; ::_thesis: verum end; theorem :: LFUZZY_1:19 for X being non empty set for R being RMembership_Func of X,X holds min (R,(converse R)) is symmetric proof let X be non empty set ; ::_thesis: for R being RMembership_Func of X,X holds min (R,(converse R)) is symmetric let R be RMembership_Func of X,X; ::_thesis: min (R,(converse R)) is symmetric set S = min (R,(converse R)); let x, y be Element of X; :: according to LFUZZY_1:def_5 ::_thesis: (min (R,(converse R))) . (x,y) = (min (R,(converse R))) . (y,x) thus (min (R,(converse R))) . (x,y) = (min (R,(converse R))) . [x,y] .= min ((R . (x,y)),((converse R) . (x,y))) by FUZZY_1:def_3 .= min ((R . (x,y)),(R . (y,x))) by FUZZY_4:26 .= min (((converse R) . (y,x)),(R . (y,x))) by FUZZY_4:26 .= (min (R,(converse R))) . [y,x] by FUZZY_1:def_3 .= (min (R,(converse R))) . (y,x) ; ::_thesis: verum end; theorem :: LFUZZY_1:20 for X being non empty set for R, R9 being RMembership_Func of X,X st R9 is symmetric & R9 c= holds R9 c= proof let X be non empty set ; ::_thesis: for R, R9 being RMembership_Func of X,X st R9 is symmetric & R9 c= holds R9 c= let R, T be RMembership_Func of X,X; ::_thesis: ( T is symmetric & T c= implies T c= ) assume that A1: T is symmetric and A2: T c= ; ::_thesis: T c= let x, y be Element of X; :: according to LFUZZY_1:def_1 ::_thesis: (max (R,(converse R))) . (x,y) <= T . (x,y) R . [y,x] <= T . [y,x] by A2, FUZZY_1:def_2; then R . (y,x) <= T . (y,x) ; then A3: R . (y,x) <= T . (x,y) by A1, Def5; R . [x,y] <= T . [x,y] by A2, FUZZY_1:def_2; then max ((R . (x,y)),(R . (y,x))) <= T . (x,y) by A3, XXREAL_0:28; then max ((R . (x,y)),((converse R) . (x,y))) <= T . (x,y) by FUZZY_4:26; then max ((R . [x,y]),((converse R) . [x,y])) <= T . [x,y] ; hence (max (R,(converse R))) . (x,y) <= T . (x,y) by FUZZY_1:def_4; ::_thesis: verum end; theorem :: LFUZZY_1:21 for X being non empty set for R, R9 being RMembership_Func of X,X st R9 is symmetric & R c= holds min (R,(converse R)) c= proof let X be non empty set ; ::_thesis: for R, R9 being RMembership_Func of X,X st R9 is symmetric & R c= holds min (R,(converse R)) c= let R, T be RMembership_Func of X,X; ::_thesis: ( T is symmetric & R c= implies min (R,(converse R)) c= ) assume that A1: T is symmetric and A2: R c= ; ::_thesis: min (R,(converse R)) c= let x, y be Element of X; :: according to LFUZZY_1:def_1 ::_thesis: T . (x,y) <= (min (R,(converse R))) . (x,y) T . [y,x] <= R . [y,x] by A2, FUZZY_1:def_2; then T . (y,x) <= R . (y,x) ; then A3: T . (x,y) <= R . (y,x) by A1, Def5; T . [x,y] <= R . [x,y] by A2, FUZZY_1:def_2; then T . (x,y) <= min ((R . (x,y)),(R . (y,x))) by A3, XXREAL_0:20; then T . (x,y) <= min ((R . (x,y)),((converse R) . (x,y))) by FUZZY_4:26; then T . [x,y] <= min ((R . [x,y]),((converse R) . [x,y])) ; hence T . (x,y) <= (min (R,(converse R))) . (x,y) by FUZZY_1:def_3; ::_thesis: verum end; begin definition let X be non empty set ; let R be RMembership_Func of X,X; let n be Nat; funcn iter R -> RMembership_Func of X,X means :Def9: :: LFUZZY_1:def 9 ex F being Function of NAT,(Funcs ([:X,X:],[.0,1.])) st ( it = F . n & F . 0 = Imf (X,X) & ( for k being Nat ex Q being RMembership_Func of X,X st ( F . k = Q & F . (k + 1) = Q (#) R ) ) ); existence ex b1 being RMembership_Func of X,X ex F being Function of NAT,(Funcs ([:X,X:],[.0,1.])) st ( b1 = F . n & F . 0 = Imf (X,X) & ( for k being Nat ex Q being RMembership_Func of X,X st ( F . k = Q & F . (k + 1) = Q (#) R ) ) ) proof reconsider n9 = n as Element of NAT by ORDINAL1:def_12; set D = the carrier of (FuzzyLattice [:X,X:]); defpred S1[ set , set , set ] means ex Q being Element of the carrier of (FuzzyLattice [:X,X:]) st ( \$2 = Q & \$3 = (@ Q) (#) R ); A1: for k being Element of NAT for x being Element of the carrier of (FuzzyLattice [:X,X:]) ex y being Element of the carrier of (FuzzyLattice [:X,X:]) st S1[k,x,y] proof let k be Element of NAT ; ::_thesis: for x being Element of the carrier of (FuzzyLattice [:X,X:]) ex y being Element of the carrier of (FuzzyLattice [:X,X:]) st S1[k,x,y] let Q be Element of the carrier of (FuzzyLattice [:X,X:]); ::_thesis: ex y being Element of the carrier of (FuzzyLattice [:X,X:]) st S1[k,Q,y] set y = (@ Q) (#) R; reconsider y9 = ([:X,X:],((@ Q) (#) R)) @ as Element of the carrier of (FuzzyLattice [:X,X:]) ; take y9 ; ::_thesis: S1[k,Q,y9] thus S1[k,Q,y9] by LFUZZY_0:def_6; ::_thesis: verum end; consider F being Function of NAT, the carrier of (FuzzyLattice [:X,X:]) such that A2: ( F . 0 = ([:X,X:],(Imf (X,X))) @ & ( for k being Element of NAT holds S1[k,F . k,F . (k + 1)] ) ) from RECDEF_1:sch_2(A1); reconsider F = F as Function of NAT,(Funcs ([:X,X:],[.0,1.])) by LFUZZY_0:14; reconsider IT = F . n9 as Element of (FuzzyLattice [:X,X:]) by LFUZZY_0:14; reconsider IT9 = @ IT as RMembership_Func of X,X ; take IT9 ; ::_thesis: ex F being Function of NAT,(Funcs ([:X,X:],[.0,1.])) st ( IT9 = F . n & F . 0 = Imf (X,X) & ( for k being Nat ex Q being RMembership_Func of X,X st ( F . k = Q & F . (k + 1) = Q (#) R ) ) ) thus ex F being Function of NAT,(Funcs ([:X,X:],[.0,1.])) st ( IT9 = F . n & F . 0 = Imf (X,X) & ( for k being Nat ex Q being RMembership_Func of X,X st ( F . k = Q & F . (k + 1) = Q (#) R ) ) ) ::_thesis: verum proof take F ; ::_thesis: ( IT9 = F . n & F . 0 = Imf (X,X) & ( for k being Nat ex Q being RMembership_Func of X,X st ( F . k = Q & F . (k + 1) = Q (#) R ) ) ) thus IT9 = F . n by LFUZZY_0:def_5; ::_thesis: ( F . 0 = Imf (X,X) & ( for k being Nat ex Q being RMembership_Func of X,X st ( F . k = Q & F . (k + 1) = Q (#) R ) ) ) thus F . 0 = Imf (X,X) by A2, LFUZZY_0:def_6; ::_thesis: for k being Nat ex Q being RMembership_Func of X,X st ( F . k = Q & F . (k + 1) = Q (#) R ) thus for k being Nat ex Q being RMembership_Func of X,X st ( F . k = Q & F . (k + 1) = Q (#) R ) ::_thesis: verum proof let k be Nat; ::_thesis: ex Q being RMembership_Func of X,X st ( F . k = Q & F . (k + 1) = Q (#) R ) reconsider n = k as Element of NAT by ORDINAL1:def_12; reconsider Q9 = F . n as Element of the carrier of (FuzzyLattice [:X,X:]) by LFUZZY_0:14; reconsider Q = @ Q9 as RMembership_Func of X,X ; take Q ; ::_thesis: ( F . k = Q & F . (k + 1) = Q (#) R ) thus F . k = Q by LFUZZY_0:def_5; ::_thesis: F . (k + 1) = Q (#) R S1[n,F . n,F . (n + 1)] by A2; hence F . (k + 1) = Q (#) R ; ::_thesis: verum end; end; end; uniqueness for b1, b2 being RMembership_Func of X,X st ex F being Function of NAT,(Funcs ([:X,X:],[.0,1.])) st ( b1 = F . n & F . 0 = Imf (X,X) & ( for k being Nat ex Q being RMembership_Func of X,X st ( F . k = Q & F . (k + 1) = Q (#) R ) ) ) & ex F being Function of NAT,(Funcs ([:X,X:],[.0,1.])) st ( b2 = F . n & F . 0 = Imf (X,X) & ( for k being Nat ex Q being RMembership_Func of X,X st ( F . k = Q & F . (k + 1) = Q (#) R ) ) ) holds b1 = b2 proof let S, T be RMembership_Func of X,X; ::_thesis: ( ex F being Function of NAT,(Funcs ([:X,X:],[.0,1.])) st ( S = F . n & F . 0 = Imf (X,X) & ( for k being Nat ex Q being RMembership_Func of X,X st ( F . k = Q & F . (k + 1) = Q (#) R ) ) ) & ex F being Function of NAT,(Funcs ([:X,X:],[.0,1.])) st ( T = F . n & F . 0 = Imf (X,X) & ( for k being Nat ex Q being RMembership_Func of X,X st ( F . k = Q & F . (k + 1) = Q (#) R ) ) ) implies S = T ) given F being Function of NAT,(Funcs ([:X,X:],[.0,1.])) such that A3: S = F . n and A4: F . 0 = Imf (X,X) and A5: for k being Nat ex Q being RMembership_Func of X,X st ( F . k = Q & F . (k + 1) = Q (#) R ) ; ::_thesis: ( for F being Function of NAT,(Funcs ([:X,X:],[.0,1.])) holds ( not T = F . n or not F . 0 = Imf (X,X) or ex k being Nat st for Q being RMembership_Func of X,X holds ( not F . k = Q or not F . (k + 1) = Q (#) R ) ) or S = T ) given G being Function of NAT,(Funcs ([:X,X:],[.0,1.])) such that A6: T = G . n and A7: G . 0 = Imf (X,X) and A8: for k being Nat ex Q being RMembership_Func of X,X st ( G . k = Q & G . (k + 1) = Q (#) R ) ; ::_thesis: S = T defpred S1[ Nat] means F . \$1 = G . \$1; A9: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A10: F . k = G . k ; ::_thesis: S1[k + 1] ( ex Q being RMembership_Func of X,X st ( G . k = Q & G . (k + 1) = Q (#) R ) & ex Q9 being RMembership_Func of X,X st ( F . k = Q9 & F . (k + 1) = Q9 (#) R ) ) by A5, A8; hence S1[k + 1] by A10; ::_thesis: verum end; A11: S1[ 0 ] by A4, A7; for k being Nat holds S1[k] from NAT_1:sch_2(A11, A9); hence S = T by A3, A6; ::_thesis: verum end; end; :: deftheorem Def9 defines iter LFUZZY_1:def_9_:_ for X being non empty set for R being RMembership_Func of X,X for n being Nat for b4 being RMembership_Func of X,X holds ( b4 = n iter R iff ex F being Function of NAT,(Funcs ([:X,X:],[.0,1.])) st ( b4 = F . n & F . 0 = Imf (X,X) & ( for k being Nat ex Q being RMembership_Func of X,X st ( F . k = Q & F . (k + 1) = Q (#) R ) ) ) ); theorem Th22: :: LFUZZY_1:22 for X being non empty set for R being RMembership_Func of X,X holds (Imf (X,X)) (#) R = R proof let X be non empty set ; ::_thesis: for R being RMembership_Func of X,X holds (Imf (X,X)) (#) R = R let R be RMembership_Func of X,X; ::_thesis: (Imf (X,X)) (#) R = R A1: 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 ; ::_thesis: ( [x,y] in dom ((Imf (X,X)) (#) R) implies ((Imf (X,X)) (#) R) . (x,y) = R . (x,y) ) assume [x,y] in dom ((Imf (X,X)) (#) R) ; ::_thesis: ((Imf (X,X)) (#) R) . (x,y) = R . (x,y) then reconsider x = x, y = y as Element of X by ZFMISC_1:87; set S = { (((Imf (X,X)) . (x,z)) "/\" (R . (z,y))) where z is Element of X : verum } ; for c being Element of (RealPoset [.0,1.]) st c in { (((Imf (X,X)) . (x,z)) "/\" (R . (z,y))) where z is Element of X : verum } holds c <<= R . [x,y] proof let c be Element of (RealPoset [.0,1.]); ::_thesis: ( c in { (((Imf (X,X)) . (x,z)) "/\" (R . (z,y))) where z is Element of X : verum } implies c <<= R . [x,y] ) assume c in { (((Imf (X,X)) . (x,z)) "/\" (R . (z,y))) where z is Element of X : verum } ; ::_thesis: c <<= R . [x,y] then consider z being Element of X such that A2: c = ((Imf (X,X)) . (x,z)) "/\" (R . (z,y)) ; percases ( x = z or x <> z ) ; supposeA3: x = z ; ::_thesis: c <<= R . [x,y] A4: R . (z,y) <= 1 by FUZZY_4:4; c = min ((R . [z,y]),1) by A2, A3, FUZZY_4:25 .= R . [x,y] by A3, A4, XXREAL_0:def_9 ; hence c <<= R . [x,y] by LFUZZY_0:3; ::_thesis: verum end; supposeA5: x <> z ; ::_thesis: c <<= R . [x,y] A6: 0 <= R . (z,y) by FUZZY_4:4; c = min ((R . [z,y]),0) by A2, A5, FUZZY_4:25 .= 0 by A6, XXREAL_0:def_9 ; then c <= R . (x,y) by FUZZY_4:4; hence c <<= R . [x,y] by LFUZZY_0:3; ::_thesis: verum end; end; end; then A7: ( ((Imf (X,X)) (#) R) . (x,y) = "\/" ( { (((Imf (X,X)) . (x,z)) "/\" (R . (z,y))) where z is Element of X : verum } ,(RealPoset [.0,1.])) & R . (x,y) is_>=_than { (((Imf (X,X)) . (x,z)) "/\" (R . (z,y))) where z is Element of X : verum } ) by LATTICE3:def_9, LFUZZY_0:22; for b being Element of (RealPoset [.0,1.]) st b is_>=_than { (((Imf (X,X)) . (x,z)) "/\" (R . (z,y))) where z is Element of X : verum } holds R . (x,y) <<= b proof let b be Element of (RealPoset [.0,1.]); ::_thesis: ( b is_>=_than { (((Imf (X,X)) . (x,z)) "/\" (R . (z,y))) where z is Element of X : verum } implies R . (x,y) <<= b ) A8: R . (x,y) <= 1 by FUZZY_4:4; ((Imf (X,X)) . (x,x)) "/\" (R . [x,y]) = min (1,(R . (x,y))) by FUZZY_4:25 .= R . [x,y] by A8, XXREAL_0:def_9 ; then A9: R . (x,y) in { (((Imf (X,X)) . (x,z)) "/\" (R . (z,y))) where z is Element of X : verum } ; assume b is_>=_than { (((Imf (X,X)) . (x,z)) "/\" (R . (z,y))) where z is Element of X : verum } ; ::_thesis: R . (x,y) <<= b hence R . (x,y) <<= b by A9, LATTICE3:def_9; ::_thesis: verum end; hence ((Imf (X,X)) (#) R) . (x,y) = R . (x,y) by A7, YELLOW_0:32; ::_thesis: verum end; dom ((Imf (X,X)) (#) R) = [:X,X:] by FUNCT_2:def_1 .= dom R by FUNCT_2:def_1 ; hence (Imf (X,X)) (#) R = R by A1, BINOP_1:20; ::_thesis: verum end; theorem Th23: :: LFUZZY_1:23 for X being non empty set for R being RMembership_Func of X,X holds R (#) (Imf (X,X)) = R proof let X be non empty set ; ::_thesis: for R being RMembership_Func of X,X holds R (#) (Imf (X,X)) = R let R be RMembership_Func of X,X; ::_thesis: R (#) (Imf (X,X)) = R A1: 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 ; ::_thesis: ( [x,y] in dom (R (#) (Imf (X,X))) implies (R (#) (Imf (X,X))) . (x,y) = R . (x,y) ) assume [x,y] in dom (R (#) (Imf (X,X))) ; ::_thesis: (R (#) (Imf (X,X))) . (x,y) = R . (x,y) then reconsider x = x, y = y as Element of X by ZFMISC_1:87; set S = { ((R . (x,z)) "/\" ((Imf (X,X)) . (z,y))) where z is Element of X : verum } ; for c being Element of (RealPoset [.0,1.]) st c in { ((R . (x,z)) "/\" ((Imf (X,X)) . (z,y))) where z is Element of X : verum } holds c <<= R . [x,y] proof let c be Element of (RealPoset [.0,1.]); ::_thesis: ( c in { ((R . (x,z)) "/\" ((Imf (X,X)) . (z,y))) where z is Element of X : verum } implies c <<= R . [x,y] ) assume c in { ((R . (x,z)) "/\" ((Imf (X,X)) . (z,y))) where z is Element of X : verum } ; ::_thesis: c <<= R . [x,y] then consider z being Element of X such that A2: c = (R . (x,z)) "/\" ((Imf (X,X)) . (z,y)) ; percases ( y = z or not y = z ) ; supposeA3: y = z ; ::_thesis: c <<= R . [x,y] A4: R . (x,z) <= 1 by FUZZY_4:4; c = min ((R . [x,z]),1) by A2, A3, FUZZY_4:25 .= R . [x,y] by A3, A4, XXREAL_0:def_9 ; hence c <<= R . [x,y] by LFUZZY_0:3; ::_thesis: verum end; supposeA5: not y = z ; ::_thesis: c <<= R . [x,y] A6: 0 <= R . (x,z) by FUZZY_4:4; c = min ((R . [x,z]),0) by A2, A5, FUZZY_4:25 .= 0 by A6, XXREAL_0:def_9 ; then c <= R . (x,y) by FUZZY_4:4; hence c <<= R . [x,y] by LFUZZY_0:3; ::_thesis: verum end; end; end; then A7: ( (R (#) (Imf (X,X))) . (x,y) = "\/" ( { ((R . (x,z)) "/\" ((Imf (X,X)) . (z,y))) where z is Element of X : verum } ,(RealPoset [.0,1.])) & R . (x,y) is_>=_than { ((R . (x,z)) "/\" ((Imf (X,X)) . (z,y))) where z is Element of X : verum } ) by LATTICE3:def_9, LFUZZY_0:22; for b being Element of (RealPoset [.0,1.]) st b is_>=_than { ((R . (x,z)) "/\" ((Imf (X,X)) . (z,y))) where z is Element of X : verum } holds R . (x,y) <<= b proof let b be Element of (RealPoset [.0,1.]); ::_thesis: ( b is_>=_than { ((R . (x,z)) "/\" ((Imf (X,X)) . (z,y))) where z is Element of X : verum } implies R . (x,y) <<= b ) A8: R . (x,y) <= 1 by FUZZY_4:4; (R . [x,y]) "/\" ((Imf (X,X)) . (y,y)) = min ((R . [x,y]),1) by FUZZY_4:25 .= R . [x,y] by A8, XXREAL_0:def_9 ; then A9: R . (x,y) in { ((R . (x,z)) "/\" ((Imf (X,X)) . (z,y))) where z is Element of X : verum } ; assume b is_>=_than { ((R . (x,z)) "/\" ((Imf (X,X)) . (z,y))) where z is Element of X : verum } ; ::_thesis: R . (x,y) <<= b hence R . (x,y) <<= b by A9, LATTICE3:def_9; ::_thesis: verum end; hence (R (#) (Imf (X,X))) . (x,y) = R . (x,y) by A7, YELLOW_0:32; ::_thesis: verum end; dom (R (#) (Imf (X,X))) = [:X,X:] by FUNCT_2:def_1 .= dom R by FUNCT_2:def_1 ; hence R (#) (Imf (X,X)) = R by A1, BINOP_1:20; ::_thesis: verum end; theorem Th24: :: LFUZZY_1:24 for X being non empty set for R being RMembership_Func of X,X holds 0 iter R = Imf (X,X) proof let X be non empty set ; ::_thesis: for R being RMembership_Func of X,X holds 0 iter R = Imf (X,X) let R be RMembership_Func of X,X; ::_thesis: 0 iter R = Imf (X,X) ex F being Function of NAT,(Funcs ([:X,X:],[.0,1.])) st ( 0 iter R = F . 0 & F . 0 = Imf (X,X) & ( for k being Nat ex Q being RMembership_Func of X,X st ( F . k = Q & F . (k + 1) = Q (#) R ) ) ) by Def9; hence 0 iter R = Imf (X,X) ; ::_thesis: verum end; theorem Th25: :: LFUZZY_1:25 for X being non empty set for R being RMembership_Func of X,X holds 1 iter R = R proof let X be non empty set ; ::_thesis: for R being RMembership_Func of X,X holds 1 iter R = R let R be RMembership_Func of X,X; ::_thesis: 1 iter R = R consider F being Function of NAT,(Funcs ([:X,X:],[.0,1.])) such that A1: ( 1 iter R = F . 1 & F . 0 = Imf (X,X) ) and A2: for k being Nat ex Q being RMembership_Func of X,X st ( F . k = Q & F . (k + 1) = Q (#) R ) by Def9; ex Q being RMembership_Func of X,X st ( F . 0 = Q & F . (0 + 1) = Q (#) R ) by A2; hence 1 iter R = R by A1, Th22; ::_thesis: verum end; theorem Th26: :: LFUZZY_1:26 for X being non empty set for R being RMembership_Func of X,X for n being Nat holds (n + 1) iter R = (n iter R) (#) R proof let X be non empty set ; ::_thesis: for R being RMembership_Func of X,X for n being Nat holds (n + 1) iter R = (n iter R) (#) R let R be RMembership_Func of X,X; ::_thesis: for n being Nat holds (n + 1) iter R = (n iter R) (#) R let n be Nat; ::_thesis: (n + 1) iter R = (n iter R) (#) R 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 Nat ex Q being RMembership_Func of X,X st ( f . k = Q & f . (k + 1) = Q (#) R ) by Def9; ex Q being RMembership_Func of X,X st ( f . n = Q & f . (n + 1) = Q (#) R ) by A2; hence (n + 1) iter R = (n iter R) (#) R by A1, A2, Def9; ::_thesis: verum end; theorem Th27: :: LFUZZY_1:27 for X being non empty set for R being RMembership_Func of X,X for m, n being Nat holds (m + n) iter R = (m iter R) (#) (n iter R) proof let X be non empty set ; ::_thesis: for R being RMembership_Func of X,X for m, n being Nat holds (m + n) iter R = (m iter R) (#) (n iter R) let R be RMembership_Func of X,X; ::_thesis: for m, n being Nat holds (m + n) iter R = (m iter R) (#) (n iter R) let m, n be Nat; ::_thesis: (m + n) iter R = (m iter R) (#) (n iter R) defpred S1[ Nat] means (m + \$1) iter R = (m iter R) (#) (\$1 iter R); A1: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A2: (m + n) iter R = (m iter R) (#) (n iter R) ; ::_thesis: S1[n + 1] thus (m iter R) (#) ((n + 1) iter R) = (m iter R) (#) ((n iter R) (#) R) by Th26 .= ((m + n) iter R) (#) R by A2, LFUZZY_0:23 .= ((m + n) + 1) iter R by Th26 .= (m + (n + 1)) iter R ; ::_thesis: verum end; (m iter R) (#) (0 iter R) = (m iter R) (#) (Imf (X,X)) by Th24 .= m iter R by Th23 ; then A3: S1[ 0 ] ; for m being Nat holds S1[m] from NAT_1:sch_2(A3, A1); hence (m + n) iter R = (m iter R) (#) (n iter R) ; ::_thesis: verum end; theorem :: LFUZZY_1:28 for X being non empty set for R being RMembership_Func of X,X for m, n being Nat holds (m * n) iter R = m iter (n iter R) proof let X be non empty set ; ::_thesis: for R being RMembership_Func of X,X for m, n being Nat holds (m * n) iter R = m iter (n iter R) let R be RMembership_Func of X,X; ::_thesis: for m, n being Nat holds (m * n) iter R = m iter (n iter R) let m, n be Nat; ::_thesis: (m * n) iter R = m iter (n iter R) defpred S1[ Nat] means (\$1 * n) iter R = \$1 iter (n iter R); A1: for m being Nat st S1[m] holds S1[m + 1] proof let m be Nat; ::_thesis: ( S1[m] implies S1[m + 1] ) assume A2: (m * n) iter R = m iter (n iter R) ; ::_thesis: S1[m + 1] A3: (m + 1) iter (n iter R) = (m iter (n iter R)) (#) (1 iter (n iter R)) by Th27 .= (m iter (n iter R)) (#) (n iter R) by Th25 ; ((m + 1) * n) iter R = ((m * n) + (1 * n)) iter R .= (m iter (n iter R)) (#) (n iter R) by A2, Th27 ; hence S1[m + 1] by A3; ::_thesis: verum end; (0 * n) iter R = Imf (X,X) by Th24 .= 0 iter (n iter R) by Th24 ; then A4: S1[ 0 ] ; for m being Nat holds S1[m] from NAT_1:sch_2(A4, A1); hence (m * n) iter R = m iter (n iter R) ; ::_thesis: verum 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 :: LFUZZY_1:def 10 "\/" ( { (n iter R) where n is Element of NAT : n > 0 } ,(FuzzyLattice [:X,X:])); coherence "\/" ( { (n iter R) where n is Element of NAT : n > 0 } ,(FuzzyLattice [:X,X:])) is RMembership_Func of X,X proof set S = "\/" ( { (n iter R) where n is Element of NAT : n > 0 } ,(FuzzyLattice [:X,X:])); "\/" ( { (n iter R) where n is Element of NAT : n > 0 } ,(FuzzyLattice [:X,X:])) = @ ("\/" ( { (n iter R) where n is Element of NAT : n > 0 } ,(FuzzyLattice [:X,X:]))) by LFUZZY_0:def_5; hence "\/" ( { (n iter R) where n is Element of NAT : n > 0 } ,(FuzzyLattice [:X,X:])) is RMembership_Func of X,X ; ::_thesis: verum end; end; :: deftheorem defines TrCl LFUZZY_1:def_10_:_ for X being non empty set for R being RMembership_Func of X,X holds TrCl R = "\/" ( { (n iter R) where n is Element of NAT : n > 0 } ,(FuzzyLattice [:X,X:])); theorem Th29: :: LFUZZY_1:29 for X being non empty set for R being RMembership_Func of X,X for x, y being Element of X holds (TrCl R) . [x,y] = "\/" ((pi ( { (n iter R) where n is Element of NAT : n > 0 } ,[x,y])),(RealPoset [.0,1.])) proof let X be non empty set ; ::_thesis: for R being RMembership_Func of X,X for x, y being Element of X holds (TrCl R) . [x,y] = "\/" ((pi ( { (n iter R) where n is Element of NAT : n > 0 } ,[x,y])),(RealPoset [.0,1.])) let R be RMembership_Func of X,X; ::_thesis: for x, y being Element of X holds (TrCl R) . [x,y] = "\/" ((pi ( { (n iter R) where n is Element of NAT : n > 0 } ,[x,y])),(RealPoset [.0,1.])) set Q = { (n iter R) where n is Element of NAT : n > 0 } ; { (n iter R) where n is Element of NAT : n > 0 } c= the carrier of (FuzzyLattice [:X,X:]) proof let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in { (n iter R) where n is Element of NAT : n > 0 } or t in the carrier of (FuzzyLattice [:X,X:]) ) assume t in { (n iter R) where n is Element of NAT : n > 0 } ; ::_thesis: t in the carrier of (FuzzyLattice [:X,X:]) then ex n being Element of NAT st ( t = n iter R & n > 0 ) ; then reconsider t = t as Membership_Func of [:X,X:] ; ([:X,X:],t) @ is Element of (FuzzyLattice [:X,X:]) ; then reconsider t = t as Element of (FuzzyLattice [:X,X:]) by LFUZZY_0:def_6; t in the carrier of (FuzzyLattice [:X,X:]) ; hence t in the carrier of (FuzzyLattice [:X,X:]) ; ::_thesis: verum end; then reconsider Q = { (n iter R) where n is Element of NAT : n > 0 } as Subset of (FuzzyLattice [:X,X:]) ; let x, z be Element of X; ::_thesis: (TrCl R) . [x,z] = "\/" ((pi ( { (n iter R) where n is Element of NAT : n > 0 } ,[x,z])),(RealPoset [.0,1.])) reconsider i = [x,z] as Element of [:X,X:] ; A1: for a being Element of [:X,X:] holds ([:X,X:] --> (RealPoset [.0,1.])) . a is complete LATTICE by FUNCOP_1:7; FuzzyLattice [:X,X:] = (RealPoset [.0,1.]) |^ [:X,X:] by LFUZZY_0:def_4 .= product ([:X,X:] --> (RealPoset [.0,1.])) by YELLOW_1:def_5 ; then (sup Q) . i = "\/" ((pi (Q,i)),(([:X,X:] --> (RealPoset [.0,1.])) . i)) by A1, WAYBEL_3:32; hence (TrCl R) . [x,z] = "\/" ((pi ( { (n iter R) where n is Element of NAT : n > 0 } ,[x,z])),(RealPoset [.0,1.])) by FUNCOP_1:7; ::_thesis: verum end; theorem Th30: :: LFUZZY_1:30 for X being non empty set for R being RMembership_Func of X,X holds TrCl R c= proof 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 proof 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 set 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; hence TrCl R c= by FUZZY_1:def_2; ::_thesis: verum end; theorem Th31: :: LFUZZY_1:31 for X being non empty set for R being RMembership_Func of X,X for n being Nat st n > 0 holds TrCl R c= proof 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 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:]; ::_thesis: (n9 iter R) . c <= (TrCl R) . c consider x, y being set 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; hence TrCl R c= by FUZZY_1:def_2; ::_thesis: verum end; theorem Th32: :: LFUZZY_1:32 for X being non empty set for Q being Subset of (FuzzyLattice X) for x being Element of X holds ("\/" (Q,(FuzzyLattice X))) . x = "\/" ((pi (Q,x)),(RealPoset [.0,1.])) proof let X be non empty set ; ::_thesis: for Q being Subset of (FuzzyLattice X) for x being Element of X holds ("\/" (Q,(FuzzyLattice X))) . x = "\/" ((pi (Q,x)),(RealPoset [.0,1.])) let Q be Subset of (FuzzyLattice X); ::_thesis: for x being Element of X holds ("\/" (Q,(FuzzyLattice X))) . x = "\/" ((pi (Q,x)),(RealPoset [.0,1.])) let x be Element of X; ::_thesis: ("\/" (Q,(FuzzyLattice X))) . x = "\/" ((pi (Q,x)),(RealPoset [.0,1.])) A1: for a being Element of X holds (X --> (RealPoset [.0,1.])) . a is complete LATTICE by FUNCOP_1:7; FuzzyLattice X = (RealPoset [.0,1.]) |^ X by LFUZZY_0:def_4 .= product (X --> (RealPoset [.0,1.])) by YELLOW_1:def_5 ; then (sup Q) . x = "\/" ((pi (Q,x)),((X --> (RealPoset [.0,1.])) . x)) by A1, WAYBEL_3:32; hence ("\/" (Q,(FuzzyLattice X))) . x = "\/" ((pi (Q,x)),(RealPoset [.0,1.])) by FUNCOP_1:7; ::_thesis: verum end; Lm2: for X being non empty set for R being RMembership_Func of X,X for Q being Subset of (FuzzyLattice [:X,X:]) for x, z being Element of X holds { ((R . (x,y)) "/\" ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . (y,z))) where y is Element of X : verum } = { ((R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))) where y is Element of X : verum } proof let X be non empty set ; ::_thesis: for R being RMembership_Func of X,X for Q being Subset of (FuzzyLattice [:X,X:]) for x, z being Element of X holds { ((R . (x,y)) "/\" ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . (y,z))) where y is Element of X : verum } = { ((R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))) where y is Element of X : verum } let R be RMembership_Func of X,X; ::_thesis: for Q being Subset of (FuzzyLattice [:X,X:]) for x, z being Element of X holds { ((R . (x,y)) "/\" ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . (y,z))) where y is Element of X : verum } = { ((R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))) where y is Element of X : verum } let Q be Subset of (FuzzyLattice [:X,X:]); ::_thesis: for x, z being Element of X holds { ((R . (x,y)) "/\" ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . (y,z))) where y is Element of X : verum } = { ((R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))) where y is Element of X : verum } let x, z be Element of X; ::_thesis: { ((R . (x,y)) "/\" ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . (y,z))) where y is Element of X : verum } = { ((R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))) where y is Element of X : verum } defpred S1[ Element of X] means verum; deffunc H1( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = (R . (x,\$1)) "/\" ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . (\$1,z)); deffunc H2( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = (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; ::_thesis: (R . [x,y]) "/\" ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . [y,z]) = (R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.]))) (@ ("\/" (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 Th32 ; hence (R . [x,y]) "/\" ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . [y,z]) = (R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.]))) ; ::_thesis: verum end; then A1: for y being Element of X holds H1(y) = H2(y) ; thus { H1(y) where y is Element of X : S1[y] } = { H2(y9) where y9 is Element of X : S1[y9] } from FRAENKEL:sch_5(A1); ::_thesis: verum end; theorem Th33: :: LFUZZY_1:33 for R being complete Heyting LATTICE for X being Subset of R for y being 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; ::_thesis: for X being Subset of R for y being Element of R holds y "/\" ("\/" (X,R)) = "\/" ( { (y "/\" x) where x is Element of R : x in X } ,R) let X be Subset of R; ::_thesis: for y being Element of R holds y "/\" ("\/" (X,R)) = "\/" ( { (y "/\" x) where x is Element of R : x in X } ,R) let y be Element of R; ::_thesis: y "/\" ("\/" (X,R)) = "\/" ( { (y "/\" x) where x is Element of R : x in X } ,R) for z being Element of R holds z "/\" is lower_adjoint by WAYBEL_1:def_19; hence y "/\" ("\/" (X,R)) = "\/" ( { (y "/\" x) where x is Element of R : x in X } ,R) by WAYBEL_1:64; ::_thesis: verum end; Lm3: for X being non empty set for R being RMembership_Func of X,X for Q being Subset of (FuzzyLattice [:X,X:]) for x, z being Element of X holds { ((R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))) where y is Element of X : verum } = { ("\/" ( { ((R . [x,y9]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y9,z]) } ,(RealPoset [.0,1.]))) where y9 is Element of X : verum } proof let X be non empty set ; ::_thesis: for R being RMembership_Func of X,X for Q being Subset of (FuzzyLattice [:X,X:]) for x, z being Element of X holds { ((R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))) where y is Element of X : verum } = { ("\/" ( { ((R . [x,y9]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y9,z]) } ,(RealPoset [.0,1.]))) where y9 is Element of X : verum } let R be RMembership_Func of X,X; ::_thesis: for Q being Subset of (FuzzyLattice [:X,X:]) for x, z being Element of X holds { ((R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))) where y is Element of X : verum } = { ("\/" ( { ((R . [x,y9]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y9,z]) } ,(RealPoset [.0,1.]))) where y9 is Element of X : verum } let Q be Subset of (FuzzyLattice [:X,X:]); ::_thesis: for x, z being Element of X holds { ((R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))) where y is Element of X : verum } = { ("\/" ( { ((R . [x,y9]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y9,z]) } ,(RealPoset [.0,1.]))) where y9 is Element of X : verum } let x, z be Element of X; ::_thesis: { ((R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))) where y is Element of X : verum } = { ("\/" ( { ((R . [x,y9]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y9,z]) } ,(RealPoset [.0,1.]))) where y9 is Element of X : verum } defpred S1[ Element of X] means verum; deffunc H1( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = (R . [x,\$1]) "/\" ("\/" ((pi (Q,[\$1,z])),(RealPoset [.0,1.]))); deffunc H2( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = "\/" ( { ((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; ::_thesis: (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.])) FuzzyLattice [:X,X:] = (RealPoset [.0,1.]) |^ [:X,X:] by LFUZZY_0:def_4 .= product ([:X,X:] --> (RealPoset [.0,1.])) by YELLOW_1:def_5 ; then reconsider Q = Q as Subset of (product ([:X,X:] --> (RealPoset [.0,1.]))) ; pi (Q,[y,z]) is Subset of (RealPoset [.0,1.]) by FUNCOP_1:7; hence (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.])) by Th33; ::_thesis: verum end; then A1: for y being Element of X holds H1(y) = H2(y) ; { H1(y) where y is Element of X : S1[y] } = { H2(y) where y is Element of X : S1[y] } from FRAENKEL:sch_5(A1); hence { ((R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))) where y is Element of X : verum } = { ("\/" ( { ((R . [x,y9]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y9,z]) } ,(RealPoset [.0,1.]))) where y9 is Element of X : verum } ; ::_thesis: verum end; Lm4: for X being non empty set for R being RMembership_Func of X,X for Q being Subset of (FuzzyLattice [:X,X:]) for 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 : verum } = { ("\/" ( { ((R . [x,y9]) "/\" (r . [y9,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.]))) where y9 is Element of X : verum } proof let X be non empty set ; ::_thesis: for R being RMembership_Func of X,X for Q being Subset of (FuzzyLattice [:X,X:]) for 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 : verum } = { ("\/" ( { ((R . [x,y9]) "/\" (r . [y9,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.]))) where y9 is Element of X : verum } let R be RMembership_Func of X,X; ::_thesis: for Q being Subset of (FuzzyLattice [:X,X:]) for 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 : verum } = { ("\/" ( { ((R . [x,y9]) "/\" (r . [y9,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.]))) where y9 is Element of X : verum } let Q be Subset of (FuzzyLattice [:X,X:]); ::_thesis: for 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 : verum } = { ("\/" ( { ((R . [x,y9]) "/\" (r . [y9,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.]))) where y9 is Element of X : verum } let x, z be Element of X; ::_thesis: { ("\/" ( { ((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 : verum } = { ("\/" ( { ((R . [x,y9]) "/\" (r . [y9,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.]))) where y9 is Element of X : verum } set RP = RealPoset [.0,1.]; set FL = FuzzyLattice [:X,X:]; defpred S1[ Element of X] means verum; deffunc H1( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = "\/" ( { ((R . [x,\$1]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[\$1,z]) } ,(RealPoset [.0,1.])); deffunc H2( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = "\/" ( { ((R . [x,\$1]) "/\" (r . [\$1,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.])); for y 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.])) = "\/" ( { ((R . [x,y]) "/\" (r . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.])) proof let y be Element of X; ::_thesis: "\/" ( { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y,z]) } ,(RealPoset [.0,1.])) = "\/" ( { ((R . [x,y]) "/\" (r . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.])) set A = { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y,z]) } ; set B = { ((R . [x,y]) "/\" (r . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ; A1: { ((R . [x,y]) "/\" (r . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } c= { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y,z]) } proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ((R . [x,y]) "/\" (r . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } or a in { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y,z]) } ) assume a in { ((R . [x,y]) "/\" (r . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ; ::_thesis: a in { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y,z]) } then consider r being Element of (FuzzyLattice [:X,X:]) such that A2: a = (R . [x,y]) "/\" (r . [y,z]) and A3: r in Q ; r . [y,z] in pi (Q,[y,z]) by A3, CARD_3:def_6; hence a in { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y,z]) } by A2; ::_thesis: verum end; { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y,z]) } c= { ((R . [x,y]) "/\" (r . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y,z]) } or a in { ((R . [x,y]) "/\" (r . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ) assume a in { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y,z]) } ; ::_thesis: a in { ((R . [x,y]) "/\" (r . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } then consider b being Element of (RealPoset [.0,1.]) such that A4: a = (R . [x,y]) "/\" b and A5: b in pi (Q,[y,z]) ; ex f being Function st ( f in Q & b = f . [y,z] ) by A5, CARD_3:def_6; hence a in { ((R . [x,y]) "/\" (r . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } by A4; ::_thesis: verum end; hence "\/" ( { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y,z]) } ,(RealPoset [.0,1.])) = "\/" ( { ((R . [x,y]) "/\" (r . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.])) by A1, XBOOLE_0:def_10; ::_thesis: verum end; then A6: for y being Element of X holds H1(y) = H2(y) ; thus { H1(y) where y is Element of X : S1[y] } = { H2(y) where y is Element of X : S1[y] } from FRAENKEL:sch_5(A6); ::_thesis: verum end; Lm5: 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 for z being Element of Z holds ( rng (min (R,S,x,z)) = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } & rng (min (R,S,x,z)) <> {} ) proof let X, Y, Z be non empty set ; ::_thesis: for R being RMembership_Func of X,Y for S being RMembership_Func of Y,Z for x being Element of X for z being Element of Z holds ( rng (min (R,S,x,z)) = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } & rng (min (R,S,x,z)) <> {} ) let R be RMembership_Func of X,Y; ::_thesis: for S being RMembership_Func of Y,Z for x being Element of X for z being Element of Z holds ( rng (min (R,S,x,z)) = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } & rng (min (R,S,x,z)) <> {} ) let S be RMembership_Func of Y,Z; ::_thesis: for x being Element of X for z being Element of Z holds ( rng (min (R,S,x,z)) = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } & rng (min (R,S,x,z)) <> {} ) let x be Element of X; ::_thesis: for z being Element of Z holds ( rng (min (R,S,x,z)) = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } & rng (min (R,S,x,z)) <> {} ) let z be Element of Z; ::_thesis: ( rng (min (R,S,x,z)) = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } & rng (min (R,S,x,z)) <> {} ) set L = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } ; A1: ( 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 FUNCT_2:def_1, RELSET_1:4; for c being set holds ( c in { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } iff c in rng (min (R,S,x,z)) ) proof let c be set ; ::_thesis: ( c in { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } iff c in rng (min (R,S,x,z)) ) hereby ::_thesis: ( c in rng (min (R,S,x,z)) implies c in { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } ) assume c in { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } ; ::_thesis: c in rng (min (R,S,x,z)) then consider y being Element of Y such that A2: c = (R . [x,y]) "/\" (S . [y,z]) ; c = (min (R,S,x,z)) . y by A2, FUZZY_4:def_2; hence c in rng (min (R,S,x,z)) by A1, PARTFUN1:4; ::_thesis: verum end; assume c in rng (min (R,S,x,z)) ; ::_thesis: c in { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } then consider y being Element of Y such that y in dom (min (R,S,x,z)) and A3: c = (min (R,S,x,z)) . y by PARTFUN1:3; c = (R . [x,y]) "/\" (S . [y,z]) by A3, FUZZY_4:def_2; hence c in { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } ; ::_thesis: verum end; hence rng (min (R,S,x,z)) = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } by TARSKI:1; ::_thesis: rng (min (R,S,x,z)) <> {} thus rng (min (R,S,x,z)) <> {} ; ::_thesis: verum end; Lm6: 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 for z being Element of Z holds (R (#) S) . [x,z] = "\/" ( { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } ,(RealPoset [.0,1.])) proof let X, Y, Z be non empty set ; ::_thesis: for R being RMembership_Func of X,Y for S being RMembership_Func of Y,Z for x being Element of X for z being Element of Z holds (R (#) S) . [x,z] = "\/" ( { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } ,(RealPoset [.0,1.])) let R be RMembership_Func of X,Y; ::_thesis: for S being RMembership_Func of Y,Z for x being Element of X for z being Element of Z holds (R (#) S) . [x,z] = "\/" ( { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } ,(RealPoset [.0,1.])) let S be RMembership_Func of Y,Z; ::_thesis: for x being Element of X for z being Element of Z holds (R (#) S) . [x,z] = "\/" ( { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } ,(RealPoset [.0,1.])) let x be Element of X; ::_thesis: for z being Element of Z holds (R (#) S) . [x,z] = "\/" ( { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } ,(RealPoset [.0,1.])) let z be Element of Z; ::_thesis: (R (#) S) . [x,z] = "\/" ( { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } ,(RealPoset [.0,1.])) set L = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } ; [x,z] in [:X,Z:] ; then A1: (R (#) S) . (x,z) = upper_bound (rng (min (R,S,x,z))) by FUZZY_4:def_3; A2: for b being Element of (RealPoset [.0,1.]) st b is_>=_than { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } holds (R (#) S) . [x,z] <<= b proof let b be Element of (RealPoset [.0,1.]); ::_thesis: ( b is_>=_than { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } implies (R (#) S) . [x,z] <<= b ) assume A3: b is_>=_than { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } ; ::_thesis: (R (#) S) . [x,z] <<= b A4: rng (min (R,S,x,z)) c= [.0,1.] by RELAT_1:def_19; A5: { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } = rng (min (R,S,x,z)) by Lm5; for r being real number st r in rng (min (R,S,x,z)) holds r <= b proof let r be real number ; ::_thesis: ( r in rng (min (R,S,x,z)) implies r <= b ) assume A6: r in rng (min (R,S,x,z)) ; ::_thesis: r <= b then reconsider r = r as Element of (RealPoset [.0,1.]) by A4, LFUZZY_0:def_3; r <<= b by A3, A5, A6, LATTICE3:def_9; hence r <= b by LFUZZY_0:3; ::_thesis: verum end; then upper_bound (rng (min (R,S,x,z))) <= b by SEQ_4:144; hence (R (#) S) . [x,z] <<= b by A1, LFUZZY_0:3; ::_thesis: verum end; for b being Element of (RealPoset [.0,1.]) st b in { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } holds (R (#) S) . [x,z] >>= b proof let b be Element of (RealPoset [.0,1.]); ::_thesis: ( b in { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } implies (R (#) S) . [x,z] >>= b ) assume b in { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } ; ::_thesis: (R (#) S) . [x,z] >>= b then consider y being Element of Y such that A7: b = (R . [x,y]) "/\" (S . [y,z]) and verum ; ( dom (min (R,S,x,z)) = Y & b = (min (R,S,x,z)) . y ) by A7, FUNCT_2:def_1, FUZZY_4:def_2; then b <= upper_bound (rng (min (R,S,x,z))) by FUZZY_4:1; hence (R (#) S) . [x,z] >>= b by A1, LFUZZY_0:3; ::_thesis: verum end; then (R (#) S) . [x,z] is_>=_than { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } by LATTICE3:def_9; hence (R (#) S) . [x,z] = "\/" ( { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } ,(RealPoset [.0,1.])) by A2, YELLOW_0:32; ::_thesis: verum end; Lm7: for X being non empty set for R being RMembership_Func of X,X for Q being Subset of (FuzzyLattice [:X,X:]) for x, z being Element of X holds { ("\/" ( { ((R . [x,y]) "/\" (r . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } = { ("\/" ( { ((R . [x,y]) "/\" ((@ r9) . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q } proof let X be non empty set ; ::_thesis: for R being RMembership_Func of X,X for Q being Subset of (FuzzyLattice [:X,X:]) for x, z being Element of X holds { ("\/" ( { ((R . [x,y]) "/\" (r . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } = { ("\/" ( { ((R . [x,y]) "/\" ((@ r9) . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q } let R be RMembership_Func of X,X; ::_thesis: for Q being Subset of (FuzzyLattice [:X,X:]) for x, z being Element of X holds { ("\/" ( { ((R . [x,y]) "/\" (r . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } = { ("\/" ( { ((R . [x,y]) "/\" ((@ r9) . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q } let Q be Subset of (FuzzyLattice [:X,X:]); ::_thesis: for x, z being Element of X holds { ("\/" ( { ((R . [x,y]) "/\" (r . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } = { ("\/" ( { ((R . [x,y]) "/\" ((@ r9) . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q } let x, z be Element of X; ::_thesis: { ("\/" ( { ((R . [x,y]) "/\" (r . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } = { ("\/" ( { ((R . [x,y]) "/\" ((@ r9) . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q } set FL = FuzzyLattice [:X,X:]; defpred S1[ Element of (FuzzyLattice [:X,X:])] means \$1 in Q; deffunc H1( Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (RealPoset [.0,1.]) = "\/" ( { ((R . [x,y]) "/\" (\$1 . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.])); deffunc H2( Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (RealPoset [.0,1.]) = "\/" ( { ((R . [x,y]) "/\" ((@ \$1) . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.])); for r being Element of (FuzzyLattice [:X,X:]) st r in Q holds "\/" ( { ((R . [x,y]) "/\" (r . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.])) = "\/" ( { ((R . [x,y]) "/\" ((@ r) . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.])) proof let r be Element of (FuzzyLattice [:X,X:]); ::_thesis: ( r in Q implies "\/" ( { ((R . [x,y]) "/\" (r . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.])) = "\/" ( { ((R . [x,y]) "/\" ((@ r) . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.])) ) assume r in Q ; ::_thesis: "\/" ( { ((R . [x,y]) "/\" (r . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.])) = "\/" ( { ((R . [x,y]) "/\" ((@ r) . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.])) { ((R . [x,y]) "/\" (r . [y,z])) where y is Element of X : verum } = { ((R . [x,y]) "/\" ((@ r) . [y,z])) where y is Element of X : verum } proof deffunc H3( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = (R . [x,\$1]) "/\" ((@ r) . [\$1,z]); deffunc H4( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = (R . [x,\$1]) "/\" (r . [\$1,z]); defpred S2[ Element of X] means verum; A1: for y being Element of X holds H4(y) = H3(y) by LFUZZY_0:def_5; thus { H4(y) where y is Element of X : S2[y] } = { H3(y) where y is Element of X : S2[y] } from FRAENKEL:sch_5(A1); ::_thesis: verum end; hence "\/" ( { ((R . [x,y]) "/\" (r . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.])) = "\/" ( { ((R . [x,y]) "/\" ((@ r) . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.])) ; ::_thesis: verum end; then A2: for r being Element of (FuzzyLattice [:X,X:]) st S1[r] holds H1(r) = H2(r) ; thus { H1(r) where r is Element of (FuzzyLattice [:X,X:]) : S1[r] } = { H2(r) where r is Element of (FuzzyLattice [:X,X:]) : S1[r] } from FRAENKEL:sch_6(A2); ::_thesis: verum end; Lm8: for X being non empty set for R being RMembership_Func of X,X for Q being Subset of (FuzzyLattice [:X,X:]) for x, z being Element of X holds { ("\/" ( { ((R . [x,y]) "/\" ((@ r) . [y,z])) where y is Element of X : verum } ,(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 X be non empty set ; ::_thesis: for R being RMembership_Func of X,X for Q being Subset of (FuzzyLattice [:X,X:]) for x, z being Element of X holds { ("\/" ( { ((R . [x,y]) "/\" ((@ r) . [y,z])) where y is Element of X : verum } ,(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 } let R be RMembership_Func of X,X; ::_thesis: for Q being Subset of (FuzzyLattice [:X,X:]) for x, z being Element of X holds { ("\/" ( { ((R . [x,y]) "/\" ((@ r) . [y,z])) where y is Element of X : verum } ,(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 } let Q be Subset of (FuzzyLattice [:X,X:]); ::_thesis: for x, z being Element of X holds { ("\/" ( { ((R . [x,y]) "/\" ((@ r) . [y,z])) where y is Element of X : verum } ,(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 } let x, z be Element of X; ::_thesis: { ("\/" ( { ((R . [x,y]) "/\" ((@ r) . [y,z])) where y is Element of X : verum } ,(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 } set FL = FuzzyLattice [:X,X:]; defpred S1[ Element of (FuzzyLattice [:X,X:])] means \$1 in Q; deffunc H1( Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (RealPoset [.0,1.]) = "\/" ( { ((R . [x,y]) "/\" ((@ \$1) . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.])); deffunc H2( Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (RealPoset [.0,1.]) = (R (#) (@ \$1)) . [x,z]; A1: for r being Element of (FuzzyLattice [:X,X:]) st S1[r] holds H1(r) = H2(r) by Lm6; thus { H1(r) where r is Element of (FuzzyLattice [:X,X:]) : S1[r] } = { H2(r) where r is Element of (FuzzyLattice [:X,X:]) : S1[r] } from FRAENKEL:sch_6(A1); ::_thesis: verum end; Lm9: for X being non empty set for R being RMembership_Func of X,X for Q being Subset of (FuzzyLattice [:X,X:]) for 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 X be non empty set ; ::_thesis: for R being RMembership_Func of X,X for Q being Subset of (FuzzyLattice [:X,X:]) for 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]) let R be RMembership_Func of X,X; ::_thesis: for Q being Subset of (FuzzyLattice [:X,X:]) for 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]) let Q be Subset of (FuzzyLattice [:X,X:]); ::_thesis: for 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]) let x, z be Element of X; ::_thesis: { ((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]) set FL = FuzzyLattice [:X,X:]; set A = { ((R (#) (@ r)) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ; set B = pi ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]); thus { ((R (#) (@ r)) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } c= pi ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) :: according to XBOOLE_0:def_10 ::_thesis: pi ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) c= { ((R (#) (@ r)) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ((R (#) (@ r)) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } or a in pi ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) ) assume a in { ((R (#) (@ r)) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ; ::_thesis: a in pi ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) then consider r being Element of (FuzzyLattice [:X,X:]) such that A1: a = (R (#) (@ r)) . [x,z] and A2: r in Q ; R (#) (@ r) in { (R (#) (@ r9)) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q } by A2; hence a in pi ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) by A1, CARD_3:def_6; ::_thesis: verum end; thus pi ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) c= { ((R (#) (@ r)) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ::_thesis: verum proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in pi ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) or b in { ((R (#) (@ r)) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ) assume b in pi ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) ; ::_thesis: b in { ((R (#) (@ r)) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } then consider f being Function such that A3: f in { (R (#) (@ r9)) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q } and A4: b = f . [x,z] by CARD_3:def_6; ex r being Element of (FuzzyLattice [:X,X:]) st ( f = R (#) (@ r) & r in Q ) by A3; hence b in { ((R (#) (@ r)) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } by A4; ::_thesis: verum end; end; Lm10: for X being non empty set for R being RMembership_Func of X,X for Q being Subset of (FuzzyLattice [:X,X:]) for 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 : verum } ,(RealPoset [.0,1.])) = "\/" ( { ("\/" ( { ((R . [x,y]) "/\" (r9 . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q } ,(RealPoset [.0,1.])) proof let X be non empty set ; ::_thesis: for R being RMembership_Func of X,X for Q being Subset of (FuzzyLattice [:X,X:]) for 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 : verum } ,(RealPoset [.0,1.])) = "\/" ( { ("\/" ( { ((R . [x,y]) "/\" (r9 . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q } ,(RealPoset [.0,1.])) let R be RMembership_Func of X,X; ::_thesis: for Q being Subset of (FuzzyLattice [:X,X:]) for 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 : verum } ,(RealPoset [.0,1.])) = "\/" ( { ("\/" ( { ((R . [x,y]) "/\" (r9 . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q } ,(RealPoset [.0,1.])) let Q be Subset of (FuzzyLattice [:X,X:]); ::_thesis: for 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 : verum } ,(RealPoset [.0,1.])) = "\/" ( { ("\/" ( { ((R . [x,y]) "/\" (r9 . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q } ,(RealPoset [.0,1.])) let x, z be Element of X; ::_thesis: "\/" ( { ("\/" ( { ((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 : verum } ,(RealPoset [.0,1.])) = "\/" ( { ("\/" ( { ((R . [x,y]) "/\" (r9 . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q } ,(RealPoset [.0,1.])) set FL = FuzzyLattice [:X,X:]; set RP = RealPoset [.0,1.]; defpred S1[ Element of X] means verum; defpred S2[ Element of (FuzzyLattice [:X,X:])] means \$1 in Q; deffunc H1( Element of X, Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (RealPoset [.0,1.]) = (R . [x,\$1]) "/\" (\$2 . [\$1,z]); deffunc H2( Element of X, Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (RealPoset [.0,1.]) = (R . [x,\$1]) "/\" (\$2 . [\$1,z]); A1: for y being Element of X for r being Element of (FuzzyLattice [:X,X:]) st S1[y] & S2[r] holds H1(y,r) = H2(y,r) ; thus "\/" ( { ("\/" ( { H1(y,r) where r is Element of (FuzzyLattice [:X,X:]) : S2[r] } ,(RealPoset [.0,1.]))) where y is Element of X : S1[y] } ,(RealPoset [.0,1.])) = "\/" ( { ("\/" ( { H2(y9,r9) where y9 is Element of X : S1[y9] } ,(RealPoset [.0,1.]))) where r9 is Element of (FuzzyLattice [:X,X:]) : S2[r9] } ,(RealPoset [.0,1.])) from LFUZZY_0:sch_5(A1); ::_thesis: verum end; theorem Th34: :: LFUZZY_1:34 for X being non empty set for R being RMembership_Func of X,X for 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 X be non empty set ; ::_thesis: for R being RMembership_Func of X,X for 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:])) let R be RMembership_Func of X,X; ::_thesis: for 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:])) let Q be Subset of (FuzzyLattice [:X,X:]); ::_thesis: R (#) (@ ("\/" (Q,(FuzzyLattice [:X,X:])))) = "\/" ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:])) set FL = FuzzyLattice [:X,X:]; set RP = RealPoset [.0,1.]; "\/" ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:])) = @ ("\/" ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:]))) by LFUZZY_0:def_5; then reconsider F = "\/" ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:])) as RMembership_Func of X,X ; for x, z being Element of X holds (R (#) (@ ("\/" (Q,(FuzzyLattice [:X,X:]))))) . (x,z) = F . (x,z) proof let x, z be Element of X; ::_thesis: (R (#) (@ ("\/" (Q,(FuzzyLattice [:X,X:]))))) . (x,z) = F . (x,z) A1: { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } c= the carrier of (FuzzyLattice [:X,X:]) proof let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } or t in the carrier of (FuzzyLattice [:X,X:]) ) assume t in { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ; ::_thesis: t in the carrier of (FuzzyLattice [:X,X:]) then consider r being Element of (FuzzyLattice [:X,X:]) such that A2: t = R (#) (@ r) and r in Q ; ([:X,X:],(R (#) (@ r))) @ = R (#) (@ r) by LFUZZY_0:def_6; hence t in the carrier of (FuzzyLattice [:X,X:]) by A2; ::_thesis: verum end; thus (R (#) (@ ("\/" (Q,(FuzzyLattice [:X,X:]))))) . (x,z) = "\/" ( { ((R . (x,y)) "/\" ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . (y,z))) where y is Element of X : verum } ,(RealPoset [.0,1.])) by LFUZZY_0:22 .= "\/" ( { ((R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))) where y is Element of X : verum } ,(RealPoset [.0,1.])) by Lm2 .= "\/" ( { ("\/" ( { ((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 : verum } ,(RealPoset [.0,1.])) by Lm3 .= "\/" ( { ("\/" ( { ((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 : verum } ,(RealPoset [.0,1.])) by Lm4 .= "\/" ( { ("\/" ( { ((R . [x,y]) "/\" (r . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.])) by Lm10 .= "\/" ( { ("\/" ( { ((R . [x,y]) "/\" ((@ r) . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.])) by Lm7 .= "\/" ( { ((R (#) (@ r)) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.])) by Lm8 .= "\/" ((pi ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z])),(RealPoset [.0,1.])) by Lm9 .= F . (x,z) by A1, Th32 ; ::_thesis: verum end; hence R (#) (@ ("\/" (Q,(FuzzyLattice [:X,X:])))) = "\/" ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:])) by Th2; ::_thesis: verum end; theorem Th35: :: LFUZZY_1:35 for X being non empty set for R being RMembership_Func of X,X for 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 X be non empty set ; ::_thesis: for R being RMembership_Func of X,X for 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:])) let R be RMembership_Func of X,X; ::_thesis: for 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:])) let Q be Subset of (FuzzyLattice [:X,X:]); ::_thesis: (@ ("\/" (Q,(FuzzyLattice [:X,X:])))) (#) R = "\/" ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:])) set FL = FuzzyLattice [:X,X:]; set RP = RealPoset [.0,1.]; "\/" ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:])) = @ ("\/" ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:]))) by LFUZZY_0:def_5; then reconsider F = "\/" ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:])) as RMembership_Func of X,X ; for x, z being Element of X holds ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) (#) R) . (x,z) = F . (x,z) proof let x, z be Element of X; ::_thesis: ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) (#) R) . (x,z) = F . (x,z) A1: { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } c= the carrier of (FuzzyLattice [:X,X:]) proof let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } or t in the carrier of (FuzzyLattice [:X,X:]) ) assume t in { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ; ::_thesis: t in the carrier of (FuzzyLattice [:X,X:]) then consider r being Element of (FuzzyLattice [:X,X:]) such that A2: t = (@ r) (#) R and r in Q ; ([:X,X:],((@ r) (#) R)) @ = (@ r) (#) R by LFUZZY_0:def_6; hence t in the carrier of (FuzzyLattice [:X,X:]) by A2; ::_thesis: verum end; A3: { (("\/" ((pi (Q,[x,y])),(RealPoset [.0,1.]))) "/\" (R . [y,z])) where y is Element of X : verum } = { ("\/" ( { (b "/\" (R . [y9,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y9]) } ,(RealPoset [.0,1.]))) where y9 is Element of X : verum } proof deffunc H1( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = "\/" ( { (b "/\" (R . [\$1,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,\$1]) } ,(RealPoset [.0,1.])); deffunc H2( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = ("\/" ((pi (Q,[x,\$1])),(RealPoset [.0,1.]))) "/\" (R . [\$1,z]); defpred S1[ Element of X] means verum; 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 (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } ,(RealPoset [.0,1.])) proof FuzzyLattice [:X,X:] = (RealPoset [.0,1.]) |^ [:X,X:] by LFUZZY_0:def_4 .= product ([:X,X:] --> (RealPoset [.0,1.])) by YELLOW_1:def_5 ; then reconsider Q = Q as Subset of (product ([:X,X:] --> (RealPoset [.0,1.]))) ; let y be Element of X; ::_thesis: ("\/" ((pi (Q,[x,y])),(RealPoset [.0,1.]))) "/\" (R . [y,z]) = "\/" ( { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } ,(RealPoset [.0,1.])) pi (Q,[x,y]) is Subset of (RealPoset [.0,1.]) by FUNCOP_1:7; hence ("\/" ((pi (Q,[x,y])),(RealPoset [.0,1.]))) "/\" (R . [y,z]) = "\/" ( { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } ,(RealPoset [.0,1.])) by LFUZZY_0:15; ::_thesis: verum end; then A4: for y being Element of X holds H2(y) = H1(y) ; { H2(y) where y is Element of X : S1[y] } = { H1(y9) where y9 is Element of X : S1[y9] } from FRAENKEL:sch_5(A4); hence { (("\/" ((pi (Q,[x,y])),(RealPoset [.0,1.]))) "/\" (R . [y,z])) where y is Element of X : verum } = { ("\/" ( { (b "/\" (R . [y9,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y9]) } ,(RealPoset [.0,1.]))) where y9 is Element of X : verum } ; ::_thesis: verum end; A5: { ("\/" ( { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } ,(RealPoset [.0,1.]))) where y is Element of X : verum } = { ("\/" ( { ((r . [x,y9]) "/\" (R . [y9,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.]))) where y9 is Element of X : verum } proof deffunc H1( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = "\/" ( { ((r . [x,\$1]) "/\" (R . [\$1,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.])); deffunc H2( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = "\/" ( { (b "/\" (R . [\$1,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,\$1]) } ,(RealPoset [.0,1.])); defpred S1[ Element of X] means verum; for y being Element of X holds "\/" ( { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } ,(RealPoset [.0,1.])) = "\/" ( { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.])) proof let y be Element of X; ::_thesis: "\/" ( { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } ,(RealPoset [.0,1.])) = "\/" ( { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.])) set A = { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } ; set B = { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ; A6: { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } c= { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } or a in { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } ) assume a in { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ; ::_thesis: a in { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } then consider r being Element of (FuzzyLattice [:X,X:]) such that A7: a = (r . [x,y]) "/\" (R . [y,z]) and A8: r in Q ; r . [x,y] in pi (Q,[x,y]) by A8, CARD_3:def_6; hence a in { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } by A7; ::_thesis: verum end; { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } c= { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } or a in { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ) assume a in { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } ; ::_thesis: a in { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } then consider b being Element of (RealPoset [.0,1.]) such that A9: a = b "/\" (R . [y,z]) and A10: b in pi (Q,[x,y]) ; ex f being Function st ( f in Q & b = f . [x,y] ) by A10, CARD_3:def_6; hence a in { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } by A9; ::_thesis: verum end; hence "\/" ( { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } ,(RealPoset [.0,1.])) = "\/" ( { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.])) by A6, XBOOLE_0:def_10; ::_thesis: verum end; then A11: for y being Element of X holds H2(y) = H1(y) ; thus { H2(y) where y is Element of X : S1[y] } = { H1(y) where y is Element of X : S1[y] } from FRAENKEL:sch_5(A11); ::_thesis: verum end; A12: "\/" ( { ("\/" ( { ((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 : verum } ,(RealPoset [.0,1.])) = "\/" ( { ("\/" ( { ((r9 . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q } ,(RealPoset [.0,1.])) proof deffunc H1( Element of X, Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (RealPoset [.0,1.]) = (\$2 . [x,\$1]) "/\" (R . [\$1,z]); deffunc H2( Element of X, Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (RealPoset [.0,1.]) = (\$2 . [x,\$1]) "/\" (R . [\$1,z]); defpred S1[ Element of (FuzzyLattice [:X,X:])] means \$1 in Q; defpred S2[ Element of X] means verum; A13: for y being Element of X for r being Element of (FuzzyLattice [:X,X:]) st S2[y] & S1[r] holds H2(y,r) = H1(y,r) ; thus "\/" ( { ("\/" ( { H2(y,r) where r is Element of (FuzzyLattice [:X,X:]) : S1[r] } ,(RealPoset [.0,1.]))) where y is Element of X : S2[y] } ,(RealPoset [.0,1.])) = "\/" ( { ("\/" ( { H1(y9,r9) where y9 is Element of X : S2[y9] } ,(RealPoset [.0,1.]))) where r9 is Element of (FuzzyLattice [:X,X:]) : S1[r9] } ,(RealPoset [.0,1.])) from LFUZZY_0:sch_5(A13); ::_thesis: verum end; A14: { ("\/" ( { ((r . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } = { ("\/" ( { (((@ r9) . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q } proof deffunc H1( Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (RealPoset [.0,1.]) = "\/" ( { (((@ \$1) . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.])); deffunc H2( Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (RealPoset [.0,1.]) = "\/" ( { ((\$1 . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.])); defpred S1[ Element of (FuzzyLattice [:X,X:])] means \$1 in Q; for r being Element of (FuzzyLattice [:X,X:]) st r in Q holds "\/" ( { ((r . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.])) = "\/" ( { (((@ r) . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.])) proof let r be Element of (FuzzyLattice [:X,X:]); ::_thesis: ( r in Q implies "\/" ( { ((r . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.])) = "\/" ( { (((@ r) . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.])) ) assume r in Q ; ::_thesis: "\/" ( { ((r . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.])) = "\/" ( { (((@ r) . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.])) { ((r . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } = { (((@ r) . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } proof deffunc H3( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = ((@ r) . [x,\$1]) "/\" (R . [\$1,z]); deffunc H4( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = (r . [x,\$1]) "/\" (R . [\$1,z]); defpred S2[ Element of X] means verum; A15: for y being Element of X holds H4(y) = H3(y) by LFUZZY_0:def_5; thus { H4(y) where y is Element of X : S2[y] } = { H3(y) where y is Element of X : S2[y] } from FRAENKEL:sch_5(A15); ::_thesis: verum end; hence "\/" ( { ((r . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.])) = "\/" ( { (((@ r) . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.])) ; ::_thesis: verum end; then A16: for r being Element of (FuzzyLattice [:X,X:]) st S1[r] holds H2(r) = H1(r) ; thus { H2(r) where r is Element of (FuzzyLattice [:X,X:]) : S1[r] } = { H1(r) where r is Element of (FuzzyLattice [:X,X:]) : S1[r] } from FRAENKEL:sch_6(A16); ::_thesis: verum end; A17: { (((@ 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 set A = { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ; set B = pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]); thus { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } c= pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) :: according to XBOOLE_0:def_10 ::_thesis: pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) c= { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } or a in pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) ) assume a in { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ; ::_thesis: a in pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) then consider r being Element of (FuzzyLattice [:X,X:]) such that A18: a = ((@ r) (#) R) . [x,z] and A19: r in Q ; (@ r) (#) R in { ((@ r9) (#) R) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q } by A19; hence a in pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) by A18, CARD_3:def_6; ::_thesis: verum end; thus pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) c= { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ::_thesis: verum proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) or b in { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ) assume b in pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) ; ::_thesis: b in { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } then consider f being Function such that A20: f in { ((@ r9) (#) R) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q } and A21: b = f . [x,z] by CARD_3:def_6; ex r being Element of (FuzzyLattice [:X,X:]) st ( f = (@ r) (#) R & r in Q ) by A20; hence b in { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } by A21; ::_thesis: verum end; end; A22: { (((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } = { (("\/" ((pi (Q,[x,y])),(RealPoset [.0,1.]))) "/\" (R . [y,z])) where y is Element of X : verum } proof deffunc H1( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = ("\/" ((pi (Q,[x,\$1])),(RealPoset [.0,1.]))) "/\" (R . [\$1,z]); deffunc H2( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . [x,\$1]) "/\" (R . [\$1,z]); defpred S1[ Element of X] means verum; 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; ::_thesis: ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . [x,y]) "/\" (R . [y,z]) = ("\/" ((pi (Q,[x,y])),(RealPoset [.0,1.]))) "/\" (R . [y,z]) (@ ("\/" (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 Th32 ; hence ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . [x,y]) "/\" (R . [y,z]) = ("\/" ((pi (Q,[x,y])),(RealPoset [.0,1.]))) "/\" (R . [y,z]) ; ::_thesis: verum end; then A23: for y being Element of X holds H2(y) = H1(y) ; thus { H2(y) where y is Element of X : S1[y] } = { H1(y9) where y9 is Element of X : S1[y9] } from FRAENKEL:sch_5(A23); ::_thesis: verum end; A24: { ("\/" ( { (((@ r) . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } = { (((@ r9) (#) R) . [x,z]) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q } proof deffunc H1( Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (RealPoset [.0,1.]) = ((@ \$1) (#) R) . [x,z]; deffunc H2( Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (RealPoset [.0,1.]) = "\/" ( { (((@ \$1) . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.])); defpred S1[ Element of (FuzzyLattice [:X,X:])] means \$1 in Q; A25: for r being Element of (FuzzyLattice [:X,X:]) st S1[r] holds H2(r) = H1(r) by Lm6; thus { H2(r) where r is Element of (FuzzyLattice [:X,X:]) : S1[r] } = { H1(r) where r is Element of (FuzzyLattice [:X,X:]) : S1[r] } from FRAENKEL:sch_6(A25); ::_thesis: verum end; thus ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) (#) R) . (x,z) = "\/" ( { (((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.])) by Lm6 .= F . (x,z) by A1, A22, A3, A5, A12, A14, A24, A17, Th32 ; ::_thesis: verum end; hence (@ ("\/" (Q,(FuzzyLattice [:X,X:])))) (#) R = "\/" ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:])) by Th2; ::_thesis: verum end; theorem Th36: :: LFUZZY_1:36 for X being non empty set for R being RMembership_Func of X,X holds (TrCl R) (#) (TrCl R) = "\/" ( { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } ,(FuzzyLattice [:X,X:])) proof let X be non empty set ; ::_thesis: for R being RMembership_Func of X,X holds (TrCl R) (#) (TrCl R) = "\/" ( { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } ,(FuzzyLattice [:X,X:])) let R be RMembership_Func of X,X; ::_thesis: (TrCl R) (#) (TrCl R) = "\/" ( { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } ,(FuzzyLattice [:X,X:])) set Q = { (n iter R) where n is Element of NAT : n > 0 } ; set FL = FuzzyLattice [:X,X:]; A1: { (n iter R) where n is Element of NAT : n > 0 } c= the carrier of (FuzzyLattice [:X,X:]) proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { (n iter R) where n is Element of NAT : n > 0 } or q in the carrier of (FuzzyLattice [:X,X:]) ) assume q in { (n iter R) where n is Element of NAT : n > 0 } ; ::_thesis: q in the carrier of (FuzzyLattice [:X,X:]) then consider i being Element of NAT such that A2: q = i iter R and 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 A2; ::_thesis: verum end; A3: { ("\/" ( { ((@ r) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } } = { ("\/" ( { (([:X,X:],((@ r9) (#) (@ s9))) @) where s9 is Element of (FuzzyLattice [:X,X:]) : s9 in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in { (n iter R) where n is Element of NAT : n > 0 } } proof deffunc H1( Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (FuzzyLattice [:X,X:]) = "\/" ( { (([:X,X:],((@ \$1) (#) (@ s))) @) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])); deffunc H2( Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (FuzzyLattice [:X,X:]) = "\/" ( { ((@ \$1) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])); defpred S1[ Element of (FuzzyLattice [:X,X:])] means \$1 in { (n iter R) where n is Element of NAT : n > 0 } ; for r being Element of (FuzzyLattice [:X,X:]) holds "\/" ( { ((@ r) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])) = "\/" ( { (([:X,X:],((@ r) (#) (@ s))) @) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])) proof let r be Element of (FuzzyLattice [:X,X:]); ::_thesis: "\/" ( { ((@ r) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])) = "\/" ( { (([:X,X:],((@ r) (#) (@ s))) @) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])) { ((@ r) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } = { (([:X,X:],((@ r) (#) (@ s))) @) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } proof deffunc H3( Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (FuzzyLattice [:X,X:]) = ([:X,X:],((@ r) (#) (@ \$1))) @ ; deffunc H4( Element of (FuzzyLattice [:X,X:])) -> Element of bool [:[:X,X:],REAL:] = (@ r) (#) (@ \$1); defpred S2[ Element of (FuzzyLattice [:X,X:])] means \$1 in { (n iter R) where n is Element of NAT : n > 0 } ; A4: for s being Element of (FuzzyLattice [:X,X:]) holds H4(s) = H3(s) by LFUZZY_0:def_6; { H4(s) where s is Element of (FuzzyLattice [:X,X:]) : S2[s] } = { H3(s) where s is Element of (FuzzyLattice [:X,X:]) : S2[s] } from FRAENKEL:sch_5(A4); hence { ((@ r) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } = { (([:X,X:],((@ r) (#) (@ s))) @) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ; ::_thesis: verum end; hence "\/" ( { ((@ r) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])) = "\/" ( { (([:X,X:],((@ r) (#) (@ s))) @) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])) ; ::_thesis: verum end; then A5: for r being Element of (FuzzyLattice [:X,X:]) holds H2(r) = H1(r) ; { H2(r) where r is Element of (FuzzyLattice [:X,X:]) : S1[r] } = { H1(r) where r is Element of (FuzzyLattice [:X,X:]) : S1[r] } from FRAENKEL:sch_5(A5); hence { ("\/" ( { ((@ r) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } } = { ("\/" ( { (([:X,X:],((@ r9) (#) (@ s9))) @) where s9 is Element of (FuzzyLattice [:X,X:]) : s9 in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in { (n iter R) where n is Element of NAT : n > 0 } } ; ::_thesis: verum end; defpred S1[ Element of (FuzzyLattice [:X,X:])] means \$1 in { (n iter R) where n is Element of NAT : n > 0 } ; defpred S2[ Element of (FuzzyLattice [:X,X:])] means \$1 in { (n iter R) where n is Element of NAT : n > 0 } ; deffunc H1( Element of (FuzzyLattice [:X,X:]), Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (FuzzyLattice [:X,X:]) = ([:X,X:],((@ \$1) (#) (@ \$2))) @ ; A6: { ((@ r) (#) (@ s)) where r, s is Element of (FuzzyLattice [:X,X:]) : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } = { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } proof set A = { ((@ r) (#) (@ s)) where r, s is Element of (FuzzyLattice [:X,X:]) : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } ; set B = { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } ; thus { ((@ r) (#) (@ s)) where r, s is Element of (FuzzyLattice [:X,X:]) : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } c= { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } :: according to XBOOLE_0:def_10 ::_thesis: { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } c= { ((@ r) (#) (@ s)) where r, s is Element of (FuzzyLattice [:X,X:]) : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ((@ r) (#) (@ s)) where r, s is Element of (FuzzyLattice [:X,X:]) : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } or a in { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } ) assume a in { ((@ r) (#) (@ s)) where r, s is Element of (FuzzyLattice [:X,X:]) : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } ; ::_thesis: a in { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } then consider r, s being Element of (FuzzyLattice [:X,X:]) such that A7: a = (@ r) (#) (@ s) and A8: ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) ; A9: ( r = @ r & s = @ s ) by LFUZZY_0:def_5; ( ex i being Element of NAT st ( r = i iter R & i > 0 ) & ex j being Element of NAT st ( s = j iter R & j > 0 ) ) by A8; hence a in { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } by A7, A9; ::_thesis: verum end; thus { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } c= { ((@ r) (#) (@ s)) where r, s is Element of (FuzzyLattice [:X,X:]) : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } ::_thesis: verum proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } or b in { ((@ r) (#) (@ s)) where r, s is Element of (FuzzyLattice [:X,X:]) : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } ) assume b in { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } ; ::_thesis: b in { ((@ r) (#) (@ s)) where r, s is Element of (FuzzyLattice [:X,X:]) : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } then consider i, j being Element of NAT such that A10: b = (i iter R) (#) (j iter R) and A11: ( i > 0 & j > 0 ) ; j iter R = ([:X,X:],(j iter R)) @ by LFUZZY_0:def_6; then reconsider s = j iter R as Element of (FuzzyLattice [:X,X:]) ; i iter R = ([:X,X:],(i iter R)) @ by LFUZZY_0:def_6; then reconsider r = i iter R as Element of (FuzzyLattice [:X,X:]) ; A12: ( @ r = r & @ s = s ) by LFUZZY_0:def_5; ( i iter R in { (n iter R) where n is Element of NAT : n > 0 } & j iter R in { (n iter R) where n is Element of NAT : n > 0 } ) by A11; hence b in { ((@ r) (#) (@ s)) where r, s is Element of (FuzzyLattice [:X,X:]) : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } by A10, A12; ::_thesis: verum end; end; A13: { (([:X,X:],((@ r) (#) (@ s))) @) where r, s is Element of (FuzzyLattice [:X,X:]) : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } = { ((@ r) (#) (@ s)) where r, s is Element of (FuzzyLattice [:X,X:]) : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } proof deffunc H2( Element of (FuzzyLattice [:X,X:]), Element of (FuzzyLattice [:X,X:])) -> Element of bool [:[:X,X:],REAL:] = (@ \$1) (#) (@ \$2); deffunc H3( Element of (FuzzyLattice [:X,X:]), Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (FuzzyLattice [:X,X:]) = ([:X,X:],((@ \$1) (#) (@ \$2))) @ ; defpred S3[ Element of (FuzzyLattice [:X,X:]), Element of (FuzzyLattice [:X,X:])] means ( \$1 in { (n iter R) where n is Element of NAT : n > 0 } & \$2 in { (n iter R) where n is Element of NAT : n > 0 } ); A14: for r, s being Element of (FuzzyLattice [:X,X:]) holds H3(r,s) = H2(r,s) by LFUZZY_0:def_6; { H3(r,s) where r, s is Element of (FuzzyLattice [:X,X:]) : S3[r,s] } = { H2(r,s) where r, s is Element of (FuzzyLattice [:X,X:]) : S3[r,s] } from FRAENKEL:sch_7(A14); hence { (([:X,X:],((@ r) (#) (@ s))) @) where r, s is Element of (FuzzyLattice [:X,X:]) : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } = { ((@ r) (#) (@ s)) where r, s is Element of (FuzzyLattice [:X,X:]) : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } ; ::_thesis: verum end; A15: "\/" ( { (n iter R) where n is Element of NAT : n > 0 } ,(FuzzyLattice [:X,X:])) = @ ("\/" ( { (n iter R) where n is Element of NAT : n > 0 } ,(FuzzyLattice [:X,X:]))) by LFUZZY_0:def_5; { ((@ r) (#) (TrCl R)) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } } = { ("\/" ( { ((@ r9) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in { (n iter R) where n is Element of NAT : n > 0 } } proof set A = { ((@ r) (#) (TrCl R)) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } } ; set B = { ("\/" ( { ((@ r9) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in { (n iter R) where n is Element of NAT : n > 0 } } ; thus { ((@ r) (#) (TrCl R)) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } } c= { ("\/" ( { ((@ r9) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in { (n iter R) where n is Element of NAT : n > 0 } } :: according to XBOOLE_0:def_10 ::_thesis: { ("\/" ( { ((@ r9) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in { (n iter R) where n is Element of NAT : n > 0 } } c= { ((@ r) (#) (TrCl R)) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } } proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ((@ r) (#) (TrCl R)) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } } or a in { ("\/" ( { ((@ r9) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in { (n iter R) where n is Element of NAT : n > 0 } } ) assume a in { ((@ r) (#) (TrCl R)) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } } ; ::_thesis: a in { ("\/" ( { ((@ r9) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in { (n iter R) where n is Element of NAT : n > 0 } } then consider r being Element of (FuzzyLattice [:X,X:]) such that A16: a = (@ r) (#) (TrCl R) and A17: r in { (n iter R) where n is Element of NAT : n > 0 } ; a = "\/" ( { ((@ r) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])) by A15, A1, A16, Th34; hence a in { ("\/" ( { ((@ r9) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in { (n iter R) where n is Element of NAT : n > 0 } } by A17; ::_thesis: verum end; thus { ("\/" ( { ((@ r9) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in { (n iter R) where n is Element of NAT : n > 0 } } c= { ((@ r) (#) (TrCl R)) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } } ::_thesis: verum proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ("\/" ( { ((@ r9) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in { (n iter R) where n is Element of NAT : n > 0 } } or a in { ((@ r) (#) (TrCl R)) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } } ) assume a in { ("\/" ( { ((@ r9) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in { (n iter R) where n is Element of NAT : n > 0 } } ; ::_thesis: a in { ((@ r) (#) (TrCl R)) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } } then consider r being Element of (FuzzyLattice [:X,X:]) such that A18: a = "\/" ( { ((@ r) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])) and A19: r in { (n iter R) where n is Element of NAT : n > 0 } ; a = (@ r) (#) (TrCl R) by A15, A1, A18, Th34; hence a in { ((@ r) (#) (TrCl R)) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } } by A19; ::_thesis: verum end; end; hence (TrCl R) (#) (TrCl R) = "\/" ( { ("\/" ( { H1(r,s) where s is Element of (FuzzyLattice [:X,X:]) : S1[s] } ,(FuzzyLattice [:X,X:]))) where r is Element of (FuzzyLattice [:X,X:]) : S2[r] } ,(FuzzyLattice [:X,X:])) by A15, A1, A3, Th35 .= "\/" ( { H1(r,s) where r, s is Element of (FuzzyLattice [:X,X:]) : ( S2[r] & S1[s] ) } ,(FuzzyLattice [:X,X:])) from LFUZZY_0:sch_1() .= "\/" ( { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } ,(FuzzyLattice [:X,X:])) by A6, A13 ; ::_thesis: verum end; registration let X be non empty set ; let R be RMembership_Func of X,X; cluster TrCl R -> transitive ; coherence TrCl R is transitive proof 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 set ; :: 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 by FUZZY_1:def_2; 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= by FUZZY_1:def_2; hence TrCl R is transitive by Def6; ::_thesis: verum end; end; theorem Th37: :: LFUZZY_1:37 for X being non empty set for R being RMembership_Func of X,X for n being Nat st R is transitive & n > 0 holds R c= proof let X be non empty set ; ::_thesis: for R being RMembership_Func of X,X for n being Nat st R is transitive & n > 0 holds R c= let R be RMembership_Func of X,X; ::_thesis: for n being Nat st R is transitive & n > 0 holds R c= let n be Nat; ::_thesis: ( R is transitive & n > 0 implies R c= ) assume that A1: R is transitive and A2: n > 0 ; ::_thesis: R c= reconsider n = n as non empty Element of NAT by A2, ORDINAL1:def_12; defpred S1[ Nat] means R c= ; A3: R c= by A1, Def6; A4: for k being non empty Nat st S1[k] holds S1[k + 1] proof let k be non empty Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume S1[k] ; ::_thesis: S1[k + 1] then R (#) R c= by Th6; then R (#) R c= by Th26; hence S1[k + 1] by A3, Th5; ::_thesis: verum end; A5: S1[1] by Th25; for k being non empty Nat holds S1[k] from NAT_1:sch_10(A5, A4); then S1[n] ; hence R c= ; ::_thesis: verum end; theorem Th38: :: LFUZZY_1:38 for X being non empty set for R being RMembership_Func of X,X st R is transitive holds R = TrCl R proof let X be non empty set ; ::_thesis: for R being RMembership_Func of X,X st R is transitive holds R = TrCl R let R be RMembership_Func of X,X; ::_thesis: ( R is transitive implies R = TrCl R ) assume A1: R is transitive ; ::_thesis: R = TrCl R for c being Element of [:X,X:] holds (TrCl R) . c <= R . c proof set Q = { (n iter R) where n is Element of NAT : n > 0 } ; set RP = RealPoset [.0,1.]; let c be Element of [:X,X:]; ::_thesis: (TrCl R) . c <= R . c for b being Element of (RealPoset [.0,1.]) st b in pi ( { (n iter R) where n is Element of NAT : n > 0 } ,c) holds b <<= R . c proof let b be Element of (RealPoset [.0,1.]); ::_thesis: ( b in pi ( { (n iter R) where n is Element of NAT : n > 0 } ,c) implies b <<= R . c ) assume b in pi ( { (n iter R) where n is Element of NAT : n > 0 } ,c) ; ::_thesis: b <<= R . c then consider f being Function such that A2: f in { (n iter R) where n is Element of NAT : n > 0 } and A3: b = f . c by CARD_3:def_6; consider n being Element of NAT such that A4: f = n iter R and A5: n > 0 by A2; R c= by A1, A5, Th37; then (n iter R) . c <= R . c by FUZZY_1:def_2; hence b <<= R . c by A3, A4, LFUZZY_0:3; ::_thesis: verum end; then A6: R . c is_>=_than pi ( { (n iter R) where n is Element of NAT : n > 0 } ,c) by LATTICE3:def_9; { (n iter R) where n is Element of NAT : n > 0 } c= the carrier of (FuzzyLattice [:X,X:]) proof let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in { (n iter R) where n is Element of NAT : n > 0 } or t in the carrier of (FuzzyLattice [:X,X:]) ) assume t in { (n iter R) where n is Element of NAT : n > 0 } ; ::_thesis: t in the carrier of (FuzzyLattice [:X,X:]) then consider i being Element of NAT such that A7: t = i iter R and 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 A7; ::_thesis: verum end; then (TrCl R) . c = "\/" ((pi ( { (n iter R) where n is Element of NAT : n > 0 } ,c)),(RealPoset [.0,1.])) by Th32; then (TrCl R) . c <<= R . c by A6, YELLOW_0:32; hence (TrCl R) . c <= R . c by LFUZZY_0:3; ::_thesis: verum end; then A8: R c= by FUZZY_1:def_2; TrCl R c= by Th30; hence R = TrCl R by A8, Th3; ::_thesis: verum end; theorem Th39: :: LFUZZY_1:39 for X being non empty set for R, S being RMembership_Func of X,X for n being Nat st S c= holds n iter S c= proof let X be non empty set ; ::_thesis: for R, S being RMembership_Func of X,X for n being Nat st S c= holds n iter S c= let R, S be RMembership_Func of X,X; ::_thesis: for n being Nat st S c= holds n iter S c= let n be Nat; ::_thesis: ( S c= implies n iter S c= ) defpred S1[ Nat] means \$1 iter S c= ; assume A1: S c= ; ::_thesis: n iter S c= A2: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: S1[k] ; ::_thesis: S1[k + 1] ( (k iter R) (#) R = (k + 1) iter R & (k iter S) (#) S = (k + 1) iter S ) by Th26; hence S1[k + 1] by A1, A3, Th6; ::_thesis: verum end; 0 iter R = Imf (X,X) by Th24 .= 0 iter S by Th24 ; then A4: S1[ 0 ] ; for k being Nat holds S1[k] from NAT_1:sch_2(A4, A2); hence n iter S c= ; ::_thesis: verum end; theorem :: LFUZZY_1:40 for X being non empty set for R, S being RMembership_Func of X,X st S is transitive & S c= holds S c= proof let X be non empty set ; ::_thesis: for R, S being RMembership_Func of X,X st S is transitive & S c= holds S c= let R, S be RMembership_Func of X,X; ::_thesis: ( S is transitive & S c= implies S c= ) assume that A1: S is transitive and A2: S c= ; ::_thesis: S c= for c being Element of [:X,X:] holds (TrCl R) . c <= (TrCl S) . c proof set Q = { (n iter R) where n is Element of NAT : n > 0 } ; set RP = RealPoset [.0,1.]; let c be Element of [:X,X:]; ::_thesis: (TrCl R) . c <= (TrCl S) . c for b being Element of (RealPoset [.0,1.]) st b in pi ( { (n iter R) where n is Element of NAT : n > 0 } ,c) holds b <<= (TrCl S) . c proof let b be Element of (RealPoset [.0,1.]); ::_thesis: ( b in pi ( { (n iter R) where n is Element of NAT : n > 0 } ,c) implies b <<= (TrCl S) . c ) assume b in pi ( { (n iter R) where n is Element of NAT : n > 0 } ,c) ; ::_thesis: b <<= (TrCl S) . c then consider f being Function such that A3: f in { (n iter R) where n is Element of NAT : n > 0 } and A4: b = f . c by CARD_3:def_6; consider n being Element of NAT such that A5: f = n iter R and A6: n > 0 by A3; A7: TrCl S c= by A6, Th31; n iter S c= by A2, Th39; then TrCl S c= by A7, Th5; then (n iter R) . c <= (TrCl S) . c by FUZZY_1:def_2; hence b <<= (TrCl S) . c by A4, A5, LFUZZY_0:3; ::_thesis: verum end; then (TrCl S) . c is_>=_than pi ( { (n iter R) where n is Element of NAT : n > 0 } ,c) by LATTICE3:def_9; then A8: "\/" ((pi ( { (n iter R) where n is Element of NAT : n > 0 } ,c)),(RealPoset [.0,1.])) <<= (TrCl S) . c by YELLOW_0:32; { (n iter R) where n is Element of NAT : n > 0 } c= the carrier of (FuzzyLattice [:X,X:]) proof let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in { (n iter R) where n is Element of NAT : n > 0 } or t in the carrier of (FuzzyLattice [:X,X:]) ) assume t in { (n iter R) where n is Element of NAT : n > 0 } ; ::_thesis: t in the carrier of (FuzzyLattice [:X,X:]) then consider i being Element of NAT such that A9: t = i iter R and 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 A9; ::_thesis: verum end; then (TrCl R) . c = "\/" ((pi ( { (n iter R) where n is Element of NAT : n > 0 } ,c)),(RealPoset [.0,1.])) by Th32; hence (TrCl R) . c <= (TrCl S) . c by A8, LFUZZY_0:3; ::_thesis: verum end; then TrCl S c= by FUZZY_1:def_2; hence S c= by A1, Th38; ::_thesis: verum end;