:: LFUZZY_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

Lm1: for a, b, c, d being real number st a <= b & c <= d holds
min a,c <= min b,d
proof end;

registration
let X be non empty set ;
cluster -> real-yielding Membership_Func of X;
coherence
for b1 being Membership_Func of X holds b1 is real-yielding
;
end;

definition
let X, Y be non empty set ;
let f, g be RMembership_Func of X,Y;
:: original: is_less_than
redefine pred f 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 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th2: :: LFUZZY_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th3: :: LFUZZY_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for R, S being Membership_Func of X holds
( R = S iff ( S c= & R c= ) )
proof end;

theorem :: LFUZZY_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for R being Membership_Func of X holds R c= ;

theorem Th5: :: LFUZZY_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for R, S, T being Membership_Func of X st S c= & T c= holds
T c=
proof end;

theorem Th6: :: LFUZZY_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

definition
let X be non empty set ;
let f, g be Membership_Func of X;
:: original: min
redefine func min f,g -> Membership_Func of X;
commutativity
for f, g being Membership_Func of X holds min f,g = min g,f
;
:: original: max
redefine func max f,g -> Membership_Func of X;
commutativity
for f, g being Membership_Func of X holds max f,g = max g,f
;
end;

theorem :: LFUZZY_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for f, g being Membership_Func of X holds f c=
proof end;

theorem :: LFUZZY_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for f, g being Membership_Func of X holds max f,g c=
proof end;

definition
let X be non empty set ;
let R be RMembership_Func of X,X;
attr R 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 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;
attr R 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 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;
attr R 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= );

Lm2: 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;
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 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;
attr R 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 );

definition
let X be non empty set ;
let R be RMembership_Func of X,X;
redefine attr R is antisymmetric means :: LFUZZY_1:def 9
for x, y being Element of X st R . [x,y] <> 0 & x <> y holds
R . [y,x] = 0;
compatibility
( R is antisymmetric iff for x, y being Element of X st R . [x,y] <> 0 & x <> y holds
R . [y,x] = 0 )
proof end;
end;

:: deftheorem defines antisymmetric LFUZZY_1:def 9 :
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 & x <> y holds
R . [y,x] = 0 );

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

registration
let X be non empty set ;
cluster reflexive symmetric transitive antisymmetric Membership_Func of [:X,X:];
existence
ex b1 being RMembership_Func of X,X st
( b1 is reflexive & b1 is transitive & b1 is symmetric & b1 is antisymmetric )
proof end;
end;

theorem Th9: :: LFUZZY_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th10: :: LFUZZY_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 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 end;
cluster max R,S -> symmetric ;
coherence
max R,S is symmetric
proof end;
end;

theorem Th11: :: LFUZZY_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 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 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 end;
end;

theorem :: LFUZZY_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: LFUZZY_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for r being Relation of X st r is antisymmetric holds
chi r,[:X,X:] is antisymmetric
proof end;

theorem :: LFUZZY_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for r being Relation of X st r is symmetric holds
chi r,[:X,X:] is symmetric
proof end;

theorem :: LFUZZY_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for r being Relation of X st r is transitive holds
chi r,[:X,X:] is transitive
proof end;

theorem :: LFUZZY_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set holds
( Zmf X,X is symmetric & Zmf X,X is antisymmetric & Zmf X,X is transitive )
proof end;

theorem :: LFUZZY_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set holds
( Umf X,X is symmetric & Umf X,X is transitive & Umf X,X is reflexive )
proof end;

theorem :: LFUZZY_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for R being RMembership_Func of X,X holds max R,(converse R) is symmetric
proof end;

theorem :: LFUZZY_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for R being RMembership_Func of X,X holds min R,(converse R) is symmetric
proof end;

theorem :: LFUZZY_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for R, R' being RMembership_Func of X,X st R' is symmetric & R' c= holds
R' c=
proof end;

