:: by Takashi Mitsuishi and Grzegorz Bancerek

::

:: Received November 23, 2003

:: Copyright (c) 2003-2018 Association of Mizar Users

registration

let X be non empty set ;

coherence

for b_{1} being Membership_Func of X holds b_{1} is real-valued
;

end;
coherence

for b

definition

let X, Y be non empty set ;

let f, g be RMembership_Func of X,Y;

( 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) )

end;
let f, g be RMembership_Func of X,Y;

:: original: is_less_than

redefine pred f is_less_than g means :: LFUZZY_1:def 1

for x being Element of X

for y being Element of Y holds f . (x,y) <= g . (x,y);

compatibility redefine pred f is_less_than g means :: LFUZZY_1:def 1

for x being Element of X

for y being Element of Y holds f . (x,y) <= g . (x,y);

( 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 end;

:: deftheorem 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) );

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

for R, S being Membership_Func of X st ( for x being Element of X holds R . x = S . x ) holds

R = S

proof 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

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 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=

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 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;
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) ;

:: deftheorem 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= );

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;

compatibility

( R is reflexive iff for x being Element of X holds R . (x,x) = 1 )

end;
let R be RMembership_Func of X,X;

compatibility

( R is reflexive iff for x being Element of X holds R . (x,x) = 1 )

proof end;

:: deftheorem 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 );

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 );

:: deftheorem 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 );

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;

( R is symmetric iff for x, y being Element of X holds R . (x,y) = R . (y,x) )

end;
let R be RMembership_Func of X,X;

redefine attr R is symmetric means :: LFUZZY_1:def 5

for x, y being Element of X holds R . (x,y) = R . (y,x);

compatibility for x, y being Element of X holds R . (x,y) = R . (y,x);

( R is symmetric iff for x, y being Element of X holds R . (x,y) = R . (y,x) )

proof end;

:: deftheorem 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) );

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) );

:: deftheorem 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= );

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 end;

definition

let X be non empty set ;

let R be RMembership_Func of X,X;

( R is transitive iff for x, y, z being Element of X holds (R . [x,y]) "/\" (R . [y,z]) <<= R . [x,z] )

end;
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 for x, y, z being Element of X holds (R . [x,y]) "/\" (R . [y,z]) <<= R . [x,z];

( R is transitive iff for x, y, z being Element of X holds (R . [x,y]) "/\" (R . [y,z]) <<= R . [x,z] )

proof 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] );

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] );

:: deftheorem 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 );

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 ;

coherence

( Imf (X,X) is symmetric & Imf (X,X) is transitive & Imf (X,X) is reflexive & Imf (X,X) is antisymmetric )

end;
coherence

( Imf (X,X) is symmetric & Imf (X,X) is transitive & Imf (X,X) is reflexive & Imf (X,X) is antisymmetric )

proof end;

registration

let X be non empty set ;

ex b_{1} being RMembership_Func of X,X st

( b_{1} is reflexive & b_{1} is transitive & b_{1} is symmetric & b_{1} is antisymmetric )

end;
cluster non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total complex-valued ext-real-valued real-valued reflexive symmetric transitive antisymmetric for RMembership_Func of ,;

existence ex b

( b

proof end;

registration

let X be non empty set ;

let R, S be symmetric RMembership_Func of X,X;

coherence

min (R,S) is symmetric by Th9;

coherence

max (R,S) is symmetric by Th10;

end;
let R, S be symmetric RMembership_Func of X,X;

coherence

min (R,S) is symmetric by Th9;

coherence

max (R,S) is symmetric by Th10;

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=

for R, S being RMembership_Func of X,X st R is transitive & S is transitive holds

min (R,S) c=

proof end;

registration

let X be non empty set ;

let R, S be transitive RMembership_Func of X,X;

coherence

min (R,S) is transitive by Th11;

end;
let R, S be transitive RMembership_Func of X,X;

coherence

min (R,S) is transitive by Th11;

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

end;
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 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

for r being Relation of X st r is_reflexive_in X holds

chi (r,[:X,X:]) is reflexive

proof 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

for r being Relation of X st r is antisymmetric holds

chi (r,[:X,X:]) is antisymmetric

proof 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

for r being Relation of X st r is symmetric holds

chi (r,[:X,X:]) is symmetric

proof 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

for r being Relation of X st r is transitive holds

chi (r,[:X,X:]) is transitive

proof 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 )

