text:
:: Transitive Closure of Fuzzy Relations
::  by Takashi Mitsuishi and Grzegorz Bancerek

environ

 vocabularies NUMBERS, XBOOLE_0, VALUED_0, FUZZY_1, FUZZY_2, LATTICE3,
      SUBSET_1, FUNCT_1, XXREAL_0, RELAT_1, ZFMISC_1, TARSKI, VALUED_1,
      RELAT_2, FUZZY_4, CARD_1, LATTICES, PARTFUN1, LFUZZY_0, EQREL_1,
      XXREAL_1, SEQ_4, FUNCT_3, FUNCT_7, FUNCT_2, ARYTM_3, STRUCT_0, QC_LANG1,
      CARD_3, FUNCOP_1, REWRITE1, WAYBEL_0, NEWTON, ORDINAL2, LATTICE2,
      WAYBEL_1, NAT_1, LFUZZY_1, REAL_1, XCMPLX_0;
 notations TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, FUNCT_1, FUNCT_2, ORDINAL1,
      NUMBERS, XCMPLX_0, DOMAIN_1, PARTFUN1, CARD_3, RELAT_2, BINOP_1, FUNCT_3,
      RFUNCT_1, SUBSET_1, XREAL_0, NAT_1, SEQ_4, VALUED_0, RCOMP_1, RELSET_1,
      STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, WAYBEL_1, WAYBEL_3,
      FUZZY_1, FUZZY_2, FUZZY_4, FUNCOP_1, LFUZZY_0, XXREAL_0;
 constructors DOMAIN_1, SQUARE_1, RFUNCT_1, MONOID_0, WAYBEL_3, FUZZY_2,
      FUZZY_4, LFUZZY_0, SEQ_4, RELSET_1, FUNCOP_1, FUZZY_1;
 registrations XBOOLE_0, SUBSET_1, XREAL_0, NAT_1, MEMBERED, STRUCT_0,
      LATTICE3, MONOID_0, YELLOW_1, WAYBEL10, WAYBEL17, LFUZZY_0, RELAT_1,
      FUNCT_2, NUMBERS, FUZZY_1, RELSET_1, VALUED_0, ORDINAL1, CARD_1;
 requirements BOOLE, SUBSET, NUMERALS, REAL, ARITHM;
 definitions TARSKI, XBOOLE_0, FUZZY_1;
 equalities BINOP_1;
 expansions FUZZY_1;
 theorems XBOOLE_0, ZFMISC_1, WAYBEL_1, RELAT_1, LATTICE3, YELLOW_0, TARSKI,
      SEQ_4, YELLOW_2, WAYBEL_3, CARD_3, YELLOW_1, FUNCOP_1, FUZZY_2, FUZZY_4,
      FUNCT_3, FUZZY_1, PARTFUN1, LFUZZY_0, RELAT_2, ORDINAL1, XXREAL_0,
      BINOP_1, RELSET_1, FUNCT_2;
 schemes FRAENKEL, RECDEF_1, NAT_1, LFUZZY_0;

begin :: Inclusion of fuzzy relations

reserve X, Y for non empty set;

registration
  let X;
  cluster -> real-valued for Membership_Func of X;
  coherence;
end;

definition
  let X,Y;
  let f,g be RMembership_Func of X,Y;
  redefine pred f is_less_than g means

  for x being Element of X, y being Element of Y holds f.(x,y) <= g.(x,y);
  compatibility
  proof
    thus f is_less_than g iff for x being Element of X, y being Element of Y
    holds f.(x,y) <= g.(x,y)
    proof
      hereby
        assume
A1:     f is_less_than g;
        thus for x being Element of X, y being Element of Y holds f.(x,y) <= g
        .(x,y )
        proof
          let x be Element of X, y be Element of Y;
          dom f = [:X,Y:] & [x,y] in [:X,Y:] by FUNCT_2:def 1;
          hence thesis by A1;
        end;
      end;
      assume
A2:   for x being Element of X, y being Element of Y holds f.(x,y) <= g.(x,y);
A3:   for c being set st c in dom f holds f.c <= g.c
      proof
        let c be set;
        assume
A4:     c in dom f;
        then consider x,y being object such that
A5:     [x,y] = c by RELAT_1:def 1;
        reconsider y as Element of Y by A4,A5,ZFMISC_1:87;
        reconsider x as Element of X by A4,A5,ZFMISC_1:87;
        f.(x,y) <= g.(x,y) by A2;
        hence thesis by A5;
      end;
      dom g = [:X,Y:] by FUNCT_2:def 1;
      hence thesis by A3;
    end;
  end;
end;

theorem Th1:
  for R,S being Membership_Func of X st for x being Element of X
  holds R.x = S.x holds R = S
proof
  let R,S be Membership_Func of X;
  assume for x being Element of X holds R.x = S.x;
  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 thesis by A1,PARTFUN1:5;
end;

theorem Th2:
  for R,S being RMembership_Func of X,Y st for x being Element of X
  , y being Element of Y holds R.(x,y) = S.(x,y) holds R = S
proof
  let R,S be RMembership_Func of X,Y;
  assume
A1: for x being Element of X, y being Element of Y holds R.(x,y) = S.(x, y);
A2: for x,y being object st [x,y] in dom R holds R.(x,y) = S.(x,y)
  proof
    let x,y be object;
    assume
A3: [x,y] in dom R;
    then reconsider x as Element of X by ZFMISC_1:87;
    reconsider y as Element of Y by A3,ZFMISC_1:87;
    R.(x,y) = S.(x,y) by A1;
    hence thesis;
  end;
  dom R = [:X,Y:] & dom S = [:X,Y:] by FUNCT_2:def 1;
  hence thesis by A2,BINOP_1:20;
end;

theorem Th3:
  for R,S being Membership_Func of X holds R = S iff R c= S & S c= R
proof
  let R,S be Membership_Func of X;
  thus R=S implies R c= S & S c= R;
  assume
A1: R c= S & S c= R;
  for x being Element of X holds R.x = S.x
  proof
    let x be Element of X;
    R.x <= S.x & S.x <= R.x by A1;
    hence thesis by XXREAL_0:1;
  end;
  hence thesis by Th1;
end;

theorem
  for R being Membership_Func of X holds R c= R;

theorem Th5:
  for R,S,T being Membership_Func of X holds R c= S & S c= T implies R c= T
proof
  let R,S,T be Membership_Func of X;
  assume
A1: R c= S & S c= T;
  for x being Element of X holds R.x <= T.x
  proof
    let x be Element of X;
    R.x <= S.x & S.x <= T.x by A1;
    hence thesis by XXREAL_0:2;
  end;
  hence thesis;
end;

theorem Th6:
  for X,Y,Z being non empty set, R,S being RMembership_Func of X,Y,