theorem :: LFUZZY_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for R, R' being RMembership_Func of X,X st R' 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 natural number ;
func n iter R -> RMembership_Func of X,X means :Def10: :: LFUZZY_1:def 10
ex F being Function of NAT , Funcs [:X,X:],[.0,1.] st
( it = F . n & F . 0 = Imf X,X & ( for k being natural number ex Q being RMembership_Func of X,X st
( F . k = Q & F . (k + 1) = Q (#) R ) ) );
existence
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 natural number ex Q being RMembership_Func of X,X st
( F . k = Q & F . (k + 1) = Q (#) R ) ) )
proof 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 natural number 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 natural number ex Q being RMembership_Func of X,X st
( F . k = Q & F . (k + 1) = Q (#) R ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines iter LFUZZY_1:def 10 :
for X being non empty set
for R being RMembership_Func of X,X
for n being natural number
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 natural number ex Q being RMembership_Func of X,X st
( F . k = Q & F . (k + 1) = Q (#) R ) ) ) );

theorem Th22: :: LFUZZY_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for R being RMembership_Func of X,X holds (Imf X,X) (#) R = R
proof end;

theorem Th23: :: LFUZZY_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for R being RMembership_Func of X,X holds R (#) (Imf X,X) = R
proof end;

theorem Th24: :: LFUZZY_1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for R being RMembership_Func of X,X holds 0 iter R = Imf X,X
proof end;

theorem Th25: :: LFUZZY_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for R being RMembership_Func of X,X holds 1 iter R = R
proof end;

theorem Th26: :: LFUZZY_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for R being RMembership_Func of X,X
for n being natural number holds (n + 1) iter R = (n iter R) (#) R
proof end;

theorem Th27: :: LFUZZY_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for R being RMembership_Func of X,X
for m, n being natural number holds (m + n) iter R = (m iter R) (#) (n iter R)
proof end;

theorem :: LFUZZY_1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for R being RMembership_Func of X,X
for m, n being natural number 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;
func TrCl R -> RMembership_Func of X,X equals :: LFUZZY_1:def 11
"\/" { (n iter R) where n is Nat : n > 0 } ,(FuzzyLattice [:X,X:]);
coherence
"\/" { (n iter R) where n is Nat : n > 0 } ,(FuzzyLattice [:X,X:]) is RMembership_Func of X,X
proof end;
end;

:: deftheorem defines TrCl LFUZZY_1:def 11 :
for X being non empty set
for R being RMembership_Func of X,X holds TrCl R = "\/" { (n iter R) where n is Nat : n > 0 } ,(FuzzyLattice [:X,X:]);

theorem Th29: :: LFUZZY_1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Nat : n > 0 } ,[x,y]),(RealPoset [.0,1.])
proof end;

theorem Th30: :: LFUZZY_1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for R being RMembership_Func of X,X holds TrCl R c=
proof end;

theorem Th31: :: LFUZZY_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for R being RMembership_Func of X,X
for n being natural number st n > 0 holds
TrCl R c=
proof end;

theorem Th32: :: LFUZZY_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 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]) "/\" ((@ ("\/" 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 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]) "/\" ("\/" (pi Q,[y,z]),(RealPoset [.0,1.]))) where y is Element of X : verum } = { ("\/" { ((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 }
proof end;

Lm5: 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,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 }
proof end;

Lm6: 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]) "/\" ((@ r') . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.])) where r' is Element of (FuzzyLattice [:X,X:]) : r' in Q }
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 (#) (@ r)) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r 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 (#) (@ 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;

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 . [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]) "/\" (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.])
proof end;

theorem Th34: :: LFUZZY_1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th35: :: LFUZZY_1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th36: :: LFUZZY_1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Nat : ( i > 0 & j > 0 ) } ,(FuzzyLattice [:X,X:])
proof 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 end;
end;

theorem Th37: :: LFUZZY_1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for R being RMembership_Func of X,X
for n being natural number st R is transitive & n > 0 holds
R c=
proof end;

theorem Th38: :: LFUZZY_1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for R being RMembership_Func of X,X st R is transitive holds
R = TrCl R
proof end;

theorem Th39: :: LFUZZY_1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for R, S being RMembership_Func of X,X
for n being natural number st S c= holds
n iter S c=
proof end;

theorem :: LFUZZY_1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;