:: Properties of Fuzzy Relation
::  by Noboru Endou , Takashi Mitsuishi and Keiji Ohkubo
::
:: Received June 25, 2001
:: Copyright (c) 2001-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, XBOOLE_0, FUZZY_1, RELAT_1, SUBSET_1, FUNCT_1, XXREAL_2,
      XXREAL_0, XXREAL_1, CARD_1, TARSKI, XREAL_0, ORDINAL1, ARYTM_3, ARYTM_1,
      FUZZY_2, ZFMISC_1, PARTFUN1, VALUED_1, SEQ_4, FUZZY_4, MEASURE5;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
      XXREAL_0, XREAL_0, SQUARE_1, BINOP_1, RELAT_1, RELSET_1, PARTFUN1,
      XXREAL_2, FUNCT_4, SEQ_1, INTEGRA1, RCOMP_1, MEASURE6, FUZZY_1, FUZZY_2,
      SEQ_4, MEASURE5;
 constructors FUNCT_4, REAL_1, SQUARE_1, RFUNCT_1, MEASURE6, INTEGRA1, FUZZY_2,
      SEQ_1, XXREAL_2, SEQ_4, RELSET_1, RELAT_1, FUZZY_1, BINOP_2, RVSUM_1,
      BINOP_1;
 registrations XBOOLE_0, SUBSET_1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED,
      INTEGRA1, RELAT_1, VALUED_0, RELSET_1, MEASURE5;
 requirements NUMERALS, REAL, SUBSET, BOOLE;
 definitions TARSKI, FUZZY_1, FUZZY_2, BINOP_1, RELAT_1;
 theorems FUZZY_1, FUNCT_3, PARTFUN1, FUNCT_1, INTEGRA1, INTEGRA2, ZFMISC_1,
      SEQ_4, SUBSET_1, XBOOLE_0, FUZZY_2, XXREAL_0, FUNCT_4, XXREAL_2, XREAL_1,
      RELSET_1, MEMBERED, FUNCT_2, RELAT_1, MEASURE5;
 schemes PARTFUN1, BINOP_1;

begin :: Basic properties of the membership function

reserve c,c1,c2,x,y,z,z1,z2 for set;
reserve C1,C2,C3 for non empty set;

registration
  let C1 be non empty set;
  let F be Membership_Func of C1;
  cluster rng F -> non empty;
  coherence
  proof
    dom F = C1 by FUNCT_2:def 1;
    then consider y being Element of C1 such that
A1: y in dom F by SUBSET_1:4;
    F.y in rng F by A1,FUNCT_1:def 3;
    hence thesis;
  end;
end;

theorem Th1:
  for F be Membership_Func of C1 holds rng F is real-bounded & (for x st
x in dom F holds F.x <= upper_bound rng F) & for x st x in dom F
holds F.x >= lower_bound rng F
proof
  let F be Membership_Func of C1;
A1: [.0,1.] is non empty closed_interval Subset of REAL by MEASURE5:14;
A2: rng F c= [.0,1.] by RELAT_1:def 19;
  then
A3: rng F is real-bounded by A1,XXREAL_2:45;
A4: for x st x in dom F holds F.x >= lower_bound rng F
  proof
    let x;
    assume x in dom F;
    then
A5: F.x in rng F by FUNCT_1:def 3;
    rng F is bounded_below by A3,XXREAL_2:def 11;
    hence thesis by A5,SEQ_4:def 2;
  end;
  for x st x in dom F holds F.x <= upper_bound rng F
  proof
    let x;
    assume x in dom F;
    then
A6: F.x in rng F by FUNCT_1:def 3;
    rng F is bounded_above by A3,XXREAL_2:def 11;
    hence thesis by A6,SEQ_4:def 1;
  end;
  hence thesis by A2,A1,A4,XXREAL_2:45;
end;

theorem
  for F,G be Membership_Func of C1 holds (for x st x in C1 holds F.x <=
  G.x) implies upper_bound rng F <= upper_bound rng G
proof
  let F,G be Membership_Func of C1;
  rng F is real-bounded by Th1;
  then
A1: rng F is bounded_above by XXREAL_2:def 11;
  assume
A2: for c st c in C1 holds F.c <= G.c;
A3: for s being real number st 0<s ex y st y in dom F &
upper_bound rng F - s <= G.y
  proof
    let s being real number;
    assume 0<s;
    then consider r being real number such that
A4: r in rng F and
A5: upper_bound rng F-s<r by A1,SEQ_4:def 1;
    consider y being set such that
A6: y in dom F and
A7: r = F.y by A4,FUNCT_1:def 3;
    r <= G.y by A2,A6,A7;
    hence thesis by A5,A6,XXREAL_0:2;
  end;
  for s being real number st 0<s
  holds upper_bound rng F - s <= upper_bound rng G
  proof
    let s being real number;
    assume 0<s;
    then consider y such that
A8: y in dom F and
A9: upper_bound rng F - s <= G.y by A3;
    y in C1 by A8;
    then y in dom G by FUNCT_2:def 1;
    then G.y <= upper_bound rng G by Th1;
    hence thesis by A9,XXREAL_0:2;
  end;
  hence thesis by XREAL_1:57;
end;

theorem Th3:
  for f be RMembership_Func of C1,C2, c be set holds 0 <= f.c & f.c <= 1
proof
  let f being RMembership_Func of C1,C2;
  let c be set;
  per cases;
  suppose
    c in [:C1,C2:];
    then reconsider c as Element of [:C1,C2:];
A1: f.c <= (Umf(C1,C2)).c by FUZZY_2:52;
    (Zmf(C1,C2)).c <= f.c by FUZZY_2:52;
    hence thesis by A1,FUNCT_3:def 3;
  end;
  suppose
A2: not c in [:C1,C2:];
    dom f = [:C1,C2:] by FUNCT_2:def 1;
    hence thesis by A2,FUNCT_1:def 2;
  end;
end;

definition
  let C1,C2;
  let f be RMembership_Func of C1,C2;
  let x,y;
  redefine func f.(x,y) -> Element of REAL;
  coherence
  proof
    f.(x,y) = f. [x,y];
    hence thesis;
  end;
end;

theorem
  for f be RMembership_Func of C1,C2, x,y holds 0 <= f.(x,y) & f.(x,y)
  <= 1 by Th3;

begin

:: Definition and properties of converse fuzzy relation

notation
  let C1,C2 be non empty set;
  let h be RMembership_Func of C2,C1;
  synonym converse h for ~h;
end;

definition
  let C1,C2 be non empty set;
  let h be RMembership_Func of C2,C1;
  redefine func converse h -> RMembership_Func of C1,C2 means
  :Def1:
  for x,y st [x,y] in [:C1,C2:] holds it.(x,y) = h.(y,x);
  coherence
  proof
    set IT = converse h;
A1: dom h = [:C2,C1:] by FUNCT_2:def 1;
    then
A2: dom IT = [:C1,C2:] by FUNCT_4:46;
    rng h c= [.0,1.] by RELAT_1:def 19;
    then
A3: rng IT c= [.0,1.] by A1,FUNCT_4:47;
    then rng IT c= REAL by MEMBERED:3;
    then reconsider IT as PartFunc of [:C1,C2:],REAL by A2,RELSET_1:4;
    IT is Membership_Func of [:C1,C2:] by A2,A3,FUNCT_2:def 1,RELAT_1:def 19;
    hence thesis;
  end;
  compatibility
  proof
    let IT be RMembership_Func of C1,C2;
A4: dom h = [:C2,C1:] by FUNCT_2:def 1;
    thus IT = ~h implies for x,y st [x,y] in [:C1,C2:] holds IT.(x,y) = h.(y,x
    )
    proof
      assume
A5:   IT = ~h;
      let x,y;
      assume [x,y] in [:C1,C2:];
      then [y,x] in dom h by A4,ZFMISC_1:88;
      hence thesis by A5,FUNCT_4:def 2;
    end;
A6: dom IT = [:C1,C2:] by FUNCT_2:def 1;
A7: for x holds x in dom IT iff ex y,z st x = [z,y] & [y,z] in dom h
    proof
      let x;
      thus x in dom IT implies ex y,z st x = [z,y] & [y,z] in dom h
      proof
        assume x in dom IT;
        then consider z,y such that
A8:     z in C1 and
A9:     y in C2 and
A10:    x = [z,y] by ZFMISC_1:def 2;
        take y,z;
        thus thesis by A4,A8,A9,A10,ZFMISC_1:def 2;
      end;
      thus thesis by A6,ZFMISC_1:88;
    end;
    assume for x,y st [x,y] in [:C1,C2:] holds IT.(x,y) = h.(y,x);
    then for y,z st [y,z] in dom h holds IT.(z,y) = h.(y,z) by ZFMISC_1:88;
    hence thesis by A7,FUNCT_4:def 2;
  end;
end;

theorem
  for f be RMembership_Func of C1,C2 holds converse converse f = f
proof
  let f being RMembership_Func of C1,C2;
A1: dom f = [:C1,C2:] by FUNCT_2:def 1;
A2: for c being Element of [:C1,C2:] st c in [:C1,C2:] holds (converse
  converse f).c = f.c
  proof
    let c being Element of [:C1,C2:];
    assume c in [:C1,C2:];
    consider x,y being set such that