( Zmf (X,X) is symmetric & Zmf (X,X) is antisymmetric & Zmf (X,X) is transitive )

proof 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 )

( Umf (X,X) is symmetric & Umf (X,X) is transitive & Umf (X,X) is reflexive )

proof 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

for R being RMembership_Func of X,X holds max (R,(converse R)) is symmetric

proof 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

for R being RMembership_Func of X,X holds min (R,(converse R)) is symmetric

proof 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=

for R, R9 being RMembership_Func of X,X st R9 is symmetric & R9 c= holds

R9 c=

proof 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=

for R, R9 being RMembership_Func of X,X st R9 is symmetric & R c= holds

min (R,(converse R)) c=

proof end;

definition

let X be non empty set ;

let R be RMembership_Func of X,X;

let n be Nat;

ex b_{1} being RMembership_Func of X,X ex F being sequence of (Funcs ([:X,X:],[.0,1.])) st

( b_{1} = 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 ) ) )

for b_{1}, b_{2} being RMembership_Func of X,X st ex F being sequence of (Funcs ([:X,X:],[.0,1.])) st

( b_{1} = 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 sequence of (Funcs ([:X,X:],[.0,1.])) st

( b_{2} = 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

b_{1} = b_{2}

end;
let R be RMembership_Func of X,X;

let n be Nat;

func n iter R -> RMembership_Func of X,X means :Def9: :: LFUZZY_1:def 9

ex F being sequence of (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 F being sequence of (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 ) ) );

ex b

( b

( F . k = Q & F . (k + 1) = Q (#) R ) ) )

proof end;

uniqueness for b

( b

( F . k = Q & F . (k + 1) = Q (#) R ) ) ) & ex F being sequence of (Funcs ([:X,X:],[.0,1.])) st

( b

( F . k = Q & F . (k + 1) = Q (#) R ) ) ) holds

b

proof 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 b_{4} being RMembership_Func of X,X holds

( b_{4} = n iter R iff ex F being sequence of (Funcs ([:X,X:],[.0,1.])) st

( b_{4} = 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 ) ) ) );

for X being non empty set

for R being RMembership_Func of X,X

for n being Nat

for b

( b

( b

( F . k = Q & F . (k + 1) = Q (#) R ) ) ) );

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

for R being RMembership_Func of X,X

for n being Nat holds (n + 1) iter R = (n iter R) (#) R

proof 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)

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 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)

for R being RMembership_Func of X,X

for m, n being Nat holds (m * n) iter R = m iter (n iter R)

proof end;

definition

let X be non empty set ;

let R be RMembership_Func of X,X;

"\/" ( { (n iter R) where n is Element of NAT : n > 0 } ,(FuzzyLattice [:X,X:])) is RMembership_Func of X,X

end;
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:]));

"\/" ( { (n iter R) where n is Element of NAT : n > 0 } ,(FuzzyLattice [:X,X:])) is RMembership_Func of X,X

proof 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:]));

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.]))

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 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=

for R being RMembership_Func of X,X

for n being Nat st n > 0 holds

TrCl R c=

proof 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.]))

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 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 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)

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 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 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 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 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 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 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 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 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 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:]))

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 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:]))

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 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:]))

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 end;

registration
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=

for R being RMembership_Func of X,X

for n being Nat st R is transitive & n > 0 holds

R c=

proof 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=

for R, S being RMembership_Func of X,X

for n being Nat st S c= holds

n iter S c=

proof 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=

for R, S being RMembership_Func of X,X st S is transitive & S c= holds

S c=

proof end;