T,U being RMembership_Func of Y,Z holds R c= S & T c= U implies R(#)T c= S(#)U
proof
  let X,Y,Z be non empty set;
  let R,S be RMembership_Func of X,Y;
  let T,U be RMembership_Func of Y,Z;
  assume
A1: R c= S & T c= U;
  for c being Element of [:X,Z:] holds (R(#)T).c <= (S(#)U).c
  proof
    let c be Element of [:X,Z:];
    consider x,z being object 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 be set st y in Y holds R. [x,y] <= S. [x,y] & T. [y,z] <= U. [y, z]
    proof
      let y be set;
      assume y in Y;
      then [x,y] in [:X,Y:] & [y,z] in [:Y,Z:] by A3,ZFMISC_1:87;
      hence thesis by A1;
    end;
    hence thesis by A2,A3,FUZZY_4:18;
  end;
  hence thesis;
end;

definition
  let X be non empty set;
  let f,g be Membership_Func of X;
  redefine func min(f,g);
  commutativity;
  redefine func max(f,g);
  commutativity;
end;

theorem
  for f,g being Membership_Func of X holds min(f,g) c= f
proof
  let f,g be Membership_Func of X;
  let x be Element of X;
  min(f,g).x = min(f.x,g.x) by FUZZY_1:def 3;
  hence min(f,g).x <= f.x by XXREAL_0:17;
end;

theorem
  for f,g being Membership_Func of X holds f c= max(f,g)
proof
  let f,g be Membership_Func of X;
  let x be Element of X;
  max(f,g).x = max(f.x,g.x) by FUZZY_1:def 4;
  hence thesis by XXREAL_0:25;
end;

begin :: Properties of fuzzy relations

definition
  let X be non empty set;
  let R be RMembership_Func of X,X;
  attr R is reflexive means
  Imf(X,X) c= R;
end;

definition
  let X be non empty set;
  let R be RMembership_Func of X,X;
  redefine attr R is reflexive means
  for x being Element of X holds R.( x,x) = 1;
  compatibility
  proof
    hereby
      assume R is reflexive;
      then
A1:   Imf(X,X) c= R;
      thus for x being Element of X holds R.(x,x) = 1
      proof
        let x be Element of X;
        Imf(X,X).(x,x) <= R.(x,x) by A1;
        then R.(x,x) <= 1 & R.(x,x) >= 1 by FUZZY_4:4,25;
        hence thesis by XXREAL_0:1;
      end;
    end;
    assume
A2: for x being Element of X holds R.(x,x) = 1;
    let x,y be Element of X;
    per cases;
    suppose
A3:   x = y;
      then Imf(X,X).(x,y) = 1 by FUZZY_4:25;
      hence thesis by A2,A3;
    end;
    suppose
      x <> y;
      then Imf(X,X).(x,y) = 0 by FUZZY_4:25;
      hence thesis by FUZZY_4:4;
    end;
  end;
end;

definition
  let X be non empty set;
  let R be RMembership_Func of X,X;
  attr R is symmetric means
  converse R = R;
end;

definition
  let X be non empty set;
  let R be RMembership_Func of X,X;
  redefine attr R is symmetric means

  for x,y being Element of X holds R .(x,y) = R.(y,x);
  compatibility
  proof
    thus R is symmetric iff for x,y being Element of X holds R.(x,y) = R.(y,x)
    proof
      thus R is symmetric implies
      for x,y being Element of X holds R.(x,y) = R.(y,x) by FUZZY_4:26;
      assume
A1:   for x,y being Element of X holds R.(x,y) = R.(y,x);
A2:   for x,y being object st [x,y] in dom R
holds (converse R).(x,y) = R.(x, y)
      proof
        let x,y be object;
        assume [x,y] in dom R;
        then reconsider x,y as Element of X by ZFMISC_1:87;
        R.(x,y) = R.(y,x) by A1;
        hence thesis by FUZZY_4:26;
      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 thesis;
    end;
  end;
end;

definition
  let X be non empty set;
  let R be RMembership_Func of X,X;
  attr R is transitive means

  R (#) R c= R;
end;

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, z being Element of Z
holds rng min(R,S,x,z) = the set of all
R. [x,y] "/\" S. [y,z] where y is Element of Y & rng min(R,S,x,z) <> {}
proof
  let X,Y,Z be non empty set;
  let R be RMembership_Func of X,Y;
  let S be RMembership_Func of Y,Z;
  let x be Element of X, z being Element of Z;
  set L = the set of all R. [x,y] "/\" S. [y,z] where y is Element of Y;
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 be object holds c in L iff c in rng min(R,S,x,z)
  proof
    let c be object;
    hereby
      assume c in L;
      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;
    end;
    assume c in rng min(R,S,x,z);
    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 thesis;
  end;
  hence rng min(R,S,x,z) = L by TARSKI:2;
  thus rng min(R,S,x,z) <> {};
end;

definition
  let X be non empty set;
  let R be RMembership_Func of X,X;
  redefine attr R is transitive means
  for x,y,z being Element of X holds R. [x ,y] "/\" R. [y,z] <<= R. [x,z];
  compatibility
  proof
    thus R is transitive iff for x,y,z being Element of X holds R. [x,y] "/\"
    R. [y,z] <<= R. [x,z]
    proof
      hereby
        assume R is transitive;
        then
A1:     R (#) R c= R;
        thus for x,y,z being Element of X holds R. [x,y] "/\" R. [y,z] <<= R.
        [x,z]
        proof
          let x,y,z be Element of X;
          R.(x,y) "/\" R.(y,z) in the set of all
R.(x,y9) "/\" R.(y9,z) where y9 is
          Element of X;
          then R.(x,y) "/\" R.(y,z) <<= "\/"((the set of all
R.(x,y9) "/\" R.(y9,z) where y9
is Element of X), 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;
          then R. [x,y] "/\" R. [y,z] <= R. [x,z] by A2,XXREAL_0:2;
          hence thesis by LFUZZY_0:3;
        end;
      end;
      assume
A3:   for x,y,z being Element of X holds R. [x,y] "/\" R. [y,z] <<= R. [x,z];
      thus R (#) R c= R
      proof
        let x,z be Element of X;
        set W = rng min(R,R,x,z);
        for r being Real st r in W holds r <= R. [x,z]
        proof
          let r be Real;
          assume r in W;
          then r in the set of all
R. [x,y9] "/\" R. [y9,z] where y9 is Element of X 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 thesis by A4,LFUZZY_0:3;
        end;
        then upper_bound W <= R. [x,z] by SEQ_4:144;
        hence thesis by FUZZY_4:def 3;
      end;
    end;
  end;
end;

definition
  let X be non empty set;
  let R be RMembership_Func of X,X;
  attr R is antisymmetric means

  for x,y being Element of X holds R.(x,y ) <> 0 & R.(y,x) <> 0 implies x = y;
end;

registration
  let X;
  cluster Imf(X,X) -> symmetric transitive reflexive antisymmetric;
  coherence
  proof
    thus Imf(X,X) is symmetric
    proof
      let x,y be Element of X;
      per cases;
      suppose
        x=y;
        hence thesis;
      end;
      suppose
A1:     not x=y;
        hence Imf(X,X).(x,y) = 0 by FUZZY_4:25
          .= Imf(X,X).(y,x) by A1,FUZZY_4:25;
      end;
    end;
    thus Imf(X,X) is transitive
    proof
      let x,y,z be Element of X;
      per cases;
      suppose
A2:     x = z;
        thus thesis
        proof
          per cases;
          suppose
A3:         x = y;
            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 thesis by LFUZZY_0:3;
          end;
          suppose
A4:         not x=y;
            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 thesis by LFUZZY_0:3;
          end;
        end;
      end;
      suppose
A5:     not x=z;
        thus thesis
        proof
          per cases;
          suppose
A6:         x=y;
            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 thesis by LFUZZY_0:3;
          end;
          suppose
A7:         x <> y;
            thus thesis
            proof
              per cases;
              suppose
A8:             y=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 thesis by LFUZZY_0:3;
              end;
              suppose
A9:             y <> 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 thesis by LFUZZY_0:3;
              end;
            end;
          end;
        end;
      end;
    end;
    thus Imf(X,X) is reflexive;
    thus for x,y being Element of X holds Imf(X,X).(x,y) <> 0 & Imf(X,X).(y,x)
    <> 0 implies x = y by FUZZY_4:25;
  end;
end;

registration
  let X;
  cluster reflexive transitive symmetric antisymmetric for
RMembership_Func of X,X;
  existence
  proof
    take Imf(X,X);
    thus thesis;
  end;
end;

theorem Th9:
  for R,S being RMembership_Func of X,X holds R is symmetric & S is
  symmetric implies converse min(R,S) = min(R,S)
by FUZZY_4:8;

theorem Th10:
  for R,S being RMembership_Func of X,X holds R is symmetric & S
  is symmetric implies converse max(R,S) = max(R,S)
by FUZZY_4:7;

registration
  let X;
  let R,S be symmetric RMembership_Func of X,X;
  cluster min(R,S) -> symmetric;
  coherence
  by Th9;
  cluster max(R,S) -> symmetric;
  coherence
  by Th10;
end;

theorem Th11:
  for R,S being RMembership_Func of X,X holds R is transitive & S
  is transitive implies min(R,S) (#) min(R,S) c= min(R,S)
proof
  let R,S be RMembership_Func of X,X;
  assume that
A1: R is transitive and
A2: S is transitive;
  let x be Element of X, y be Element of X;
  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(#)S c= S by A2;
  then (S(#)S).(x,y) <= S.(x,y);
  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(#)R c= R by A1;
  then (R(#)R).(x,y) <= R.(x,y);
  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(R,S) (#) min(R,S)) c= min(min(R,S) (#) R, min(R,S) (#) S) 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];
  min(R,S) (#) S c= min(R(#)S, S(#)S) by FUZZY_4:16;
  then
A8: (min(R,S) (#) S). [x,y] <= min(R(#)S, S(#)S). [x,y];
  min(R,S) (#) R c= min(R(#)R, S(#)R) 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 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 thesis by FUZZY_1:def 3;
end;

registration
  let X;
  let R,S be transitive RMembership_Func of X,X;
  cluster min(R,S) -> transitive;
  coherence
  by Th11;
end;

definition
  let A be set, X be non empty set;
  redefine func chi(A,X) -> Membership_Func of X;
  coherence
  proof
    dom chi(A,X) = X by FUNCT_3:def 3;
    hence chi(A,X) is Membership_Func of X by FUNCT_2:def 1;
  end;
end;

theorem
  for r being Relation of X st r is_reflexive_in X holds chi(r,[:X,X:])
  is reflexive
proof
  let r be Relation of X;
  assume
A1: r is_reflexive_in X;
  for x being Element of X holds chi(r,[:X,X:]).(x,x) = 1
  proof
    let x be Element of X;
    [x,x] in r by A1,RELAT_2:def 1;
    hence thesis by FUNCT_3:def 3;
  end;
  hence thesis;
end;

theorem
  for r being Relation of X st r is antisymmetric holds chi(r,[:X,X:])
  is antisymmetric
proof
  let r be Relation of X;
  assume r is antisymmetric;
  then
A1: r is_antisymmetric_in field r by RELAT_2:def 12;
  for x,y being Element of X holds chi(r,[:X,X:]).(x,y) <> 0 & chi(r,[:X,X
  :]).(y,x) <> 0 implies x = y
  proof
    let x,y be Element of X;
    assume that
A2: chi(r,[:X,X:]).(x,y) <> 0 and
A3: chi(r,[:X,X:]).(y,x) <> 0;
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 thesis by A3,A4,FUNCT_3:def 3,RELAT_1:15;
  end;
  hence thesis;
end;

theorem
  for r being Relation of X st r is symmetric holds chi(r,[:X,X:]) is symmetric
proof
  let r be Relation of X;
  assume r is symmetric;
  then
A1: r is_symmetric_in field r by RELAT_2:def 11;
  let x,y be Element of X;
A2: x in field r & y in field r & [x,y] in r implies [y,x] in r 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;
  per cases;
  suppose
A4: [x,y] in r;
    then chi(r,[:X,X:]). [x,y] = 1 by FUNCT_3:def 3;
    hence thesis by A2,A4,FUNCT_3:def 3,RELAT_1:15;
  end;
  suppose
    not [x,y] in r;
    then ( not [y,x] in r)& chi(r,[:X,X:]). [x,y] = 0 by A3,FUNCT_3:def 3
,RELAT_1:15;
    hence thesis by FUNCT_3:def 3;
  end;
end;

theorem
  for r being Relation of X st r is transitive holds chi(r,[:X,X:]) is
  transitive
proof
  let r be Relation of X;
  assume
A1: r is transitive;
  let x,y,z be Element of X;
  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;
  per cases;
  suppose
A3: [x,y] in r;
    thus thesis
    proof
      per cases;
      suppose
A4:     [y,z] in r;
        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 thesis by LFUZZY_0:3;
      end;
      suppose
A5:     not [y,z] in r;
        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 thesis by LFUZZY_0:3;
      end;
    end;
  end;
  suppose
A6: not [x,y] in r;
    thus thesis
    proof
      per cases;
      suppose
A7:     [y,z] in r;
        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 thesis by LFUZZY_0:3;
      end;
      suppose
A8:     not [y,z] in r;
        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 thesis by LFUZZY_0:3;
      end;
    end;
  end;
end;

theorem
  Zmf(X,X) is symmetric antisymmetric transitive
proof
  thus Zmf(X,X) is symmetric
  proof
    let x,y be Element of X;
    Zmf(X,X). [x,y] = 0 & Zmf(X,X). [y,x] = 0 by FUZZY_4:21;
    hence thesis;
  end;
  thus Zmf(X,X) is antisymmetric
  proof
    let x,y be Element of X;
    Zmf(X,X). [x,y] = 0 by FUZZY_4:21;
    hence thesis;
  end;
  thus Zmf(X,X) is transitive
  proof
    let x,y,z be Element of X;
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 thesis by A1,LFUZZY_0:3;
  end;
end;

theorem
  Umf(X,X) is symmetric transitive reflexive
proof
  thus Umf(X,X) is symmetric
  proof
    let x,y be Element of X;
    thus Umf(X,X).(x,y) = Umf(X,X). [x,y] .= 1 by FUZZY_4:21
      .= Umf(X,X). [y,x] by FUZZY_4:21
      .= Umf(X,X).(y,x);
  end;
  thus Umf(X,X) is transitive
  proof
    let x,y,z be Element of X;
    Umf(X,X). [x,y] "/\" Umf(X,X). [y,z] = min(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 thesis by LFUZZY_0:3;
  end;
  thus Umf(X,X) is reflexive
  proof
    let x be Element of X;
    Umf(X,X). [x,x] = 1 by FUZZY_4:21;
    hence thesis;
  end;
end;

theorem
  for R being RMembership_Func of X,X holds max(R,converse R) is symmetric
proof
  let R be RMembership_Func of X,X;
  set S = max(R,converse R);
  let x,y be Element of X;
  thus S.(x,y) = S. [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
    .= S. [y,x] by FUZZY_1:def 4
    .= S.(y,x);
end;

theorem
  for R being RMembership_Func of X,X holds min(R,converse R) is symmetric
proof
  let R be RMembership_Func of X,X;
  set S = min(R,converse R);
  let x,y be Element of X;
  thus S.(x,y) = S. [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
    .= S. [y,x] by FUZZY_1:def 3
    .= S.(y,x);
end;

theorem
  for R being RMembership_Func of X,X for R9 being RMembership_Func of X
  ,X st R9 is symmetric & R c= R9 holds max(R, converse R) c= R9
proof
  let R be RMembership_Func of X,X;
  let T be RMembership_Func of X,X;
  assume that
A1: T is symmetric and
A2: R c= T;
  let x,y be Element of X;
  R. [y,x] <= T. [y,x] by A2;
  then R.(y,x) <= T.(y,x);
  then
A3: R.(y,x) <= T.(x,y) by A1;
  R. [x,y] <= T. [x,y] by A2;
  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 thesis by FUZZY_1:def 4;
end;

theorem
  for R being RMembership_Func of X,X for R9 being RMembership_Func of X
  ,X st R9 is symmetric & R9 c= R holds R9 c= min(R, converse R)
proof
  let R be RMembership_Func of X,X;
  let T be RMembership_Func of X,X;
  assume that
A1: T is symmetric and
A2: T c= R;
  let x,y be Element of X;
  T. [y,x] <= R. [y,x] by A2;
  then T.(y,x) <= R.(y,x);
  then
A3: T.(x,y) <= R.(y,x) by A1;
  T. [x,y] <= R. [x,y] by A2;
  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 thesis by FUZZY_1:def 3;
end;

begin :: Transitive closure of a fuzzy relation

definition
  let X be non empty set;
  let R be RMembership_Func of X,X;
  let n be Nat;
  func n iter R -> RMembership_Func of X,X means
  :Def9:
  ex F being sequence of Funcs([:X,X:],[. 0,1 .]) st it = F.n & F.0 = Imf(X,X)
  & for k being Nat
  ex Q being RMembership_Func of X,X st F.k = Q & F.(k + 1) = Q (#) R;
  existence
  proof
    reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
    set D = the carrier of FuzzyLattice [:X,X:];
    defpred P[set,set,set] means ex Q being Element of D st $2 = Q & $3 = @Q
    (#) R;
A1: for k being Nat for x being Element of D ex y being Element
    of D st P[k,x,y]
    proof
      let k be Nat;
      let Q be Element of D;
      set y = @Q (#) R;
      reconsider y9 = ([:X,X:],y)@ as Element of D;
      take y9;
      thus thesis by LFUZZY_0:def 6;
    end;
    consider F being sequence of D such that
A2: F.0 = ([:X,X:],Imf(X,X))@ & for k being Nat holds P[k,F
    .k,F.(k+1)] from RECDEF_1:sch 2 (A1);
    reconsider F as sequence of 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;
    thus ex F being sequence of 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
    proof
      take F;
      thus IT9 = F.n by LFUZZY_0:def 5;
      thus F.0 = Imf(X,X) by A2,LFUZZY_0:def 6;
      thus for k being Nat ex Q being RMembership_Func of X,X st F.
      k = Q & F.(k + 1) = Q (#) R
      proof
        let k be Nat;
        reconsider n=k as Element of NAT by ORDINAL1:def 12;
        reconsider Q9 = F.n as Element of D by LFUZZY_0:14;
        reconsider Q = @Q9 as RMembership_Func of X,X;
        take Q;
        thus F.k = Q by LFUZZY_0:def 5;
        P[n,F.n,F.(n+1)] by A2;
        hence thesis;
      end;
    end;
  end;
  uniqueness
  proof
    let S,T be RMembership_Func of X,X;
    given F being sequence of 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;
    given G being sequence of 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;
    defpred P[Nat] means F.$1 = G.$1;
A9: for k being Nat st P[k] holds P[k+1]
    proof
      let k be Nat;
      assume
A10:  F.k = G.k;
      (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 thesis by A10;
    end;
A11: P[0] by A4,A7;
    for k being Nat holds P[k] from NAT_1:sch 2(A11,A9);
    hence S=T by A3,A6;
  end;
end;

reserve X for non empty set;
reserve R for RMembership_Func of X,X;

theorem Th22:
  Imf(X,X) (#) R = R
proof
A1: for x,y being object st [x,y] in dom (Imf(X,X) (#) R)
holds (Imf(X,X) (#) R).(x,y) = R.(x,y)
  proof
    let x,y be object;
    assume [x,y] in dom (Imf(X,X) (#) R);
    then reconsider x,y as Element of X by ZFMISC_1:87;
    set S = the set of all Imf(X,X).(x,z) "/\" R.(z,y) where z is Element of X;
    for c being Element of RealPoset [. 0,1 .] st c in S holds c <<= R. [x ,y]
    proof
      let c be Element of RealPoset [. 0,1 .];
      assume c in S;
      then consider z being Element of X such that
A2:   c = Imf(X,X).(x,z) "/\" R.(z,y);
      per cases;
      suppose
A3:     x = z;
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 thesis by LFUZZY_0:3;
      end;
      suppose
A5:     x <> z;
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 thesis by LFUZZY_0:3;
      end;
    end;
    then
A7: (Imf(X,X) (#) R).(x,y) = "\/"((the set of all
Imf(X,X).(x,z) "/\" R.(z,y) where z is
Element of X), RealPoset [. 0,1 .]) & R.(x,y) is_>=_than S
    by LATTICE3:def 9,LFUZZY_0:22;
    for b being Element of RealPoset [. 0,1 .] st b is_>=_than S holds R.
    (x,y) <<= b
    proof
      let b be Element of RealPoset [. 0,1 .];
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 S;
      assume b is_>=_than S;
      hence thesis by A9,LATTICE3:def 9;
    end;
    hence thesis by A7,YELLOW_0:32;
  end;
  dom (Imf(X,X) (#) R) = [:X,X:] by FUNCT_2:def 1
    .= dom R by FUNCT_2:def 1;
  hence thesis by A1,BINOP_1:20;
end;

theorem Th23:
  R (#) Imf(X,X) = R
proof
A1: for x,y being object st [x,y] in dom (R (#) Imf(X,X))
 holds (R (#) Imf(X,X)).(x,y) = R.(x,y)
  proof
    let x,y be object;
    assume [x,y] in dom (R (#) Imf(X,X));
    then reconsider x,y as Element of X by ZFMISC_1:87;
    set S = the set of all R.(x,z) "/\" Imf(X,X).(z,y) where z is Element of X;
    for c being Element of RealPoset [. 0,1 .] st c in S holds c <<= R. [x ,y]
    proof
      let c be Element of RealPoset [. 0,1 .];
      assume c in S;
      then consider z being Element of X such that
A2:   c = R.(x,z) "/\" Imf(X,X).(z,y);
      per cases;
      suppose
A3:     y = z;
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 thesis by LFUZZY_0:3;
      end;
      suppose
A5:     not y = z;
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 thesis by LFUZZY_0:3;
      end;
    end;
    then
A7: (R (#) Imf(X,X)).(x,y) = "\/"((the set of all
R.(x,z) "/\" Imf(X,X).(z,y) where z is
Element of X), RealPoset [. 0,1 .]) & R.(x,y) is_>=_than S
    by LATTICE3:def 9,LFUZZY_0:22;
    for b being Element of RealPoset [. 0,1 .] st b is_>=_than S holds R.
    (x,y) <<= b
    proof
      let b be Element of RealPoset [. 0,1 .];
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 S;
      assume b is_>=_than S;
      hence thesis by A9,LATTICE3:def 9;
    end;
    hence thesis by A7,YELLOW_0:32;
  end;
  dom (R (#) Imf(X,X)) = [:X,X:] by FUNCT_2:def 1
    .= dom R by FUNCT_2:def 1;
  hence thesis by A1,BINOP_1:20;
end;

theorem Th24:
  0 iter R = Imf(X,X)
proof
  ex F being sequence of 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 thesis;
end;

theorem Th25:
  1 iter R = R
proof
  consider F being sequence of 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 thesis by A1,Th22;
end;

theorem Th26:
  for n being Nat holds (n+1) iter R = (n iter R) (#) R
proof
  let n be Nat;
  consider f being sequence of 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 thesis by A1,A2,Def9;
end;

theorem Th27:
  for m,n being Nat holds (m+n) iter R = (m iter R) (#) (n iter R)
proof
  let m,n be Nat;
  defpred P[Nat] means (m+ $1) iter R = (m iter R) (#) ($1 iter R);
A1: for n being Nat st P[n] holds P[n+1]
  proof
    let n be Nat;
    assume
A2: (m+n) iter R = (m iter R) (#) (n iter R);
    thus ((m) iter R) (#) ((n+1) iter R) = (m iter R) (#) ((n iter R) (#)R )
    by Th26
      .= ((m+n) iter R) (#) R by A2,LFUZZY_0:23
      .= ((m+n)+1) iter R by Th26
      .= (m+(n+1)) iter R;
  end;
  (m iter R) (#) (0 iter R) = (m iter R) (#) Imf(X,X) by Th24
    .= m iter R by Th23;
  then
A3: P[0];
  for m being Nat holds P[m] from NAT_1:sch 2(A3,A1);
  hence thesis;
end;

theorem
  for m,n being Nat holds (m*n) iter R = m iter (n iter R)
proof
  let m,n be Nat;
  defpred P[Nat] means ($1 * n) iter R = $1 iter (n iter R);
A1: for m being Nat st P[m] holds P[m+1]
  proof
    let m be Nat;
    assume
A2: (m*n) iter R = m iter (n iter R);
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 thesis by A3;
  end;
  (0*n) iter R = Imf(X,X) by Th24
    .= 0 iter (n iter R) by Th24;
  then
A4: P[0];
  for m being Nat holds P[m] from NAT_1:sch 2(A4,A1);
  hence thesis;
end;

definition
  let X be non empty set;
  let R be RMembership_Func of X,X;
  func TrCl R -> RMembership_Func of X,X equals
  "\/"({n iter R where n is
  Element of NAT : n > 0},FuzzyLattice [:X,X:]);
  coherence
  proof
    set S = "\/"({n iter R where n is Element of NAT : n > 0}, FuzzyLattice [:
    X,X:]);
    S = @S by LFUZZY_0:def 5;
    hence thesis;
  end;
end;

theorem Th29:
  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
  set Q = {n iter R where n is Element of NAT : n > 0};
  Q c= the carrier of FuzzyLattice [:X,X:]
  proof
    let t be object;
    assume t in Q;
    then ex n being Element of NAT st t = n iter R & n > 0;
    then reconsider t as Membership_Func of [:X,X:];
    ([:X,X:],t)@ is Element of FuzzyLattice [:X,X:];
    then reconsider t as Element of FuzzyLattice [:X,X:] by LFUZZY_0:def 6;
    t in the carrier of FuzzyLattice [:X,X:];
    hence thesis;
  end;
  then reconsider Q as Subset of FuzzyLattice [:X,X:];
  let x,z be Element of X;
  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 thesis by FUNCOP_1:7;
end;

theorem Th30:
  R c= TrCl R
proof
  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 :];
    consider x,y being object such that
A1: [x,y] = c by RELAT_1:def 1;
    reconsider x,y as Element of X by A1,ZFMISC_1:87;
    R = 1 iter R by Th25;
    then R in Q;
    then
A2: R. [x,y] in pi(Q, [x,y]) by CARD_3:def 6;
    (TrCl R). [x,y] = "\/"(pi(Q, [x,y]), RealPoset [. 0,1 .]) by Th29;
    then R. [x,y] <<= (TrCl R). [x,y] by A2,YELLOW_2:22;
    hence thesis by A1,LFUZZY_0:3;
  end;
  hence thesis;
end;

theorem Th31:
  for n being Nat st n > 0 holds n iter R c= TrCl R
proof
  let n9 be Nat;
  assume
A1: n9 > 0;
  for c being Element of [: X,X :] holds (n9 iter R).c <= (TrCl R).c
  proof
    reconsider 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 :];
    consider x,y being object such that
A2: [x,y] = c by RELAT_1:def 1;
    reconsider x,y as Element of X by A2,ZFMISC_1:87;
    n9 iter R in Q by A1;
    then
A3: (n9 iter R). [x,y] in pi(Q, [x,y]) by CARD_3:def 6;
    (TrCl R). [x,y] = "\/"(pi(Q, [x,y]), RealPoset [. 0,1 .]) by Th29;
    then (n9 iter R). [x,y] <<= (TrCl R). [x,y] by A3,YELLOW_2:22;
    hence thesis by A2,LFUZZY_0:3;
  end;
  hence thesis;
end;

theorem Th32:
  for Q being Subset of FuzzyLattice X, x being Element of X holds
  ("\/"(Q,FuzzyLattice X)). x = "\/"(pi(Q, x), RealPoset [. 0,1 .])
proof
  let Q be Subset of FuzzyLattice X;
  let x be Element of X;
A1: 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 thesis by FUNCOP_1:7;
end;

Lm2: for R being RMembership_Func of X,X, Q being Subset of FuzzyLattice [:X,X
:], x,z being Element of X holds the set of all
R.(x,y) "/\" (@("\/"(Q,FuzzyLattice [:X,X:]))
).(y,z) where y is Element of X = the set of all R. [x,y] "/\" "\/"(pi(Q,
[y,z]), RealPoset [. 0,1 .]) where y is Element of X
proof
  let R be RMembership_Func of X,X;
  let Q be Subset of FuzzyLattice [:X,X:];
  let x,z be Element of X;
  defpred P[Element of X] means not contradiction;
  deffunc F(Element of X) = R.(x,$1) "/\" (@("\/"(Q,FuzzyLattice [:X,X:]))).(
  $1,z);
  deffunc G(Element of X) = R. [x,$1] "/\" "\/"(pi(Q, [$1,z]), RealPoset [. 0,
  1 .]);
  for y being Element of X holds R. [x,y] "/\" (@("\/"(Q,FuzzyLattice [:X,
  X:]))). [y,z] = R. [x,y] "/\" "\/"(pi(Q, [y,z]), RealPoset [. 0,1 .])
  proof
    let y be Element of X;
    (@("\/"(Q,FuzzyLattice [:X,X:]))). [y,z] = (("\/"(Q,FuzzyLattice [:X,X
    :]))). [y,z] by LFUZZY_0:def 5
      .= "\/"(pi(Q, [y,z]), RealPoset [. 0,1 .]) by Th32;
    hence thesis;
  end;
  then
A1: for y being Element of X holds F(y) = G(y);
  thus {F(y) where y is Element of X: P[y]} = {G(y9) where y9 is Element of X:
  P[y9]} from FRAENKEL:sch 5(A1);
end;

theorem Th33:
  for R being complete Heyting LATTICE, X being Subset of R, y be
Element of R holds y "/\" "\/"(X,R) = "\/"({y "/\" x where x is Element of R: x
  in X},R)
proof
  let R be complete Heyting LATTICE, X be Subset of R, y be Element of R;
  for z being Element of R holds z "/\" is lower_adjoint by WAYBEL_1:def 19;
  hence thesis by WAYBEL_1:64;
end;

Lm3: for R being RMembership_Func of X,X, Q being Subset of FuzzyLattice [:X,X
:], x,z being Element of X holds the set of all
R. [x,y] "/\" "\/"(pi(Q, [y,z]), RealPoset [.
0,1 .]) where y is Element of X = the set of all "\/"({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
proof
  let R be RMembership_Func of X,X;
  let Q be Subset of FuzzyLattice [:X,X:];
  let x,z be Element of X;
  defpred P[Element of X] means not contradiction;
  deffunc F(Element of X) = R. [x,$1] "/\" "\/"(pi(Q, [$1,z]), RealPoset [. 0,
  1 .]);
  deffunc G(Element of X) = "\/"({R. [x,$1] "/\" b where b is Element of
  RealPoset [. 0,1 .]: b in pi(Q,[$1,z])} ,RealPoset [. 0,1 .]);
  for y being Element of X holds R. [x,y] "/\" "\/"(pi(Q, [y,z]),
RealPoset [. 0,1 .]) = "\/"({R. [x,y] "/\" b where b is Element of RealPoset [.
  0,1 .]: b in pi(Q,[y,z])} ,RealPoset [. 0,1 .])
  proof
    let y be Element of X;
    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 as Subset of product ([:X,X:] --> RealPoset [. 0,1 .]);
    pi(Q, [y,z]) is Subset of RealPoset [. 0,1 .] by FUNCOP_1:7;
    hence thesis by Th33;
  end;
  then
A1: for y being Element of X holds F(y) = G (y);
  {F(y) where y is Element of X:P[y]} = {G(y) where y is Element of X:P[y]
  } from FRAENKEL:sch 5(A1);
  hence thesis;
end;

Lm4: for R being RMembership_Func of X,X, Q being Subset of FuzzyLattice [:X,X
:], x,z being Element of X holds the set of all
"\/"({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 = the set of all "\/"({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
proof
  let R be RMembership_Func of X,X;
  let Q be Subset of FuzzyLattice [:X,X:];
  let x,z be Element of X;
  set RP = RealPoset [. 0,1 .], FL = FuzzyLattice [:X,X:];
  defpred P[Element of X] means not contradiction;
  deffunc F(Element of X) = "\/"({R. [x,$1] "/\" b where b is Element of RP: b
  in pi(Q,[$1,z])} ,RP);
  deffunc G(Element of X) = "\/"({R. [x,$1] "/\" r. [$1,z] where r is Element
  of FL: r in Q} ,RP);
  for y being Element of X holds "\/"({R. [x,y] "/\" b where b is Element
of RP: b in pi(Q,[y,z])} ,RP) = "\/"({R. [x,y] "/\" r. [y,z] where r is Element
  of FL: r in Q} ,RP)
  proof
    let y be Element of X;
    set A = {R. [x,y] "/\" b where b is Element of RP: b in pi(Q,[y,z])}, B =
    {R. [x,y] "/\" r. [y,z] where r is Element of FL: r in Q};
A1: B c= A
    proof
      let a be object;
      assume a in B;
      then consider r being Element of FL 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 thesis by A2;
    end;
    A c= B
    proof
      let a be object;
      assume a in A;
      then consider b be Element of RP such that
A4:   a = R. [x,y] "/\" b and
A5:   b in pi(Q,[y,z]);
      ex f be Function st f in Q & b = f. [y,z] by A5,CARD_3:def 6;
      hence thesis by A4;
    end;
    hence thesis by A1,XBOOLE_0:def 10;
  end;
  then
A6: for y being Element of X holds F(y) = G (y);
  thus {F(y) where y is Element of X:P[y]} = {G(y) where y is Element of X:P[y
  ]} from FRAENKEL:sch 5(A6);
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, z being Element of Z
holds rng min(R,S,x,z) = the set of all
R. [x,y] "/\" S. [y,z] where y is Element of Y & rng min(R,S,x,z) <> {}
proof
  let X,Y,Z being non empty set;
  let R being RMembership_Func of X,Y;
  let S being RMembership_Func of Y,Z;
  let x being Element of X, z being Element of Z;
  set L = the set of all R. [x,y] "/\" S. [y,z] where y is Element of Y;
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 be object holds c in L iff c in rng min(R,S,x,z)
  proof
    let c be object;
    hereby
      assume c in L;
      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;
    end;
    assume c in rng min(R,S,x,z);
    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 thesis;
  end;
  hence rng min(R,S,x,z) = L by TARSKI:2;
  thus rng min(R,S,x,z) <> {};
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, z being Element of Z
holds (R (#) S). [x,z] = "\/"((the set of all
R. [x,y] "/\" S. [y,z] where y is Element of Y), RealPoset [. 0,1 .])
proof
  let X,Y,Z being non empty set;
  let R being RMembership_Func of X,Y;
  let S being RMembership_Func of Y,Z;
  let x being Element of X, z being Element of Z;
  set L = the set of all R. [x,y] "/\" S. [y,z] where y is Element of Y;
  [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 L holds (R
  (#) S). [x,z] <<= b
  proof
    let b be Element of RealPoset [. 0,1 .];
    assume
A3: b is_>=_than the set of all R. [x,y] "/\" S. [y,z] where y is Element of Y;
A4: rng min(R,S,x,z) c= [. 0,1 .] by RELAT_1:def 19;
A5: L = rng min(R,S,x,z) by Lm5;
    for r being Real st r in rng min(R,S,x,z) holds r <= b
    proof
      let r be Real;
      assume
A6:   r in rng min(R,S,x,z);
      then reconsider r as Element of RealPoset [. 0,1 .] by A4,LFUZZY_0:def 3;
      r <<= b by A3,A5,A6,LATTICE3:def 9;
      hence thesis by LFUZZY_0:3;
    end;
    then upper_bound rng min(R,S,x,z) <= b by SEQ_4:144;
    hence thesis by A1,LFUZZY_0:3;
  end;
  for b being Element of RealPoset [. 0,1 .] st b in L holds (R (#) S). [x
  ,z] >>= b
  proof
    let b be Element of RealPoset [. 0,1 .];
    assume b in L;
    then consider y being Element of Y such that
A7: b = R. [x,y] "/\" S. [y,z];
    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 thesis by A1,LFUZZY_0:3;
  end;
  then (R (#) S). [x,z] is_>=_than L by LATTICE3:def 9;
  hence thesis by A2,YELLOW_0:32;
end;

Lm7: for R being RMembership_Func of X,X, Q being Subset of FuzzyLattice [:X,X
:], x,z being Element of X holds {"\/"((the set of all
R. [x,y] "/\" r. [y,z] where y is
Element of X) ,RealPoset [. 0,1 .]) where r is Element of
FuzzyLattice [:X,X:]: r in Q} = {"\/"((the set of all
R. [x,y] "/\" @(r9). [y,z] where y is
Element of X) ,RealPoset [. 0,1 .]) where r9 is Element of
FuzzyLattice [:X,X:]: r9 in Q}
proof
  let R be RMembership_Func of X,X;
  let Q be Subset of FuzzyLattice [:X,X:];
  let x,z be Element of X;
  set FL = FuzzyLattice [:X,X:];
  defpred P[Element of FL] means $1 in Q;
  deffunc F(Element of FL) = "\/"((the set of all
R. [x,y] "/\" $1. [y,z] where y is Element
  of X),RealPoset [. 0,1 .]);
  deffunc G(Element of FL) = "\/"((the set of all
R. [x,y] "/\" @($1). [y,z] where y is
  Element of X) ,RealPoset [. 0,1 .]);
  for r being Element of FL st r in Q holds "\/"((the set of all
R. [x,y] "/\" r. [y,z]
where y is Element of X),RealPoset [. 0,1 .]) = "\/"((the set of all R. [x,
y] "/\" @(r). [y,z] where y is Element of X),RealPoset [. 0,
  1 .])
  proof
    let r be Element of FL;
    assume r in Q;
    the set of all R. [x,y] "/\" r. [y,z] where y is Element of X =the set of
all
    R. [x,y] "/\" @r. [y,z] where y is Element of X
    proof
      deffunc g(Element of X) = R. [x,$1] "/\" @r. [$1,z];
      deffunc f(Element of X) = R. [x,$1] "/\" r. [$1,z];
      defpred P[Element of X] means not contradiction;
A1:   for y being Element of X holds f(y) = g(y) by LFUZZY_0:def 5;
      thus {f(y) where y is Element of X:P[y]} ={g(y) where y is Element of X:
      P[y]} from FRAENKEL:sch 5(A1);
    end;
    hence thesis;
  end;
  then
A2: for r being Element of FL st P[r] holds F(r) = G(r);
  thus {F(r) where r is Element of FuzzyLattice [:X,X:]: P[r] } = {G(r) where
  r is Element of FuzzyLattice [:X,X:]: P[r]} from FRAENKEL:sch 6(A2);
end;

Lm8: for R being RMembership_Func of X,X, Q being Subset of FuzzyLattice [:X,X
:], x,z being Element of X holds {"\/"((the set of all
R. [x,y] "/\" @(r). [y,z] where y is
Element of X) ,RealPoset [. 0,1 .]) where r is Element of
FuzzyLattice [:X,X:]: r in Q} = {(R(#)@r). [x,z] where r is Element of
FuzzyLattice [:X,X:]: r in Q}
proof
  let R be RMembership_Func of X,X;
  let Q be Subset of FuzzyLattice [:X,X:];
  let x,z be Element of X;
  set FL = FuzzyLattice [:X,X:];
  defpred P[Element of FL] means $1 in Q;
  deffunc F(Element of FL) = "\/"((the set of all
R. [x,y] "/\" @($1). [y,z] where y is
  Element of X),RealPoset [. 0,1 .]);
  deffunc G(Element of FL) = (R (#) @($1)). [x,z];
A1: for r being Element of FL st P[r] holds F(r) = G(r) by Lm6;
  thus {F(r) where r is Element of FuzzyLattice [:X,X:]:P[r]} = {G(r) where r
  is Element of FuzzyLattice [:X,X:]: P[r]} from FRAENKEL:sch 6(A1);
end;

Lm9: for R being RMembership_Func of X,X, Q being Subset of FuzzyLattice [:X,X
:], x,z being Element of X holds {(R(#)@r). [x,z] where r is Element of
FuzzyLattice [:X,X:]: r in Q} = pi({(R(#)@r) where r is Element of FuzzyLattice
[:X,X:]: r in Q}, [x,z])
proof
  let R be RMembership_Func of X,X;
  let Q be Subset of FuzzyLattice [:X,X:];
  let x,z be Element of X;
  set FL = FuzzyLattice [:X,X:], A= {(R(#)@r). [x,z] where r is Element of
FuzzyLattice [:X,X:]: r in Q}, B= pi({(R(#)@r) where r is Element of FL: r in Q
  }, [x,z]);
  thus A c= B
  proof
    let a be object;
    assume a in A;
    then consider r being Element of FL such that
A1: a = (R(#)@r). [x,z] and
A2: r in Q;
    (R(#)@r) in {(R(#)@r9) where r9 is Element of FL: r9 in Q} by A2;
    hence thesis by A1,CARD_3:def 6;
  end;
  thus B c= A
  proof
    let b be object;
    assume b in B;
    then consider f be Function such that
A3: f in {(R(#)@r9) where r9 is Element of FL: r9 in Q} and
A4: b = f. [x,z] by CARD_3:def 6;
    ex r being Element of FL st f = R (#) @r & r in Q by A3;
    hence thesis by A4;
  end;
end;

Lm10: for R being RMembership_Func of X,X, Q being Subset of FuzzyLattice [:X,
X:], x,z being Element of X holds "\/"((the set of all
"\/"({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),RealPoset [. 0,1 .]) = "\/"({"\/"((the set of all R. [x,y]
"/\" r9. [y,z] where y is Element of X),RealPoset [. 0,1 .])
where r9 is Element of FuzzyLattice [:X,X:]: r9 in Q},RealPoset [. 0,1 .])
proof
  let R be RMembership_Func of X,X;
  let Q be Subset of FuzzyLattice [:X,X:];
  let x,z be Element of X;
  set FL = FuzzyLattice [:X,X:], RP = RealPoset [. 0,1 .];
  defpred P[Element of X] means not contradiction;
  defpred Q[Element of FuzzyLattice [:X,X:]] means $1 in Q;
  deffunc F(Element of X,Element of FuzzyLattice [:X,X:]) = R. [x,$1] "/\" $2
  . [$1,z];
A1: for y being Element of X, r being Element of FL st P[y] & Q[r] holds F(
  y,r) = F(y,r);
  thus "\/"({ "\/"({F(y,r) where r is Element of FL: Q[r]}, RP) where y is
Element of X: P[y] }, RP) = "\/"({ "\/"({F(y9,r9) where y9 is Element of X: P[
  y9]}, RP) where r9 is Element of FL: Q[r9] }, RP) from LFUZZY_0:sch 5(A1);
end;

theorem Th34:
  for R being RMembership_Func of X,X, Q being Subset of
FuzzyLattice [:X,X:] holds R (#) @("\/"(Q,FuzzyLattice [:X,X:])) = "\/"({R (#)
  @r where r is Element of FuzzyLattice [:X,X:]:r in Q}, FuzzyLattice [:X,X:])
proof
  let R be RMembership_Func of X,X;
  let Q be Subset of FuzzyLattice [:X,X:];
  set FL = FuzzyLattice [:X,X:], RP = RealPoset [. 0,1 .];
  ("\/"({R (#) @r where r is Element of FL:r in Q},FL)) = @("\/"({R (#) @r
  where r is Element of FL:r in Q},FL)) by LFUZZY_0:def 5;
  then reconsider F = ("\/"({R (#) @r where r is Element of FL:r in Q},FL)) as
  RMembership_Func of X,X;
  for x,z being Element of X holds (R (#) @("\/"(Q,FL))).(x,z) = F.(x,z)
  proof
    let x,z be Element of X;
A1: {(R(#)@r) where r is Element of FL: r in Q} c= the carrier of
    FuzzyLattice [:X,X:]
    proof
      let t be object;
      assume t in {(R(#)@r) where r is Element of FL: r in Q};
      then consider r being Element of FuzzyLattice [:X,X:] such that
A2:   t = (R(#)@r) and
      r in Q;
      ([:X,X:],(R(#)@r))@ = (R(#)@r) by LFUZZY_0:def 6;
      hence thesis by A2;
    end;
    thus (R (#) @("\/"(Q,FL))).(x,z) = "\/"((the set of all
R.(x,y) "/\" (@("\/"(Q,FL))) . (y
    ,z) where y is Element of X),RP) by LFUZZY_0:22
      .= "\/"((the set of all
R. [x,y] "/\" "\/"(pi(Q, [y,z]), RP) where y is Element of X),RP) by Lm2
      .= "\/"((the set of all
"\/"({R. [x,y] "/\" b where b is Element of RP:b in pi(Q,[y,
    z])} ,RP) where y is Element of X),RP) by Lm3
      .= "\/"((the set of all
"\/"({R. [x,y] "/\" r. [y,z] where r is Element of FL: r in
    Q} ,RP) where y is Element of X),RP) by Lm4
      .= "\/"( {"\/"((the set of all R. [x,y] "/\" r. [y,z]
      where y is Element of X)
,RP) where r is Element of FL: r in Q},RP) by Lm10
      .= "\/"( {"\/"((the set of all R. [x,y] "/\" @r. [y,z]
      where y is Element of X)
      ,RP) where r is Element of FL: r in Q},RP) by Lm7
      .= "\/"({(R(#)@r). [x,z] where r is Element of FL: r in Q},RP) by Lm8
      .= "\/"(pi({(R(#)@r) where r is Element of FL: r in Q}, [x,z]),RP) by Lm9
      .= F.(x,z) by A1,Th32;
  end;
  hence thesis by Th2;
end;

theorem Th35:
  for R being RMembership_Func of X,X, Q being Subset of
FuzzyLattice [:X,X:] holds @("\/"(Q,FuzzyLattice [:X,X:])) (#) R = "\/"({@r (#)
  R where r is Element of FuzzyLattice [:X,X:]:r in Q}, FuzzyLattice [:X,X:])
proof
  let R be RMembership_Func of X,X;
  let Q be Subset of FuzzyLattice [:X,X:];
  set FL = FuzzyLattice [:X,X:], RP = RealPoset [. 0,1 .];
  ("\/"({@r (#) R where r is Element of FL:r in Q},FL)) = @("\/"({@r (#) R
  where r is Element of FL:r in Q},FL)) by LFUZZY_0:def 5;
  then reconsider F = ("\/"({@r (#) R where r is Element of FL:r in Q},FL)) as
  RMembership_Func of X,X;
  for x,z being Element of X holds (@("\/"(Q,FL)) (#) R).(x,z) = F.(x,z)
  proof
    let x,z be Element of X;
A1: {(@r(#)R) where r is Element of FL: r in Q} c= the carrier of
    FuzzyLattice [:X,X:]
    proof
      let t be object;
      assume t in {(@r(#)R) where r is Element of FL: r in Q};
      then consider r being Element of FuzzyLattice [:X,X:] such that
A2:   t = (@r(#)R) and
      r in Q;
      ([:X,X:],(@r(#)R))@ = (@r(#)R) by LFUZZY_0:def 6;
      hence thesis by A2;
    end;
A3: the set of all "\/"(pi(Q, [x,y]), RP) "/\" R. [y,z] where y is Element of X
 = the set of all "\/"({b "/\" R. [y9,z] where b is Element of RP:b in pi(Q,[x,
    y9])} ,RP) where y9 is Element of X
    proof
      deffunc G(Element of X) = "\/"({b "/\" R. [$1,z] where b is Element of
RP:   b in pi(Q,[x,$1])} ,RP);
      deffunc F(Element of X) = "\/"(pi(Q, [x,$1]),RP) "/\" R. [$1,z];
      defpred P[Element of X] means not contradiction;
      for y being Element of X holds "\/"(pi(Q, [x,y]), RealPoset [. 0,1
.]) "/\" R. [y,z] = "\/"({b "/\" R. [y,z] where b is Element of RP:b in pi(Q,[x
      ,y])} ,RP)
      proof
        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 as Subset of product ([:X,X:] --> RealPoset [. 0,1 .]);
        let y be Element of X;
        pi(Q, [x,y]) is Subset of RealPoset [. 0,1 .] by FUNCOP_1:7;
        hence thesis by LFUZZY_0:15;
      end;
      then
A4:   for y being Element of X holds F(y) = G (y);
      {F(y) where y is Element of X:P[y]} = {G(y9) where y9 is Element of
X:    P[y9]} from FRAENKEL:sch 5(A4);
      hence thesis;
    end;
A5: the set of all
"\/"({b "/\" R. [y,z] where b is Element of RP:b in pi(Q,[x,y])} ,RP
) where y is Element of X = the set of all "\/"({r. [x,y9] "/\" R. [y9,z]
    where r is Element of FL: r in Q} ,RP) where y9 is Element of X
    proof
      deffunc G(Element of X) = "\/"({r. [x,$1] "/\" R. [$1,z] where r is
      Element of FL: r in Q} ,RP);
      deffunc F(Element of X) = "\/"({b "/\" R. [$1,z] where b is Element of
RP:   b in pi(Q,[x,$1])} ,RP);
      defpred P[Element of X] means not contradiction;
      for y being Element of X holds "\/"({b "/\" R. [y,z] where b is
Element of RP: b in pi(Q,[x,y])} ,RP) = "\/"({r. [x,y] "/\" R. [y,z] where r is
      Element of FL: r in Q} ,RP)
      proof
        let y be Element of X;
        set A = {b "/\" R. [y,z] where b is Element of RP: b in pi(Q,[x,y])},
        B = {r. [x,y] "/\" R. [y,z] where r is Element of FL: r in Q};
A6:     B c= A
        proof
          let a be object;
          assume a in B;
          then consider r being Element of FL 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 thesis by A7;
        end;
        A c= B
        proof
          let a be object;
          assume a in A;
          then consider b be Element of RP such that
A9:       a = b "/\" R. [y,z] and
A10:      b in pi(Q,[x,y]);
          ex f be Function st f in Q & b = f. [x,y] by A10,CARD_3:def 6;
          hence thesis by A9;
        end;
        hence thesis by A6,XBOOLE_0:def 10;
      end;
      then
A11:  for y being Element of X holds F(y) = G (y);
      thus {F(y) where y is Element of X:P[y]} = {G(y) where y is Element of X
      :P[y]} from FRAENKEL:sch 5(A11);
    end;
A12: "\/"((the set of all "\/"({r. [x,y] "/\" R. [y,z]
     where r is Element of FL: r in Q}
    ,RP) where y is Element of X),RP) = "\/"({"\/"((the set of all r9. [x,y]
    "/\" R. [y,z] where y is Element of X),RP) where r9 is
    Element of FL: r9 in Q},RP)
    proof
      deffunc F(Element of X,Element of FuzzyLattice [:X,X:]) = $2. [x,$1]
      "/\" R. [$1,z];
      defpred Q[Element of FuzzyLattice [:X,X:]] means $1 in Q;
      defpred P[Element of X] means not contradiction;
A13:  for y being Element of X, r being Element of FL st P[y] & Q[r]
      holds F(y,r) = F(y,r);
      thus "\/"({ "\/"({F(y,r) where r is Element of FL: Q[r]}, RP) where y
is Element of X: P[y] }, RP) = "\/"({ "\/"({F(y9,r9) where y9 is Element of X:
P[y9]}, RP) where r9 is Element of FL: Q[r9] }, RP) from LFUZZY_0:sch 5(A13);
    end;
A14: {"\/"((the set of all r. [x,y] "/\" R. [y,z] where y is Element of X),RP)
     where r is Element of FL: r in Q} = {"\/"((the set of all @r9. [x,y] "/\"
R. [y,z] where y is Element of X) ,RP) where r9 is Element of
FL: r9 in Q}
    proof
      deffunc G(Element of FL) = "\/"((the set of all
      @($1). [x,y] "/\" R. [y,z] where y is
      Element of X),RealPoset [. 0,1 .]);
      deffunc F(Element of FL) = "\/"((the set of all
      $1. [x,y] "/\" R. [y,z] where y is
      Element of X),RealPoset [. 0,1 .]);
      defpred P[Element of FL] means $1 in Q;
      for r being Element of FL st r in Q holds "\/"((the set of all
      r. [x,y] "/\" R. [y
,z] where y is Element of X) ,RealPoset [. 0,1 .]) = "\/"((the set of all @r
. [x,y] "/\" R. [y,z] where y is Element of X) ,RealPoset [.
      0,1 .])
      proof
        let r be Element of FL;
        assume r in Q;
        the set of all r. [x,y] "/\" R. [y,z] where y is Element of X =the set
of all @r. [x,y] "/\" R. [y,z] where y is Element of X
        proof
          deffunc g(Element of X) = @r. [x,$1] "/\" R. [$1,z];
          deffunc f(Element of X) = r. [x,$1] "/\" R. [$1,z];
          defpred P[Element of X] means not contradiction;
A15:      for y being Element of X holds f(y) = g(y) by LFUZZY_0:def 5;
          thus {f(y) where y is Element of X:P[y]} ={g(y) where y is Element
          of X:P[y]} from FRAENKEL:sch 5(A15);
        end;
        hence thesis;
      end;
      then
A16:  for r being Element of FL st P[r] holds F(r) = G(r);
      thus {F(r) where r is Element of FuzzyLattice [:X,X:]: P[r] } = {G(r)
where r is Element of FuzzyLattice [:X,X:]: P[r]} from FRAENKEL:sch 6(A16);
    end;
A17: {(@r(#)R). [x,z] where r is Element of FL: r in Q} = pi({(@r(#)R)
    where r is Element of FL: r in Q}, [x,z])
    proof
      set A= {(@r(#)R). [x,z] where r is Element of FL: r in Q}, B= pi({(@r(#)
      R) where r is Element of FL: r in Q}, [x,z]);
      thus A c= B
      proof
        let a be object;
        assume a in A;
        then consider r being Element of FL such that
A18:    a = (@r(#)R). [x,z] and
A19:    r in Q;
        (@r(#)R) in {(@r9(#)R) where r9 is Element of FL: r9 in Q} by A19;
        hence thesis by A18,CARD_3:def 6;
      end;
      thus B c= A
      proof
        let b be object;
        assume b in B;
        then consider f be Function such that
A20:    f in {(@r9(#)R) where r9 is Element of FL: r9 in Q} and
A21:    b = f. [x,z] by CARD_3:def 6;
        ex r being Element of FL st f = (@r(#)R) & r in Q by A20;
        hence thesis by A21;
      end;
    end;
A22: the set of all
(@("\/"(Q,FL))). [x,y] "/\" R. [y,z] where y is Element of X = the set of all
"\/"(pi(Q, [x,y]), RP) "/\" R. [y,z] where y is Element of X
    proof
      deffunc G(Element of X) = "\/"(pi(Q, [x,$1]), RP) "/\" R. [$1,z];
      deffunc F(Element of X) = (@("\/"(Q,FL))). [x,$1] "/\" R. [$1,z];
      defpred P[Element of X] means not contradiction;
      for y being Element of X holds (@("\/"(Q,FuzzyLattice [:X,X:]))). [x
      ,y] "/\" R. [y,z] = "\/"(pi(Q, [x,y]), RealPoset [. 0,1 .]) "/\" R. [y,z]
      proof
        let y be Element of X;
        (@("\/"(Q,FuzzyLattice [:X,X:]))). [x,y] = (("\/"(Q,FuzzyLattice
        [:X,X:]))). [x,y] by LFUZZY_0:def 5
          .= "\/"(pi(Q, [x,y]), RealPoset [. 0,1 .]) by Th32;
        hence thesis;
      end;
      then
A23:  for y being Element of X holds F(y) = G(y);
      thus {F(y) where y is Element of X: P[y]} = {G(y9) where y9 is Element
      of X: P[y9]} from FRAENKEL:sch 5 (A23);
    end;
A24: {"\/"((the set of all @r. [x,y] "/\" R. [y,z] where y is Element of X),RP)
     where r is Element of FL: r in Q} = {(@r9(#)R). [x,z] where
    r9 is Element of FL: r9 in Q}
    proof
      deffunc G(Element of FL) = (@($1)(#)R). [x,z];
      deffunc F(Element of FL) = "\/"((the set of all @($1). [x,y] "/\"
      R. [y,z] where y is Element of X),RealPoset [. 0,1 .]);
      defpred P[Element of FL] means $1 in Q;
A25:  for r being Element of FL st P[r] holds F(r) = G(r) by Lm6;
      thus {F(r) where r is Element of FuzzyLattice [:X,X:]:P[r]} = {G(r)
where r is Element of FuzzyLattice [:X,X:]: P[r]} from FRAENKEL:sch 6(A25);
    end;
    thus (@("\/"(Q,FL)) (#) R).(x,z) = "\/"((the set of all
    (@("\/"(Q,FL))). [x,y] "/\" R. [y
    ,z] where y is Element of X),RP) by Lm6
      .= F.(x,z) by A1,A22,A3,A5,A12,A14,A24,A17,Th32;
  end;
  hence thesis by Th2;
end;

theorem Th36:
  for R being RMembership_Func of X,X holds (TrCl R)(#)(TrCl R) =
"\/"({(i iter R) (#) (j iter R) where i is Element of NAT, j is Element of NAT:
  i > 0 & j > 0},FuzzyLattice [:X,X:])
proof
  let R be RMembership_Func of X,X;
  set Q = {n iter R where n is Element of NAT : n > 0}, FL = FuzzyLattice [:X,
  X:];
A1: Q c= the carrier of FL
  proof
    let q be object;
    assume q in Q;
    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 thesis by A2;
  end;
A3: {"\/"({@r (#) @s where s is Element of FL : s in Q},FL) where r is
Element of FL : r in Q} = {"\/"({([:X,X:],@r9 (#) @s9)@ where s9 is Element of
FL: s9 in Q},FL) where r9 is Element of FL : r9 in Q}
  proof
    deffunc G(Element of FL) = "\/"({([:X,X:],@$1 (#) @s)@ where s is Element
    of FL : s in Q},FL);
    deffunc F(Element of FL) = "\/"({@$1 (#) @s where s is Element of FL : s
    in Q},FL);
    defpred P[Element of FL] means $1 in Q;
    for r being Element of FL holds "\/"({@r (#) @s where s is Element of
FL: s in Q},FL) = "\/"({([:X,X:],@r (#) @s)@ where s is Element of FL : s in Q
    },FL)
    proof
      let r be Element of FL;
      {@r (#) @s where s is Element of FL : s in Q} = {([:X,X:],@r (#) @s
      )@ where s is Element of FL : s in Q}
      proof
        deffunc g(Element of FL) = ([:X,X:],@r (#) @$1)@;
        deffunc f(Element of FL) = @r (#) @$1;
        defpred P[Element of FL] means $1 in Q;
A4:     for s being Element of FL holds f(s) = g(s) by LFUZZY_0:def 6;
        {f(s) where s is Element of FL : P[s]} = {g(s) where s is Element
        of FL : P[s]} from FRAENKEL:sch 5 (A4);
        hence thesis;
      end;
      hence thesis;
    end;
    then
A5: for r being Element of FL holds F(r) = G(r);
    {F(r) where r is Element of FL : P[r]} = {G(r) where r is Element of
FL: P[r]} from FRAENKEL:sch 5 (A5);
    hence thesis;
  end;
  defpred R[Element of FL] means $1 in Q;
  defpred P[Element of FL] means $1 in Q;
  deffunc f(Element of FL,Element of FL) = ([:X,X:],@$1 (#) @$2)@;
A6: {@r (#) @s where r is Element of FL,s is Element of FL:r in Q & s in Q}
= {(i iter R) (#) (j iter R) where i is Element of NAT, j is Element of NAT:i >
  0 & j > 0}
  proof
    set A = {@r (#) @s where r is Element of FL,s is Element of FL:r in Q & s
in Q}, B = {(i iter R) (#) (j iter R) where i is Element of NAT, j is Element
    of NAT:i > 0 & j > 0};
    thus A c= B
    proof
      let a be object;
      assume a in A;
      then consider r,s being Element of FL such that
A7:   a = @r (#) @s and
A8:   r in Q & s in Q;
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 thesis by A7,A9;
    end;
    thus B c= A
    proof
      let b be object;
      assume b in B;
      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 FL;
      (i iter R) = ([:X,X:],(i iter R))@ by LFUZZY_0:def 6;
      then reconsider r = i iter R as Element of FL;
A12:  @r = r & @s = s by LFUZZY_0:def 5;
      (i iter R) in Q & (j iter R) in Q by A11;
      hence thesis by A10,A12;
    end;
  end;
A13: {([:X,X:],@r (#) @s)@ where r is Element of FL, s is Element of FL:r in
Q & s in Q} = {@r (#) @s where r is Element of FL, s is Element of FL:r in Q &
  s in Q}
  proof
    deffunc G(Element of FL,Element of FL) = @$1 (#) @$2;
    deffunc F(Element of FL,Element of FL) = ([:X,X:],@$1 (#) @$2)@;
    defpred P[Element of FL,Element of FL] means $1 in Q & $2 in Q;
A14: for r being Element of FL, s being Element of FL holds F(r,s) = G(r,s
    ) by LFUZZY_0:def 6;
    {F(r,s) where r is Element of FL,s is Element of FL:P[r,s]} ={G(r,s)
where r is Element of FL,s is Element of FL:P[r,s]} from FRAENKEL:sch 7(A14);
    hence thesis;
  end;
A15: "\/"(Q,FL) = @"\/"(Q,FL) by LFUZZY_0:def 5;
  {@r (#) (TrCl R) where r is Element of FL:r in Q} = {"\/"({@r9 (#) @s
  where s is Element of FL:s in Q},FL) where r9 is Element of FL : r9 in Q}
  proof
    set A = {@r (#) (TrCl R) where r is Element of FL:r in Q}, B = {"\/"({@r9
(#) @s where s is Element of FL:s in Q},FL) where r9 is Element of FL : r9 in Q
    };
    thus A c= B
    proof
      let a be object;
      assume a in A;
      then consider r being Element of FL such that
A16:  a = @r (#) (TrCl R) and
A17:  r in Q;
      a = "\/"({@r (#) @s where s is Element of FL:s in Q},FL) by A15,A1,A16
,Th34;
      hence thesis by A17;
    end;
    thus B c= A
    proof
      let a be object;
      assume a in B;
      then consider r being Element of FL such that
A18:  a = "\/"({@r (#) @s where s is Element of FL:s in Q},FL) and
A19:  r in Q;
      a = @r (#) (TrCl R) by A15,A1,A18,Th34;
      hence thesis by A19;
    end;
  end;
  hence
  (TrCl R)(#)(TrCl R) = "\/"({"\/"({f(r,s) where s is Element of FL:R[s]}
  ,FL) where r is Element of FL :P[r]},FL) by A15,A1,A3,Th35
    .= "\/"({f(r,s) where r is Element of FL, s is Element of FL: P[r] & R[s
  ]},FL) from LFUZZY_0:sch 1
    .= "\/"({(i iter R) (#) (j iter R) where i is Element of NAT, j is
  Element of NAT: i > 0 & j > 0},FL) by A6,A13;
end;

registration
  let X be non empty set;
  let R be RMembership_Func of X,X;
  cluster TrCl R -> transitive;
  coherence
  proof
    set FL = FuzzyLattice [:X,X:], RP = RealPoset [. 0,1 .], A = {(i iter R)
(#) (j iter R) where i is Element of NAT, 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:];
A1:   A c= the carrier of FuzzyLattice [:X,X:]
      proof
        let t be object;
        assume t in A;
        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 thesis by A2;
      end;
      for b being Element of RP st b in pi(A,c) holds b <<= (TrCl R) . c
      proof
        let b be Element of RP;
        assume b in pi(A,c);
        then consider f be Function such that
A3:     f in A 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 as RMembership_Func of X,X by A5;
        f c= TrCl R by A6,A7,Th31;
        then f.c <= (TrCl R).c;
        hence thesis by A4,LFUZZY_0:3;
      end;
      then (TrCl R).c is_>=_than pi(A,c) by LATTICE3:def 9;
      then
A8:   "\/"(pi(A,c),RP) <<= (TrCl R).c by YELLOW_0:32;
      ((TrCl R)(#)(TrCl R)).c = "\/"(A,FL).c by Th36
        .= "\/"(pi(A,c),RP) by A1,Th32;
      hence thesis by A8,LFUZZY_0:3;
    end;
    then (TrCl R)(#)(TrCl R) c= (TrCl R);
    hence thesis;
  end;
end;

theorem Th37:
  for R being RMembership_Func of X,X, n being Nat st R
  is transitive & n > 0 holds n iter R c= R
proof
  let R be RMembership_Func of X,X;
  let n be Nat;
  assume that
A1: R is transitive and
A2: n > 0;
  reconsider n as non zero Element of NAT by A2,ORDINAL1:def 12;
  defpred P[Nat] means $1 iter R c= R;
A3: R (#) R c= R by A1;
A4: for k being non zero Nat st P[k] holds P[k+1]
  proof
    let k be non zero Nat;
    assume P[k];
    then k iter R (#) R c= R(#)R by Th6;
    then (k+1) iter R c= R(#)R by Th26;
    hence thesis by A3,Th5;
  end;
A5: P[1] by Th25;
  for k being non zero Nat holds P[k] from NAT_1:sch 10(A5,A4);
  then P[n];
  hence thesis;
end;

theorem Th38:
  for R being RMembership_Func of X,X st R is transitive holds R = TrCl R
proof
  let R be RMembership_Func of X,X;
  assume
A1: R is transitive;
  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}, RP = RealPoset [. 0,
    1 .];
    let c be Element of [:X,X:];
    for b being Element of RP st b in pi(Q,c) holds b <<= R.c
    proof
      let b be Element of RP;
      assume b in pi(Q,c);
      then consider f being Function such that
A2:   f in Q and
A3:   b = f.c by CARD_3:def 6;
      consider n be Element of NAT such that
A4:   f = n iter R and
A5:   n>0 by A2;
      n iter R c= R by A1,A5,Th37;
      then (n iter R).c <= R.c;
      hence thesis by A3,A4,LFUZZY_0:3;
    end;
    then
A6: R.c is_>=_than pi(Q,c) by LATTICE3:def 9;
    Q c= the carrier of FuzzyLattice [:X,X:]
    proof
      let t be object;
      assume t in Q;
      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 thesis by A7;
    end;
    then (TrCl R).c = "\/"(pi(Q,c),RP) by Th32;
    then (TrCl R).c <<= R.c by A6,YELLOW_0:32;
    hence thesis by LFUZZY_0:3;
  end;
  then
A8: TrCl R c= R;
  R c= TrCl R by Th30;
  hence thesis by A8,Th3;
end;

theorem Th39:
  for R,S being RMembership_Func of X,X, n being Nat st
  R c= S holds n iter R c= n iter S
proof
  let R,S be RMembership_Func of X,X;
  let n be Nat;
  defpred P[Nat] means $1 iter R c= $1 iter S;
  assume
A1: R c= S;
A2: for k being Nat st P[k] holds P[k+1]
  proof
    let k be Nat;
    assume
A3: P[k];
    (k iter R) (#) R = (k+1) iter R & (k iter S) (#) S = (k+1) iter S by Th26;
    hence thesis by A1,A3,Th6;
  end;
  0 iter R = Imf(X,X) by Th24
    .= 0 iter S by Th24;
  then
A4: P[0];
  for k being Nat holds P[k] from NAT_1:sch 2(A4,A2);
  hence thesis;
end;

theorem
  for R,S being RMembership_Func of X,X st S is transitive & R c= S
  holds TrCl R c= S
proof
  let R,S be RMembership_Func of X,X;
  assume that
A1: S is transitive and
A2: R c= S;
  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}, RP = RealPoset [. 0,
    1 .];
    let c be Element of [:X,X:];
    for b being Element of RP st b in pi(Q,c) holds b <<= (TrCl S).c
    proof
      let b be Element of RP;
      assume b in pi(Q,c);
      then consider f being Function such that
A3:   f in Q and
A4:   b = f.c by CARD_3:def 6;
      consider n be Element of NAT such that
A5:   f = n iter R and
A6:   n>0 by A3;
A7:   n iter S c= TrCl S by A6,Th31;
      n iter R c= n iter S by A2,Th39;
      then n iter R c= TrCl S by A7,Th5;
      then (n iter R).c <= (TrCl S).c;
      hence thesis by A4,A5,LFUZZY_0:3;
    end;
    then (TrCl S).c is_>=_than pi(Q,c) by LATTICE3:def 9;
    then
A8: "\/"(pi(Q,c),RP) <<= (TrCl S).c by YELLOW_0:32;
    Q c= the carrier of FuzzyLattice [:X,X:]
    proof
      let t be object;
      assume t in Q;
      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 thesis by A9;
    end;
    then (TrCl R).c = "\/"(pi(Q,c),RP) by Th32;
    hence thesis by A8,LFUZZY_0:3;
  end;
  then TrCl R c= TrCl S;
  hence thesis by A1,Th38;
end;

subset_name: curated