A3: x in C1 and
A4: y in C2 and
A5: c = [x,y] by ZFMISC_1:def 2;
A6: [y,x] in [:C2,C1:] by A3,A4,ZFMISC_1:87;
    (converse converse f).(x,y) = (converse f).(y,x) by A5,Def1
      .= f.(x,y) by A6,Def1;
    hence thesis by A5;
  end;
  dom(converse converse f) = [:C1,C2:] by FUNCT_2:def 1;
  hence thesis by A2,A1,PARTFUN1:5;
end;

theorem Th6:
  for f be RMembership_Func of C1,C2 holds 1_minus(converse f) =
  converse(1_minus f)
proof
  let f being RMembership_Func of C1,C2;
A1: [:C2,C1:] = dom converse(1_minus f ) by FUNCT_2:def 1;
A2: for c being Element of [:C2,C1:] st c in [:C2,C1:] holds (1_minus(
  converse f)).c = (converse(1_minus f)).c
  proof
    let c being Element of [:C2,C1:];
    assume c in [:C2,C1:];
    consider y,x being set such that
A3: y in C2 and
A4: x in C1 and
A5: c = [y,x] by ZFMISC_1:def 2;
A6: [x,y] in [:C1,C2:] by A3,A4,ZFMISC_1:87;
    (1_minus(converse f)).(y,x) = 1-(converse f).(y,x) by A5,FUZZY_1:def 5
      .= 1-f.(x,y) by A5,Def1
      .= (1_minus f).(x,y) by A6,FUZZY_1:def 5
      .= (converse(1_minus f)).(y,x) by A5,Def1;
    hence thesis by A5;
  end;
  dom(1_minus(converse f)) = [:C2,C1:] by FUNCT_2:def 1;
  hence thesis by A2,A1,PARTFUN1:5;
end;

theorem Th7:
  for f,g be RMembership_Func of C1,C2 holds converse max(f,g) =
  max(converse f,converse g)
proof
  let f,g be RMembership_Func of C1,C2;
A1: dom max(converse f,converse g) = [:C2,C1:] by FUNCT_2:def 1;
A2: for c being Element of [:C2,C1:] st c in [:C2,C1:] holds (converse max(f
  ,g)).c = max(converse f,converse g).c
  proof
    let c being Element of [:C2,C1:];
    assume c in [:C2,C1:];
    consider y,x such that
A3: y in C2 and
A4: x in C1 and
A5: c = [y,x] by ZFMISC_1:def 2;
A6: [x,y] in [:C1,C2:] by A3,A4,ZFMISC_1:87;
    (converse max(f,g)).(y,x) = max(f,g).(x,y) by A5,Def1
      .=max(f.(x,y),g.(x,y)) by A6,FUZZY_1:def 4
      .=max((converse f).(y,x), g.(x,y)) by A5,Def1
      .=max((converse f).(y,x),(converse g).(y,x)) by A5,Def1
      .=max(converse f,converse g).(y,x) by A5,FUZZY_1:def 4;
    hence thesis by A5;
  end;
  dom converse max(f,g) = [:C2,C1:] by FUNCT_2:def 1;
  hence thesis by A1,A2,PARTFUN1:5;
end;

theorem Th8:
  for f,g be RMembership_Func of C1,C2 holds converse min(f,g) =
  min(converse f,converse g)
proof
  let f,g be RMembership_Func of C1,C2;
A1: dom min(converse f,converse g) = [:C2,C1:] by FUNCT_2:def 1;
A2: for c being Element of [:C2,C1:] st c in [:C2,C1:] holds (converse min(f
  ,g)).c = min(converse f,converse g).c
  proof
    let c being Element of [:C2,C1:];
    assume c in [:C2,C1:];
    consider y,x such that
A3: y in C2 and
A4: x in C1 and
A5: c = [y,x] by ZFMISC_1:def 2;
A6: [x,y] in [:C1,C2:] by A3,A4,ZFMISC_1:87;
    (converse min(f,g)).(y,x) = min(f,g).(x,y) by A5,Def1
      .=min(f.(x,y),g.(x,y)) by A6,FUZZY_1:def 3
      .=min((converse f).(y,x), g.(x,y)) by A5,Def1
      .=min((converse f).(y,x),(converse g).(y,x)) by A5,Def1;
    hence thesis by A5,FUZZY_1:def 3;
  end;
  dom converse min(f,g) = [:C2,C1:] by FUNCT_2:def 1;
  hence thesis by A1,A2,PARTFUN1:5;
end;

theorem Th9:
  for f,g be RMembership_Func of C1,C2, x,y st x in C1 & y in C2
  holds f. [x,y] <= g. [x,y]
   implies (converse f). [y,x] <= (converse g). [y,x]
proof
  let f,g being RMembership_Func of C1,C2, x,y;
  assume that
A1: x in C1 and
A2: y in C2 and
A3: f. [x,y] <= g. [x,y];
A4: [y,x] in [:C2,C1:] by A1,A2,ZFMISC_1:87;
  then
A5: g.(x,y) = (converse g).(y,x) by Def1;
  f.(x,y) = (converse f).(y,x) by A4,Def1;
  hence thesis by A3,A5;
end;

theorem
  for f,g be RMembership_Func of C1,C2 holds f c= g implies converse f
  c= converse g
proof
  let f,g be RMembership_Func of C1,C2;
  assume
A1: f c= g;
  let c being Element of [:C2,C1:];
  ex y,x st y in C2 & x in C1 & c = [y,x] by ZFMISC_1:def 2;
  then consider x,y being set such that
A2: x in C1 and
A3: y in C2 and
A4: c = [y,x];
  [x,y] in [:C1,C2:] by A2,A3,ZFMISC_1:87;
  then f. [x,y] <= g. [x,y] by A1,FUZZY_1:def 2;
  hence thesis by A2,A3,A4,Th9;
end;

theorem
  for f,g be RMembership_Func of C1,C2 holds converse(f\g) = (converse f
  )\(converse g)
proof
  let f,g be RMembership_Func of C1,C2;
  converse(f\g) = min(converse f,converse 1_minus g) by Th8
    .= min(converse f,1_minus converse g) by Th6;
  hence thesis;
end;

theorem
  for f,g be RMembership_Func of C1,C2 holds converse (f \+\ g) = (
  converse f) \+\ (converse g)
proof
  let f,g be RMembership_Func of C1,C2;
  converse (f \+\ g) = max(converse min(f,1_minus g),converse min(1_minus
  f,g)) by Th7
    .= max(min(converse f,converse 1_minus g), converse min(1_minus f,g)) by
Th8
    .= max(min(converse f,converse 1_minus g), min(converse 1_minus f,
  converse g)) by Th8
    .= max(min(converse f,1_minus (converse g)), min(converse 1_minus f,
  converse g)) by Th6
    .= max(min(converse f,1_minus (converse g)), min(1_minus converse f,
  converse g)) by Th6;
  hence thesis;
end;

begin

:: Definition and properties of the composition

definition
  let C1,C2,C3 be non empty set;
  let h be RMembership_Func of C1,C2;
  let g be RMembership_Func of C2,C3;
  let x,z be set;
  assume that
A1: x in C1 and
A2: z in C3;
  func min(h,g,x,z) -> Membership_Func of C2 means
  :Def2:
  for y being Element of C2 holds it.y = min(h. [x,y],g. [y,z]);
  existence
  proof
    defpred P[set,set] means $2 = min(h. [x,$1],g. [$1,z]);
A3: for y,c1,c2 st y in C2 & P[y,c1] & P[y,c2] holds c1=c2;
A4: for y,c st y in C2 & P[y,c] holds c in REAL;
    consider IT being PartFunc of C2,REAL such that
A5: (for y holds y in dom IT iff y in C2 & ex c st P[y,c]) & for y st
    y in dom IT holds P[y,IT.y] from PARTFUN1:sch 2(A4,A3);
A6: dom IT = C2 & rng IT c= [.0,1.]
    proof
      C2 c= dom IT
      proof
        let y being set;
A7:     ex c st c = min(h. [x,y],g. [y,z]);
        assume y in C2;
        hence thesis by A5,A7;
      end;
      hence dom IT = C2 by XBOOLE_0:def 10;
      reconsider A=[.0,1.] as
       non empty closed_interval Subset of REAL by MEASURE5:14;
      let c being set;
A8:   rng h c= [.0,1.] by RELAT_1:def 19;
      assume c in rng IT;
      then consider y being Element of C2 such that
A9:   y in dom IT and
A10:  c = IT.y by PARTFUN1:3;
A11:  h. [x,y] >= min(h. [x,y],g. [y,z]) by XXREAL_0:17;
      [x,y] in [:C1,C2:] by A1,ZFMISC_1:87;
      then [x,y] in dom h by FUNCT_2:def 1;
      then
A12:  h. [x,y] in rng h by FUNCT_1:def 3;
      [y,z] in [:C2,C3:] by A2,ZFMISC_1:87;
      then [y,z] in dom g by FUNCT_2:def 1;
      then
A13:  g. [y,z] in rng g by FUNCT_1:def 3;
A14:  A = [. lower_bound A, upper_bound A .] by INTEGRA1:4;
      then
A15:  0=lower_bound A by INTEGRA1:5;
A16:  1=upper_bound A by A14,INTEGRA1:5;
      then h. [x,y] <= 1 by A8,A12,INTEGRA2:1;
      then min(h. [x,y],g. [y,z]) <= 1 by A11,XXREAL_0:2;
      then
A17:  IT.y <= 1 by A5,A9;
      rng g c= [.0,1.] by RELAT_1:def 19;
      then
