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