A18:  0 <= g. [y,z] by A15,A13,INTEGRA2:1;
      0 <= h. [x,y] by A8,A15,A12,INTEGRA2:1;
      then 0 <= min(h. [x,y],g. [y,z]) by A18,XXREAL_0:20;
      then 0 <= IT.y by A5,A9;
      hence thesis by A10,A15,A16,A17,INTEGRA2:1;
    end;
    then
A19: IT is Membership_Func of C2 by FUNCT_2:def 1,RELAT_1:def 19;
    for y being Element of C2 holds IT.y = min(h. [x,y],g. [y,z]) by A5,A6;
    hence thesis by A19;
  end;
  uniqueness
  proof
    let F,G be Membership_Func of C2;
    assume that
A20: for y being Element of C2 holds F.y = min(h. [x,y],g. [y,z]) and
A21: for y being Element of C2 holds G.y = min(h. [x,y],g. [y,z]);
A22: for y being Element of C2 st y in C2 holds F.y = G.y
    proof
      let y being Element of C2;
      F.y = min(h. [x,y],g. [y,z]) by A20;
      hence thesis by A21;
    end;
A23: dom G = C2 by FUNCT_2:def 1;
    dom F = C2 by FUNCT_2:def 1;
    hence thesis by A23,A22,PARTFUN1:5;
  end;
end;

definition
  let C1,C2,C3 be non empty set;
  let h be RMembership_Func of C1,C2;
  let g be RMembership_Func of C2,C3;
  func h(#)g -> RMembership_Func of C1,C3 means
  :Def3:
  for x,z st [x,z] in [:
  C1,C3:] holds it.(x,z) = upper_bound(rng(min(h,g,x,z)));
  existence
  proof
    defpred P[set,set,set] means $3 = upper_bound(rng(min(h,g,$1,$2)));
A1: for x,z,c1,c2 st x in C1 & z in C3 & P[x,z,c1] & P[x,z,c2] holds c1=c2;
A2: for x,z,c st x in C1 & z in C3 & P[x,z,c] holds c in REAL;
    consider IT being PartFunc of [:C1,C3:],REAL such that
A3: (for x,z holds [x,z] in dom IT iff x in C1 & z in C3 & ex c st P[x
,z,c]) & for x,z st [x,z] in dom IT holds P[x,z,IT.(x,z)] from BINOP_1:sch 5(A2
    ,A1);
A4: [:C1,C3:] c= dom IT
    proof
      let x,z being set;
A5:   ex c st c = upper_bound(rng(min(h,g,x,z)));
      assume
A6:   [x,z] in [:C1,C3:];
      then
A7:   z in C3 by ZFMISC_1:87;
      x in C1 by A6,ZFMISC_1:87;
      hence thesis by A3,A7,A5;
    end;
    then
A8: dom IT = [:C1,C3:] by XBOOLE_0:def 10;
A9: dom IT = [:C1,C3:] by A4,XBOOLE_0:def 10;
    rng IT c= [.0,1.]
    proof
      reconsider A=[.0,1.] as
       non empty closed_interval Subset of REAL by MEASURE5:14;
      let c being set;
      assume c in rng IT;
      then consider a being Element of [:C1,C3:] such that
      a in dom IT and
A10:  c = IT.a by PARTFUN1:3;
A11:  A = [. lower_bound A, upper_bound A .] by INTEGRA1:4;
      then
A12:  0=lower_bound A by INTEGRA1:5;
A13:  0 <= upper_bound(rng(min(h,g,x,z))) & upper_bound(rng(min(h,g,x,z))) <= 1
      proof
A14:    rng(min(h,g,x,z)) c= A by RELAT_1:def 19;
        A is bounded_below by INTEGRA1:3;
        then
A15:    lower_bound A <= lower_bound(rng(min (h,g,x,z))) by A14,SEQ_4:47;
        A is bounded_above by INTEGRA1:3;
        then
A16:    upper_bound(rng(min(h,g,x,z))) <= upper_bound A by A14,SEQ_4:48;
        lower_bound(rng(min(h,g,x,z))) <= upper_bound(rng(min(h,g,x,z)))
        by Th1,SEQ_4:11;
        hence thesis by A11,A16,A15,INTEGRA1:5;
      end;
      consider x,z being set such that
      x in C1 and
      z in C3 and
A17:  a = [x,z] by ZFMISC_1:def 2;
A18:  IT.(x,z) = upper_bound(rng(min(h,g,x,z))) by A3,A9,A17;
      then
A19:  IT.a <= 1 by A13,A17;
A20:  1=upper_bound A by A11,INTEGRA1:5;
      0 <= IT.a by A13,A17,A18;
      hence thesis by A10,A12,A20,A19,INTEGRA2:1;
    end;
    then IT is RMembership_Func of C1,C3 by A8,FUNCT_2:def 1,RELAT_1:def 19;
    hence thesis by A3,A8;
  end;
  uniqueness
  proof
    let F,G be RMembership_Func of C1,C3;
    assume that
A21: for x,z st [x,z] in [:C1,C3:] holds F.(x,z) = upper_bound(rng(min(h,g,x,z
    ))) and
A22: for x,z st [x,z] in [:C1,C3:] holds G.(x,z) = upper_bound(rng(min(h,g,x,z
    )));
A23: for c being Element of [:C1,C3:] st c in [:C1,C3:] holds F.c = G.c
    proof
      let c being Element of [:C1,C3:];
      consider x,z being set such that
      x in C1 and
      z in C3 and
A24:  c = [x,z] by ZFMISC_1:def 2;
A25:  G.(x,z) = upper_bound(rng(min(h,g,x,z))) by A22,A24;
      F.(x,z) = upper_bound(rng(min(h,g,x,z))) by A21,A24;
      hence thesis by A24,A25;
    end;
A26: dom G = [:C1,C3:] by FUNCT_2:def 1;
    dom F = [:C1,C3:] by FUNCT_2:def 1;
    hence thesis by A26,A23,PARTFUN1:5;
  end;
end;

Lm1: for f be RMembership_Func of C1,C2, g,h be RMembership_Func of C2,C3, x,z
be set st x in C1 & z in C3
 holds upper_bound(rng(min(f,max(g,h),x,z))) = max(upper_bound rng(
min(f,g,x,z)),upper_bound rng(min(f,h,x,z)))
proof
  let f being RMembership_Func of C1,C2, g,h being RMembership_Func of C2,C3,x
  ,z being set;
  assume that
A1: x in C1 and
A2: z in C3;
A3: for y be Element of C2 st y in C2 holds max(min(f,g,x,z),min(f,h,x,z)).y
  =min(f,max(g,h),x,z).y
  proof
    let y being Element of C2;
    assume y in C2;
A4: [y,z] in [:C2,C3:] by A2,ZFMISC_1:87;
    max(min(f,g,x,z),min(f,h,x,z)).y =max(min(f,g,x,z).y,min(f,h,x,z).y)
    by FUZZY_1:def 4
      .=max(min(f,g,x,z).y,min(f. [x,y],h. [y,z])) by A1,A2,Def2
      .=max( min(f. [x,y],g. [y,z]),min(f. [x,y],h. [y,z]) ) by A1,A2,Def2
      .=min(f. [x,y],max(g. [y,z],h. [y,z])) by XXREAL_0:38
      .=min(f. [x,y],max(g,h). [y,z]) by A4,FUZZY_1:def 4
      .=min(f,max(g,h),x,z).y by A1,A2,Def2;
    hence thesis;
  end;
  set F = min(f,g,x,z), G = min(f,h,x,z);
A5: dom min(f,max(g,h),x,z) = C2 by FUNCT_2:def 1;
  rng max(F,G) is real-bounded by Th1;
  then
A6: rng max(F,G) is bounded_above by XXREAL_2:def 11;
A7: for s being real number st 0<s
 ex y st y in dom max(F,G) & upper_bound rng max(
  F,G) - s < max(F,G).y
  proof
    let s being real number;
    assume 0 < s;
    then consider r being real number such that
A8: r in rng max(F,G) and
A9: upper_bound rng max(F,G) - s < r by A6,SEQ_4:def 1;
    ex y being set st y in dom max(F,G) & r = max(F,G).y by A8,FUNCT_1:def 3;
    hence thesis by A9;
  end;
  for s being real number st 0<s
   holds upper_bound rng max(F,G) - s < max(upper_bound rng
  F,upper_bound rng G)
  proof
    let s being real number;
    assume 0 < s;
    then consider y such that
A10: y in dom max(F,G) and
A11: upper_bound rng max(F,G) - s < max(F,G).y by A7;
A12: max(F,G).y = max(F.y,G.y) by A10,FUZZY_1:def 4;
A13: for y st y in C2 holds F.y <= upper_bound rng F & G.y <= upper_bound rng G
    proof
      let y;
      assume
A14:  y in C2;
      then y in dom G by FUNCT_2:def 1;
      then
A15:  G.y in rng G by FUNCT_1:def 3;
      rng G is real-bounded by Th1;
      then
A16:  rng G is bounded_above by XXREAL_2:def 11;
      rng F is real-bounded by Th1;
      then
A17:  rng F is bounded_above by XXREAL_2:def 11;
      y in dom F by A14,FUNCT_2:def 1;
      then F.y in rng F by FUNCT_1:def 3;
      hence thesis by A15,A17,A16,SEQ_4:def 1;
    end;
    then
A18: G.y <= upper_bound rng G by A10;
    F.y <= upper_bound rng F by A10,A13;
    then max(F,G).y <= max(upper_bound rng F,upper_bound rng G)
    by A12,A18,XXREAL_0:26;
    hence thesis by A11,XXREAL_0:2;
  end;
  then for s being real number st 0<s
   holds upper_bound rng max(F,G) - s <= max(upper_bound
  rng F,upper_bound rng G);
  then
A19: upper_bound rng max(F,G) <= max(upper_bound rng F, upper_bound rng G)
 by XREAL_1:57;
A20: for y st y in C2 holds max(F,G).y <= upper_bound rng max(F,G)
  proof
    let y;
    assume y in C2;
    then y in dom max(F,G) by FUNCT_2:def 1;
    then
A21: max(F,G).y in rng max(F,G) by FUNCT_1:def 3;
    rng max(F,G) is real-bounded by Th1;
    then rng max(F,G) is bounded_above by XXREAL_2:def 11;
    hence thesis by A21,SEQ_4:def 1;
  end;
  rng G is real-bounded by Th1;
  then
A22: rng G is bounded_above by XXREAL_2:def 11;
A23: for s being real number st 0<s
 ex y st y in dom G & upper_bound rng G - s < G.y
  proof
    let s being real number;
    assume 0 < s;
    then consider r being real number such that
A24: r in rng G and
A25: upper_bound rng G - s < r by A22,SEQ_4:def 1;
    ex y being set st y in dom G & r = G.y by A24,FUNCT_1:def 3;
    hence thesis by A25;
  end;
  for s being real number st 0<s
   holds upper_bound rng G - s <= upper_bound rng max(F,G)
  proof
    let s being real number;
    assume 0<s;
    then consider y such that
A26: y in dom G and
A27: upper_bound rng G - s < G.y by A23;
    G.y <= max(F.y,G.y) by XXREAL_0:25;
    then G.y <= max(F,G).y by A26,FUZZY_1:def 4;
    then
A28: upper_bound rng G - s < max(F,G).y by A27,XXREAL_0:2;
    max(F,G).y <= upper_bound rng max(F,G) by A20,A26;
    hence thesis by A28,XXREAL_0:2;
  end;
  then
A29: upper_bound rng G <= upper_bound rng max(F,G) by XREAL_1:57;
  rng F is real-bounded by Th1;
  then
A30: rng F is bounded_above by XXREAL_2:def 11;
A31: for s being real number st 0<s
 ex y st y in dom F & upper_bound rng F - s < F.y
  proof
    let s being real number;
    assume 0 < s;
    then consider r being real number such that
A32: r in rng F and
A33: upper_bound rng F - s < r by A30,SEQ_4:def 1;
    ex y being set st y in dom F & r = F.y by A32,FUNCT_1:def 3;
    hence thesis by A33;
  end;
  for s being real number st 0<s
   holds upper_bound rng F - s <= upper_bound rng max(F,G)
  proof
    let s being real number;
    assume 0<s;
    then consider y such that
A34: y in dom F and
A35: upper_bound rng F - s < F.y by A31;
    F.y <= max(F.y,G.y) by XXREAL_0:25;
    then F.y <= max(F,G).y by A34,FUZZY_1:def 4;
    then
A36: upper_bound rng F - s < max(F,G).y by A35,XXREAL_0:2;
    max(F,G).y <= upper_bound rng max(F,G) by A20,A34;
    hence thesis by A36,XXREAL_0:2;
  end;
  then upper_bound rng F <= upper_bound rng max(F,G) by XREAL_1:57;
  then max(upper_bound rng F, upper_bound rng G)
   <= upper_bound rng max(F,G) by A29,XXREAL_0:28;
  then
A37: upper_bound rng max(F,G) = max(upper_bound rng F, upper_bound rng G)
by A19,XXREAL_0:1;
  dom max(min(f,g,x,z),min(f,h,x,z)) = C2 by FUNCT_2:def 1;
  hence thesis by A5,A3,A37,PARTFUN1:5;
end;

theorem
  for f be RMembership_Func of C1,C2, g,h be RMembership_Func of C2,C3
  holds f(#)(max(g,h)) = max(f(#)g,f(#)h)
proof
  let f be RMembership_Func of C1,C2,g,h be RMembership_Func of C2,C3;
A1: dom max(f(#)g,f(#)h) = [:C1,C3:] by FUNCT_2:def 1;
A2: for c being Element of [:C1,C3:] st c in [:C1,C3:] holds (f(#)(max(g,h))
  ).c = max(f(#)g,f(#)h).c
  proof
    let c being Element of [:C1,C3:];
    consider x,z being set such that
A3: x in C1 and
A4: z in C3 and
A5: c = [x,z] by ZFMISC_1:def 2;
    (f(#)(max(g,h))).c = (f(#)(max(g,h))).(x,z) by A5
      .= upper_bound(rng(min(f,max(g,h),x,z))) by A5,Def3
      .= max(upper_bound rng(min(f,g,x,z)),upper_bound rng(min(f,h,x,z)))
      by A3,A4,Lm1
      .= max((f(#)g).(x,z),upper_bound rng(min(f,h,x,z))) by A5,Def3
      .= max((f(#)g).(x,z),(f(#)h).(x,z)) by A5,Def3
      .= max(f(#)g,f(#)h).c by A5,FUZZY_1:def 4;
    hence thesis;
  end;
  dom(f(#)(max(g,h))) = [:C1,C3:] by FUNCT_2:def 1;
  hence thesis by A1,A2,PARTFUN1:5;
end;

Lm2: for f,g be RMembership_Func of C1,C2, h be RMembership_Func of C2,C3, x,z
be set st x in C1 & z in C3
 holds upper_bound(rng(min(max(f,g),h,x,z))) = max(upper_bound rng(
min(f,h,x,z)),upper_bound rng(min(g,h,x,z)))
proof
  let f,g be RMembership_Func of C1,C2, h be RMembership_Func of C2,C3, x,z be
  set;
  assume that
A1: x in C1 and
A2: z in C3;
A3: for y being Element of C2 st y in C2 holds min(max(f,g),h,x,z).y = max(
  min(f,h,x,z),min(g,h,x,z)).y
  proof
    let y being Element of C2;
    assume y in C2;
A4: [x,y] in [:C1,C2:] by A1,ZFMISC_1:87;
    min(max(f,g),h,x,z).y = min(max(f,g). [x,y],h. [y,z]) by A1,A2,Def2
      .= min(max(f. [x,y],g. [x,y]),h. [y,z]) by A4,FUZZY_1:def 4
      .= max(min(f. [x,y],h. [y,z]),min(g. [x,y],h. [y,z])) by XXREAL_0:38
      .= max(min(f. [x,y],h. [y,z]),min(g,h,x,z).y) by A1,A2,Def2
      .= max(min(f,h,x,z).y,min(g,h,x,z).y) by A1,A2,Def2;
    hence thesis by FUZZY_1:def 4;
  end;
  set F = min(f,h,x,z), G = min(g,h,x,z);
A5: dom max(min(f,h,x,z),min(g,h,x,z)) = C2 by FUNCT_2:def 1;
  rng max(F,G) is real-bounded by Th1;
  then
A6: rng max(F,G) is bounded_above by XXREAL_2:def 11;
A7: for y st y in dom max(F,G) holds max(F,G).y <= upper_bound rng(max(F,G))
  proof
    let y;
    assume y in dom max(F,G);
    then max(F,G).y in rng max(F,G) by FUNCT_1:def 3;
    hence thesis by A6,SEQ_4:def 1;
  end;
  rng G is real-bounded by Th1;
  then
A8: rng G is bounded_above by XXREAL_2:def 11;
A9: for y st y in dom G holds G.y <= upper_bound rng G
  proof
    let y;
    assume y in dom G;
    then G.y in rng G by FUNCT_1:def 3;
    hence thesis by A8,SEQ_4:def 1;
  end;
A10: for s being real number st 0<s
 ex y st y in dom G & upper_bound rng G-s <= max(
  F,G).y
  proof
    let s being real number;
    assume 0<s;
    then consider r being real number such that
A11: r in rng G and
A12: upper_bound rng G-s<r by A8,SEQ_4:def 1;
    consider y being set such that
A13: y in dom G and
A14: r = G.y by A11,FUNCT_1:def 3;
    G.y <= max(F.y,G.y) by XXREAL_0:25;
    then r <= max(F,G).y by A13,A14,FUZZY_1:def 4;
    hence thesis by A12,A13,XXREAL_0:2;
  end;
  for s being real number st 0<s
   holds upper_bound rng G-s <= upper_bound rng max(F,G)
  proof
    let s being real number;
    assume 0<s;
    then consider y such that
A15: y in dom G and
A16: upper_bound rng G - s <= max(F,G).y by A10;
    y in C2 by A15;
    then y in dom max(F,G) by FUNCT_2:def 1;
    then max(F,G).y <= upper_bound rng max(F,G) by A7;
    hence thesis by A16,XXREAL_0:2;
  end;
  then
A17: upper_bound rng G <= upper_bound rng(max(F,G)) by XREAL_1:57;
  rng F is real-bounded by Th1;
  then
A18: rng F is bounded_above by XXREAL_2:def 11;
A19: for s being real number st 0<s
 ex y st y in dom F & upper_bound rng F-s <= max(
  F,G).y
  proof
    let s being real number;
    assume 0<s;
    then consider r being real number such that
A20: r in rng F and
A21: upper_bound rng F-s<r by A18,SEQ_4:def 1;
    consider y being set such that
A22: y in dom F and
A23: r = F.y by A20,FUNCT_1:def 3;
    F.y <= max(F.y,G.y) by XXREAL_0:25;
    then r <= max(F,G).y by A22,A23,FUZZY_1:def 4;
    hence thesis by A21,A22,XXREAL_0:2;
  end;
  for s being real number st 0<s
   holds upper_bound rng F-s <= upper_bound rng max(F,G)
  proof
    let s being real number;
    assume 0<s;
    then consider y such that
A24: y in dom F and
A25: upper_bound rng F - s <= max(F,G).y by A19;
    y in C2 by A24;
    then y in dom max(F,G) by FUNCT_2:def 1;
    then max(F,G).y <= upper_bound rng max(F,G) by A7;
    hence thesis by A25,XXREAL_0:2;
  end;
  then upper_bound rng F <= upper_bound rng(max(F,G)) by XREAL_1:57;
  then
A26: upper_bound rng(max(F,G)) >=
 max(upper_bound rng F,upper_bound rng G) by A17,XXREAL_0:28;
A27: for y st y in dom F holds F.y <= upper_bound rng F
  proof
    let y;
    assume y in dom F;
    then F.y in rng F by FUNCT_1:def 3;
    hence thesis by A18,SEQ_4:def 1;
  end;
  for s being real number st 0<s
   holds upper_bound rng max(F,G) - s <= max(upper_bound
  rng F,upper_bound rng G)
  proof
    let s being real number;
    assume 0<s;
    then consider r being real number such that
A28: r in rng max(F,G) and
A29: upper_bound rng max(F,G)-s<r by A6,SEQ_4:def 1;
    consider y be set such that
A30: y in dom max(F,G) and
A31: r = max(F,G).y by A28,FUNCT_1:def 3;
A32: y in C2 by A30;
    then y in dom G by FUNCT_2:def 1;
    then
A33: G.y <= upper_bound rng G by A9;
    y in dom F by A32,FUNCT_2:def 1;
    then F.y <= upper_bound rng F by A27;
    then
A34: max(F.y,G.y) <=
 max(upper_bound rng F,upper_bound rng G) by A33,XXREAL_0:26;
    upper_bound rng max(F,G)-s<=max(F.y,G.y) by A29,A30,A31,FUZZY_1:def 4;
    hence thesis by A34,XXREAL_0:2;
  end;
  then
A35: upper_bound rng(max(F,G)) <=
 max(upper_bound rng F,upper_bound rng G) by XREAL_1:57;
  dom min(max(f,g),h,x,z) = C2 by FUNCT_2:def 1;
  then min(max(f,g),h,x,z) = max(min(f,h,x,z),min(g,h,x,z)) by A5,A3,PARTFUN1:5
;
  hence thesis by A35,A26,XXREAL_0:1;
end;

theorem
  for f,g be RMembership_Func of C1,C2, h be RMembership_Func of C2,C3
  holds (max(f,g))(#)h = max(f(#)h,g(#)h)
proof
  let f,g be RMembership_Func of C1,C2, h be RMembership_Func of C2,C3;
A1: dom max(f(#)h,g(#)h) = [:C1,C3:] by FUNCT_2:def 1;
A2: for c being Element of [:C1,C3:] st c in [:C1,C3:] holds ((max(f,g))(#)h
  ).c = max(f(#)h,g(#)h).c
  proof
    let c being Element of [:C1,C3:];
    consider x,z being set such that
A3: x in C1 and
A4: z in C3 and
A5: c = [x,z] by ZFMISC_1:def 2;
    ((max(f,g))(#)h).c = ((max(f,g))(#)h).(x,z) by A5
      .= upper_bound(rng(min(max(f,g),h,x,z))) by A5,Def3
      .= max(upper_bound rng(min(f,h,x,z)),upper_bound rng(min(g,h,x,z)))
       by A3,A4,Lm2
      .= max((f(#)h).(x,z),upper_bound rng(min(g,h,x,z))) by A5,Def3
      .= max((f(#)h).(x,z),(g(#)h).(x,z)) by A5,Def3
      .= max(f(#)h,g(#)h).c by A5,FUZZY_1:def 4;
    hence thesis;
  end;
  dom((max(f,g))(#)h) = [:C1,C3:] by FUNCT_2:def 1;
  hence thesis by A1,A2,PARTFUN1:5;
end;

Lm3: for f be RMembership_Func of C1,C2, g,h be RMembership_Func of C2,C3, x,z
be set st x in C1 & z in C3
 holds upper_bound(rng(min(f,min(g,h),x,z))) <= min(upper_bound rng(
min(f,g,x,z)),upper_bound rng(min(f,h,x,z)))
proof
  let f be RMembership_Func of C1,C2, g,h be RMembership_Func of C2,C3, x,z be
  set;
  assume that
A1: x in C1 and
A2: z in C3;
  set F = min(f,min(g,h),x,z), G = min(f,g,x,z), H = min(f,h,x,z);
  rng F is real-bounded by Th1;
  then
A3: rng F is bounded_above by XXREAL_2:def 11;
A4: for s being real number st 0<s
 ex y st y in dom F & upper_bound rng F - s <= G.
  y
  proof
    let s being real number;
    assume 0<s;
    then consider r being real number such that
A5: r in rng F and
A6: upper_bound rng F-s<r by A3,SEQ_4:def 1;
    consider y being set such that
A7: y in dom F and
A8: r = F.y by A5,FUNCT_1:def 3;
A9: [y,z] in [:C2,C3:] by A2,A7,ZFMISC_1:87;
    F.y = min(f. [x,y],min(g,h). [y,z]) by A1,A2,A7,Def2
      .= min(f. [x,y],min(g. [y,z],h. [y,z])) by A9,FUZZY_1:def 3
      .= min(min(f. [x,y],g. [y,z]),h. [y,z]) by XXREAL_0:33
      .= min(G.y,h. [y,z]) by A1,A2,A7,Def2;
    then r <= G.y by A8,XXREAL_0:17;
    hence thesis by A6,A7,XXREAL_0:2;
  end;
A10: for s being real number st 0<s
 ex y st y in dom F & upper_bound rng F - s <= H.
  y
  proof
    let s being real number;
    assume 0<s;
    then consider r being real number such that
A11: r in rng F and
A12: upper_bound rng F-s<r by A3,SEQ_4:def 1;
    consider y being set such that
A13: y in dom F and
A14: r = F.y by A11,FUNCT_1:def 3;
A15: [y,z] in [:C2,C3:] by A2,A13,ZFMISC_1:87;
    F.y = min(f. [x,y],min(g,h). [y,z]) by A1,A2,A13,Def2
      .= min(f. [x,y],min(g. [y,z],h. [y,z])) by A15,FUZZY_1:def 3
      .= min(min(f. [x,y],h. [y,z]),g. [y,z]) by XXREAL_0:33
      .= min(H.y,g. [y,z]) by A1,A2,A13,Def2;
    then r <= H.y by A14,XXREAL_0:17;
    hence thesis by A12,A13,XXREAL_0:2;
  end;
  rng H is real-bounded by Th1;
  then
A16: rng H is bounded_above by XXREAL_2:def 11;
A17: for y st y in dom H holds H.y <= upper_bound rng H
  proof
    let y;
    assume y in dom H;
    then H.y in rng H by FUNCT_1:def 3;
    hence thesis by A16,SEQ_4:def 1;
  end;
  for s being real number st 0<s
   holds upper_bound rng F - s <= upper_bound rng H
  proof
    let s being real number;
    assume 0<s;
    then consider y such that
A18: y in dom F and
A19: upper_bound rng F - s <= H.y by A10;
    y in C2 by A18;
    then y in dom H by FUNCT_2:def 1;
    then H.y <= upper_bound rng H by A17;
    hence thesis by A19,XXREAL_0:2;
  end;
  then
A20: upper_bound rng F <= upper_bound rng H by XREAL_1:57;
  rng G is real-bounded by Th1;
  then
A21: rng G is bounded_above by XXREAL_2:def 11;
A22: for y st y in dom G holds G.y <= upper_bound rng G
  proof
    let y;
    assume y in dom G;
    then G.y in rng G by FUNCT_1:def 3;
    hence thesis by A21,SEQ_4:def 1;
  end;
  for s being real number st 0<s
   holds upper_bound rng F - s <= upper_bound rng G
  proof
    let s being real number;
    assume 0<s;
    then consider y such that
A23: y in dom F and
A24: upper_bound rng F - s <= G.y by A4;
    y in C2 by A23;
    then y in dom G by FUNCT_2:def 1;
    then G.y <= upper_bound rng G by A22;
    hence thesis by A24,XXREAL_0:2;
  end;
  then upper_bound rng F <= upper_bound rng G by XREAL_1:57;
  hence thesis by A20,XXREAL_0:20;
end;

theorem
  for f be RMembership_Func of C1,C2, g,h be RMembership_Func of C2,C3
  holds f(#)(min(g,h)) c= min(f(#)g,f(#)h)
proof
  let f be RMembership_Func of C1,C2,g,h be RMembership_Func of C2,C3;
  let c be Element of [:C1,C3:];
  consider x,z being set such that
A1: x in C1 and
A2: z in C3 and
A3: c = [x,z] by ZFMISC_1:def 2;
A4: (f(#)(min(g,h))).(x,z) = upper_bound(rng(min(f,min(g,h),x,z))) by A3,Def3;
  min(f(#)g,f(#)h).(x,z) = min((f(#)g).(x,z),(f(#)h).(x,z)) by A3,FUZZY_1:def 3
    .= min((f(#)g).(x,z),upper_bound rng(min(f,h,x,z))) by A3,Def3
    .= min(upper_bound rng(min(f,g,x,z)),
    upper_bound rng(min(f,h,x,z))) by A3,Def3;
  hence thesis by A1,A2,A3,A4,Lm3;
end;

Lm4: for f,g be RMembership_Func of C1,C2, h be RMembership_Func of C2,C3, x,z
be set st x in C1 & z in C3
 holds upper_bound(rng(min(min(f,g),h,x,z))) <= min(upper_bound(rng(
min(f,h,x,z))),upper_bound(rng(min(g,h,x,z))))
proof
  let f,g be RMembership_Func of C1,C2, h be RMembership_Func of C2,C3, x,z be
  set;
  assume that
A1: x in C1 and
A2: z in C3;
  set F = min(min(f,g),h,x,z), G = min(f,h,x,z), H = min(g,h,x,z);
  rng F is real-bounded by Th1;
  then
A3: rng F is bounded_above by XXREAL_2:def 11;
A4: for s being real number st 0<s
 ex y st y in dom F & upper_bound rng F - s <= G.
  y
  proof
    let s being real number;
    assume 0<s;
    then consider r being real number such that
A5: r in rng F and
A6: upper_bound rng F-s<r by A3,SEQ_4:def 1;
    consider y being set such that
A7: y in dom F and
A8: r = F.y by A5,FUNCT_1:def 3;
A9: [x,y] in [:C1,C2:] by A1,A7,ZFMISC_1:87;
    F.y = min(min(f,g). [x,y],h. [y,z]) by A1,A2,A7,Def2
      .= min(min(f. [x,y],g. [x,y]),h. [y,z]) by A9,FUZZY_1:def 3
      .= min(min(h. [y,z],f. [x,y]),g. [x,y]) by XXREAL_0:33
      .= min(G.y,g. [x,y]) by A1,A2,A7,Def2;
    then r <= G.y by A8,XXREAL_0:17;
    hence thesis by A6,A7,XXREAL_0:2;
  end;
A10: for s being real number st 0<s
 ex y st y in dom F & upper_bound rng F - s <= H.
  y
  proof
    let s being real number;
    assume 0<s;
    then consider r being real number such that
A11: r in rng F and
A12: upper_bound rng F-s<r by A3,SEQ_4:def 1;
    consider y being set such that
A13: y in dom F and
A14: r = F.y by A11,FUNCT_1:def 3;
A15: [x,y] in [:C1,C2:] by A1,A13,ZFMISC_1:87;
    F.y = min(min(f,g). [x,y],h. [y,z]) by A1,A2,A13,Def2
      .= min(min(f. [x,y],g. [x,y]),h. [y,z]) by A15,FUZZY_1:def 3
      .= min(f. [x,y],min(h. [y,z],g. [x,y])) by XXREAL_0:33
      .= min(H.y,f. [x,y]) by A1,A2,A13,Def2;
    then r <= H.y by A14,XXREAL_0:17;
    hence thesis by A12,A13,XXREAL_0:2;
  end;
  rng H is real-bounded by Th1;
  then
A16: rng H is bounded_above by XXREAL_2:def 11;
A17: for y st y in dom H holds H.y <= upper_bound rng H
  proof
    let y;
    assume y in dom H;
    then H.y in rng H by FUNCT_1:def 3;
    hence thesis by A16,SEQ_4:def 1;
  end;
  for s being real number st 0<s
   holds upper_bound rng F - s <= upper_bound rng H
  proof
    let s being real number;
    assume 0<s;
    then consider y such that
A18: y in dom F and
A19: upper_bound rng F - s <= H.y by A10;
    y in C2 by A18;
    then y in dom H by FUNCT_2:def 1;
    then H.y <= upper_bound rng H by A17;
    hence thesis by A19,XXREAL_0:2;
  end;
  then
A20: upper_bound rng F <= upper_bound rng H by XREAL_1:57;
  rng G is real-bounded by Th1;
  then
A21: rng G is bounded_above by XXREAL_2:def 11;
A22: for y st y in dom G holds G.y <= upper_bound rng G
  proof
    let y;
    assume y in dom G;
    then G.y in rng G by FUNCT_1:def 3;
    hence thesis by A21,SEQ_4:def 1;
  end;
  for s being real number st 0<s
   holds upper_bound rng F - s <= upper_bound rng G
  proof
    let s being real number;
    assume 0<s;
    then consider y such that
A23: y in dom F and
A24: upper_bound rng F - s <= G.y by A4;
    y in C2 by A23;
    then y in dom G by FUNCT_2:def 1;
    then G.y <= upper_bound rng G by A22;
    hence thesis by A24,XXREAL_0:2;
  end;
  then upper_bound rng F <= upper_bound rng G by XREAL_1:57;
  hence thesis by A20,XXREAL_0:20;
end;

theorem
  for f,g be RMembership_Func of C1,C2, h be RMembership_Func of C2,C3
  holds min(f,g)(#)h c= min(f(#)h,g(#)h)
proof
  let f,g be RMembership_Func of C1,C2, h be RMembership_Func of C2,C3;
  let c be Element of [:C1,C3:];
  consider x,z being set such that
A1: x in C1 and
A2: z in C3 and
A3: c = [x,z] by ZFMISC_1:def 2;
A4: (min(f,g)(#)h).(x,z) = upper_bound(rng(min(min(f,g),h,x,z))) by A3,Def3;
  min(f(#)h,g(#)h).(x,z) = min((f(#)h).(x,z),(g(#)h).(x,z)) by A3,FUZZY_1:def 3
    .= min(upper_bound(rng(min(f,h,x,z))),(g(#)h).(x,z)) by A3,Def3
    .= min(upper_bound(rng(min(f,h,x,z))),
    upper_bound(rng(min(g,h,x,z)))) by A3,Def3;
  hence thesis by A1,A2,A3,A4,Lm4;
end;

Lm5: for f be RMembership_Func of C1,C2, g be RMembership_Func of C2,C3, x,z
be set st x in C1 & z in C3
 holds upper_bound rng min(converse g,converse f,z,x) = upper_bound
rng min(f,g,x,z)
proof
  let f be RMembership_Func of C1,C2, g be RMembership_Func of C2,C3, x,z be
  set;
  assume that
A1: x in C1 and
A2: z in C3;
  rng min(f,g,x,z) is real-bounded by Th1;
  then
A3: rng min(f,g,x,z) is bounded_above by XXREAL_2:def 11;
  for s being real number st 0<s
   holds upper_bound rng min(f,g,x,z) - s <= upper_bound
  rng min(converse g,converse f,z,x)
  proof
    let s being real number;
    assume s>0;
    then consider r being real number such that
A4: r in rng min(f,g,x,z) and
A5: upper_bound rng min(f,g,x,z) - s < r by A3,SEQ_4:def 1;
    consider y be set such that
A6: y in dom min(f,g,x,z) and
A7: r = min(f,g,x,z).y by A4,FUNCT_1:def 3;
A8: [z,y] in [:C3,C2:] by A2,A6,ZFMISC_1:87;
    y in C2 by A6;
    then y in dom min(converse g,converse f,z,x) by FUNCT_2:def 1;
    then
A9: min(converse g,converse f,z,x).y <=
 upper_bound rng min(converse g,converse f
    ,z,x) by Th1;
A10: [y,x] in [:C2,C1:] by A1,A6,ZFMISC_1:87;
    r = min(f.(x,y),g.(y,z)) by A1,A2,A6,A7,Def2
      .= min((converse f).(y,x),g.(y,z)) by A10,Def1
      .= min((converse f).(y,x),(converse g).(z,y)) by A8,Def1
      .= min(converse g,converse f,z,x).y by A1,A2,A6,Def2;
    hence thesis by A5,A9,XXREAL_0:2;
  end;
  then
A11: upper_bound rng min(converse g,converse f,z,x) >=
 upper_bound rng min(f,g,x,z) by XREAL_1:57;
  rng min(converse g,converse f,z,x) is real-bounded by Th1;
  then
A12: rng min(converse g,converse f,z,x) is bounded_above by XXREAL_2:def 11;
  for s being real number st 0<s
   holds upper_bound rng min(converse g,converse f,z
  ,x) - s <= upper_bound rng min(f,g,x,z)
  proof
    let s being real number;
    assume s>0;
    then consider r being real number such that
A13: r in rng min(converse g,converse f,z,x) and
A14: upper_bound rng min(converse g,converse f,z,x) - s < r by A12,SEQ_4:def 1;
    consider y be set such that
A15: y in dom min(converse g,converse f,z,x) and
A16: r = min(converse g,converse f,z,x).y by A13,FUNCT_1:def 3;
A17: [z,y] in [:C3,C2:] by A2,A15,ZFMISC_1:87;
    y in C2 by A15;
    then y in dom min(f,g,x,z ) by FUNCT_2:def 1;
    then
A18: min(f,g,x,z).y <= upper_bound rng min(f,g,x,z) by Th1;
A19: [y,x] in [:C2,C1:] by A1,A15,ZFMISC_1:87;
    r = min((converse g).(z,y),(converse f).(y,x)) by A1,A2,A15,A16,Def2
      .= min(g.(y,z),(converse f).(y,x)) by A17,Def1
      .= min(g.(y,z),f.(x,y)) by A19,Def1
      .= min(f,g,x,z).y by A1,A2,A15,Def2;
    hence thesis by A14,A18,XXREAL_0:2;
  end;
  then upper_bound rng min(converse g,converse f,z,x) <=
   upper_bound rng min(f,g,x,z) by XREAL_1:57;
  hence thesis by A11,XXREAL_0:1;
end;

theorem
  for f be RMembership_Func of C1,C2, g be RMembership_Func of C2,C3
  holds converse(f(#)g) = (converse g)(#)(converse f)
proof
  let f be RMembership_Func of C1,C2, g be RMembership_Func of C2,C3;
A1: dom((converse g)(#)(converse f)) = [:C3,C1:] by FUNCT_2:def 1;
A2: for c being Element of [:C3,C1:] st c in [:C3,C1:] holds (converse(f(#)g
  )).c = ((converse g)(#)(converse f)).c
  proof
    let c being Element of [:C3,C1:];
    assume c in [:C3,C1:];
    consider z,x be set such that
A3: z in C3 and
A4: x in C1 and
A5: c =[z,x] by ZFMISC_1:def 2;
A6: [x,z] in [:C1,C3:] by A3,A4,ZFMISC_1:87;
A7: ((converse g)(#)(converse f)).(z,x) =
 upper_bound rng min(converse g,converse
    f,z,x) by A5,Def3;
    (converse(f(#)g)).(z,x) = (f(#)g).(x,z) by A5,Def1
      .= upper_bound rng min(f,g,x,z) by A6,Def3;
    hence thesis by A3,A4,A5,A7,Lm5;
  end;
  dom converse(f(#)g) = [:C3,C1:] by FUNCT_2:def 1;
  hence thesis by A1,A2,PARTFUN1:5;
end;

theorem Th18:
  for f,g be RMembership_Func of C1,C2, h,k be RMembership_Func of
C2,C3, x,z be set st x in C1 & z in C3 & (for y be set st y in C2 holds f. [x,y
  ]<=g. [x,y] & h. [y,z]<=k. [y,z]) holds (f(#)h). [x,z] <= (g(#)k). [x,z]
proof
  let f,g be RMembership_Func of C1,C2, h,k be RMembership_Func of C2,C3, x,z
  be set;
  assume that
A1: x in C1 and
A2: z in C3 and
A3: for y be set st y in C2 holds f. [x,y]<=g. [x,y] & h. [y,z]<=k. [y, z];
A4: [x,z] in [:C1,C3:] by A1,A2,ZFMISC_1:87;
  then
A5: (g(#)k).(x,z) = upper_bound rng min(g,k,x,z) by Def3;
  rng min(f,h,x,z) is real-bounded by Th1;
  then
A6: rng min(f,h,x,z) is bounded_above by XXREAL_2:def 11;
A7: for s being real number st s>0
 holds upper_bound (rng (min(f,h,x,z))) - s <= upper_bound
  rng min(g,k,x,z)
  proof
    let s being real number;
    assume s>0;
    then consider r be real number such that
A8: r in rng min(f,h,x,z) and
A9: upper_bound rng min(f,h,x,z)-s<r by A6,SEQ_4:def 1;
    consider y being set such that
A10: y in dom min(f,h,x,z) and
A11: r=min(f,h,x,z).y by A8,FUNCT_1:def 3;
A12: h. [y,z]<=k. [y,z] by A3,A10;
    f. [x,y]<=g. [x,y] by A3,A10;
    then min(f. [x,y],h. [y,z]) <= min(g. [x,y],k. [y,z]) by A12,XXREAL_0:18;
    then
A13: min(f,h,x,z).y <= min(g. [x,y],k. [y,z]) by A1,A2,A10,Def2;
    y in C2 by A10;
    then
A14: y in dom min(g,k,x,z) by FUNCT_2:def 1;
    min(g. [x,y],k. [y,z]) = min(g,k,x,z).y by A1,A2,A10,Def2;
    then min(g. [x,y],k. [y,z]) <= upper_bound rng min(g,k,x,z) by A14,Th1;
    then min(f,h,x,z).y <= upper_bound rng min(g,k,x,z) by A13,XXREAL_0:2;
    hence thesis by A9,A11,XXREAL_0:2;
  end;
  (f(#)h).(x,z) = upper_bound (rng (min(f,h,x,z))) by A4,Def3;
  hence thesis by A5,A7,XREAL_1:57;
end;

theorem
  for f,g be RMembership_Func of C1,C2, h,k be RMembership_Func of C2,C3
  st f c= g & h c= k holds f(#)h c= g(#)k
proof
  let f,g be RMembership_Func of C1,C2, h,k being RMembership_Func of C2,C3;
  assume that
A1: f c= g and
A2: h c= k;
  let c be Element of [:C1,C3:];
  consider x,z being set such that
A3: x in C1 and
A4: z in C3 and
A5: c = [x,z] by ZFMISC_1:def 2;
  for y be set st y in C2 holds f. [x,y]<=g. [x,y] & h. [y,z]<=k. [y,z]
  proof
    let y be set;
    assume
A6: y in C2;
    then
A7: [y,z] in [:C2,C3:] by A4,ZFMISC_1:87;
    [x,y] in [:C1,C2:] by A3,A6,ZFMISC_1:87;
    hence thesis by A1,A2,A7,FUZZY_1:def 2;
  end;
  hence thesis by A3,A4,A5,Th18;
end;

begin

:: Definition of identity relation
:: and properties of universe relation and zero relation

definition
  let C1,C2 be non empty set;
  func Imf(C1,C2) -> RMembership_Func of C1,C2 means
  :Def4:
  for x,y st [x,y]
  in [:C1,C2:] holds (x=y implies it.(x,y) = 1) & (x<>y implies it.(x,y) = 0);
  existence
  proof
    defpred P[set,set,set] means ($1=$2 implies $3 = 1) & (not $1=$2 implies
    $3 = 0);
A1: for x,y,z1,z2 st x in C1 & y in C2 & P[x,y,z1] & P[x,y,z2] holds z1=z2;
A2: for x,y,z st x in C1 & y in C2 & P[x,y,z] holds z in REAL;
    consider IT being PartFunc of [:C1,C2:],REAL such that
A3: (for x,y holds [x,y] in dom IT iff x in C1 & y in C2 & ex z st P[x
,y,z]) & for x,y st [x,y] in dom IT holds P[x,y,IT.(x,y)] from BINOP_1:sch 5(A2
    ,A1);
    [:C1,C2:] c= dom IT
    proof
      let x,y be set;
A4:   not x=y implies ex z st (x=y implies z = 1) & (not x=y implies z = 0 );
      assume
A5:   [x,y] in [:C1,C2:];
      then
A6:   y in C2 by ZFMISC_1:87;
      x in C1 by A5,ZFMISC_1:87;
      hence thesis by A3,A6,A4;
    end;
    then
A7: dom IT = [:C1,C2:] by XBOOLE_0:def 10;
    rng IT c= [.0,1.]
    proof
      let c being set;
      assume c in rng IT;
      then consider z being Element of [:C1,C2:] such that
A8:   z in dom IT and
A9:   c = IT.z by PARTFUN1:3;
      consider x,y being set such that
      x in C1 and
      y in C2 and
A10:  z = [x,y] by ZFMISC_1:def 2;
A11:  1 in [.0,1.] & 0 in [.0,1.]
      proof
        reconsider A=[.0,1.] as
         non empty closed_interval Subset of REAL by MEASURE5:14;
A12:    A = [. lower_bound A, upper_bound A .] by INTEGRA1:4;
        then
A13:    1=upper_bound A by INTEGRA1:5;
        0=lower_bound A by A12,INTEGRA1:5;
        hence thesis by A13,INTEGRA2:1;
      end;
      then
A14:  x<>y implies IT.(x,y) in [.0 , 1.] by A3,A8,A10;
      x=y implies IT.(x,y) in [.0,1.] by A3,A8,A10,A11;
      hence thesis by A9,A10,A14;
    end;
    then IT is RMembership_Func of C1,C2 by A7,FUNCT_2:def 1,RELAT_1:def 19;
    hence thesis by A3,A7;
  end;
  uniqueness
  proof
    let F,G be RMembership_Func of C1,C2;
    assume that
A15: for x,y st [x,y] in [:C1,C2:] holds (x=y implies F.(x,y) = 1) & (
    x<>y implies F.(x,y) = 0) and
A16: for x,y st [x,y] in [:C1,C2:] holds (x=y implies G.(x,y) = 1) & (
    x<>y implies G.(x,y) = 0);
A17: for x,y st x in C1 & y in C2 holds F.(x,y) = G.(x,y)
    proof
      let x,y be set;
      assume that
A18:  x in C1 and
A19:  y in C2;
A20:  [x,y] in [:C1,C2:] by A18,A19,ZFMISC_1:87;
      then
A21:  not x=y implies F.(x,y) = 0 by A15;
      x=y implies F.(x,y) = 1 by A15,A20;
      hence thesis by A16,A20,A21;
    end;
A22: dom G = [:C1,C2:] by FUNCT_2:def 1;
    dom F = [:C1,C2:] by FUNCT_2:def 1;
    hence thesis by A22,A17,FUNCT_3:6;
  end;
end;

theorem
  for c be Element of [:C1,C2:] holds (Zmf(C1,C2)).c = 0 & (Umf(C1,C2)).
  c = 1 by FUNCT_3:def 3;

theorem
  for x,y st [x,y] in [:C1,C2:] holds (Zmf(C1,C2)). [x,y] = 0 & (Umf(C1,
  C2)). [x,y] = 1 by FUNCT_3:def 3;

Lm6: for f be RMembership_Func of C2,C3, x,z be set st x in C1 & z in C3 holds
upper_bound rng min(Zmf(C1,C2),f,x,z) = Zmf(C1,C3). [x,z]
proof
  let f be RMembership_Func of C2,C3, x,z be set;
  assume that
A1: x in C1 and
A2: z in C3;
  rng min(Zmf(C1,C2),f,x,z) is real-bounded by Th1;
  then
A3: rng min(Zmf(C1,C2),f,x,z) is bounded_above by XXREAL_2:def 11;
  for s being real number st 0<s
   holds upper_bound rng min(Zmf(C1,C2),f,x,z) - s
  <= Zmf(C1,C3). [x,z]
  proof
    let s being real number;
    assume s>0;
    then consider r being real number such that
A4: r in rng min(Zmf(C1,C2),f,x,z) and
A5: upper_bound rng min(Zmf(C1,C2),f,x,z) - s < r by A3,SEQ_4:def 1;
    consider y be set such that
A6: y in dom min(Zmf(C1,C2),f,x,z) and
A7: r = min(Zmf(C1,C2),f,x,z).y by A4,FUNCT_1:def 3;
A8: [x,y] in [:C1,C2:] by A1,A6,ZFMISC_1:87;
A9: [x,z] in [:C1,C3:] by A1,A2,ZFMISC_1:87;
A10: 0 <= f. [y,z] by Th3;
    r = min(Zmf(C1,C2). [x,y],f. [y,z]) by A1,A2,A6,A7,Def2
      .= min(0,f. [y,z]) by A8,FUNCT_3:def 3
      .= 0 by A10,XXREAL_0:def 9
      .= Zmf(C1,C3). [x,z] by A9,FUNCT_3:def 3;
    hence thesis by A5;
  end;
  then
A11: upper_bound rng min(Zmf(C1,C2),f,x,z) <= Zmf(C1,C3). [x,z] by XREAL_1:57;
  upper_bound rng min(Zmf(C1,C2),f,x,z) >= Zmf(C1,C3). [x,z]
  proof
    reconsider A=[.0,1.] as
     non empty closed_interval Subset of REAL by MEASURE5:14;
A12: A is bounded_below by INTEGRA1:3;
    rng min(Zmf(C1,C2),f,x,z) c= [.0,1.] by RELAT_1:def 19;
    then
A13: lower_bound A <= lower_bound rng min(Zmf(C1,C2),f,x,z) by A12,SEQ_4:47;
    A = [. lower_bound A, upper_bound A .] by INTEGRA1:4;
    then
A14: 0=lower_bound A by INTEGRA1:5;
A15: lower_bound rng min(Zmf(C1,C2),f,x,z) <=
 upper_bound rng min(Zmf(C1,C2),f,x,z) by Th1,SEQ_4:11;
    [x,z] in [:C1,C3:] by A1,A2,ZFMISC_1:87;
    hence thesis by A14,A13,A15,FUNCT_3:def 3;
  end;
  hence thesis by A11,XXREAL_0:1;
end;

theorem Th22:
  for f be RMembership_Func of C2,C3 holds Zmf(C1,C2)(#)f = Zmf(C1 ,C3)
proof
  let f be RMembership_Func of C2,C3;
A1: dom(Zmf(C1,C3)) = [:C1,C3:] by FUNCT_2:def 1;
A2: for c being Element of [:C1,C3:] st c in [:C1,C3:] holds (Zmf(C1,C2)(#)f
  ).c = Zmf(C1,C3).c
  proof
    let c be Element of [:C1,C3:];
    consider x,z being set such that
A3: x in C1 and
A4: z in C3 and
A5: c = [x,z] by ZFMISC_1:def 2;
    (Zmf(C1,C2)(#)f).c = (Zmf(C1,C2)(#)f).(x,z) by A5
      .= upper_bound rng min(Zmf(C1,C2),f,x,z) by A5,Def3
      .= Zmf(C1,C3).c by A3,A4,A5,Lm6;
    hence thesis;
  end;
  dom(Zmf(C1,C2)(#)f) = [:C1,C3:] by FUNCT_2:def 1;
  hence thesis by A1,A2,PARTFUN1:5;
end;

Lm7: for f be RMembership_Func of C1,C2, x,z be set st x in C1 & z in C3 holds
upper_bound rng min(f,Zmf(C2,C3),x,z) = Zmf(C1,C3). [x,z]
proof
  let f be RMembership_Func of C1,C2, x,z be set;
  assume that
A1: x in C1 and
A2: z in C3;
  rng min(f,Zmf(C2,C3),x,z) is real-bounded by Th1;
  then
A3: rng min(f,Zmf(C2,C3),x,z) is bounded_above by XXREAL_2:def 11;
  for s being real number st 0<s
   holds upper_bound rng min(f,Zmf(C2,C3),x,z) - s
  <= Zmf(C1,C3). [x,z]
  proof
    let s being real number;
    assume s>0;
    then consider r being real number such that
A4: r in rng min(f,Zmf(C2,C3),x,z) and
A5: upper_bound rng min(f,Zmf(C2,C3),x,z) - s < r by A3,SEQ_4:def 1;
    consider y be set such that
A6: y in dom min(f,Zmf(C2,C3),x,z) and
A7: r = min(f,Zmf(C2,C3),x,z).y by A4,FUNCT_1:def 3;
A8: [y,z] in [:C2,C3:] by A2,A6,ZFMISC_1:87;
A9: [x,z] in [:C1,C3:] by A1,A2,ZFMISC_1:87;
A10: 0 <= f. [x,y] by Th3;
    r = min(f. [x,y],Zmf(C2,C3). [y,z]) by A1,A2,A6,A7,Def2
      .= min(f. [x,y],0) by A8,FUNCT_3:def 3
      .= 0 by A10,XXREAL_0:def 9
      .= Zmf(C1,C3). [x,z] by A9,FUNCT_3:def 3;
    hence thesis by A5;
  end;
  then
A11: upper_bound rng min(f,Zmf(C2,C3),x,z) <= Zmf(C1,C3). [x,z] by XREAL_1:57;
  upper_bound rng min(f,Zmf(C2,C3),x,z) >= Zmf(C1,C3). [x,z]
  proof
    reconsider A=[.0,1.] as
     non empty closed_interval Subset of REAL by MEASURE5:14;
A12: A is bounded_below by INTEGRA1:3;
    rng min(f,Zmf(C2,C3),x,z) c= [.0,1.] by RELAT_1:def 19;
    then
A13: lower_bound A <= lower_bound rng min(f,Zmf(C2,C3),x,z) by A12,SEQ_4:47;
    A = [. lower_bound A, upper_bound A .] by INTEGRA1:4;
    then
A14: 0=lower_bound A by INTEGRA1:5;
A15: lower_bound rng min(f,Zmf(C2,C3),x,z) <=
 upper_bound rng min(f,Zmf(C2,C3),x,z) by Th1,SEQ_4:11;
    [x,z] in [:C1,C3:] by A1,A2,ZFMISC_1:87;
    hence thesis by A14,A13,A15,FUNCT_3:def 3;
  end;
  hence thesis by A11,XXREAL_0:1;
end;

theorem Th23:
  for f be RMembership_Func of C1,C2 holds f(#)Zmf(C2,C3) = Zmf(C1 ,C3)
proof
  let f be RMembership_Func of C1,C2;
A1: dom(Zmf(C1,C3)) = [:C1,C3:] by FUNCT_2:def 1;
A2: for c being Element of [:C1,C3:] st c in [:C1,C3:] holds (f(#)Zmf(C2,C3)
  ).c = Zmf(C1,C3).c
  proof
    let c be Element of [:C1,C3:];
    consider x,z being set such that
A3: x in C1 and
A4: z in C3 and
A5: c = [x,z] by ZFMISC_1:def 2;
    (f(#)Zmf(C2,C3)).c = (f(#)Zmf(C2,C3)).(x,z) by A5
      .= upper_bound rng min(f,Zmf(C2,C3),x,z) by A5,Def3
      .= Zmf(C1,C3).c by A3,A4,A5,Lm7;
    hence thesis;
  end;
  dom(f(#)Zmf(C2,C3)) = [:C1,C3:] by FUNCT_2:def 1;
  hence thesis by A1,A2,PARTFUN1:5;
end;

theorem
  for f be RMembership_Func of C1,C1 holds f(#)Zmf(C1,C1) = Zmf(C1,C1) (#)f
proof
  let f be RMembership_Func of C1,C1;
  f(#)Zmf(C1,C1) = Zmf(C1,C1) by Th23;
  hence thesis by Th22;
end;

begin :: Addenda
:: missing, 2006.12.03, AT

theorem
  for X,Y being non empty set for x being Element of X, y being Element
of Y holds (x = y implies Imf(X,Y).(x,y) = 1) & (x <> y implies Imf(X,Y).(x,y)
  = 0)
proof
  let X,Y being non empty set;
  let x being Element of X, y being Element of Y;
  [x,y] in [:X,Y:] by ZFMISC_1:87;
  hence thesis by Def4;
end;

theorem
  for X,Y being non empty set for x being Element of X, y being Element
  of Y for f being RMembership_Func of X,Y holds (converse f).(y,x) = f.(x,y)
proof
  let X,Y being non empty set;
  let x being Element of X, y being Element of Y;
  let f being RMembership_Func of X,Y;
  [y,x] in [:Y,X:] by ZFMISC_1:87;
  hence thesis by Def1;
end;