ROUGHIF1

:: Formal Development of Rough Inclusion Functions
::  by Adam Grabowski
:: 
:: Received August 29, 2019
:: Copyright (c) 2019-2026 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 STRUCT_0, ORDERS_2, RELAT_1, TARSKI, ZFMISC_1, XBOOLE_0,
      SUBSET_1, FUNCT_1, ROUGHS_1, ROUGHS_2, ROUGHS_5, ROUGHIF1, FINSET_1,
      CARD_1, REAL_1, NUMBERS, ARYTM_3, XXREAL_0, XXREAL_1, ARYTM_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, BINOP_1, ENUMSET1, ORDINAL1,
      XCMPLX_0, XXREAL_0, FINSET_1, CARD_1, XREAL_0, PARTFUN1, FUNCT_2,
      RCOMP_1, STRUCT_0, ORDERS_2, ROUGHS_1, ROUGHS_2, ROUGHS_5;
 constructors REALSET2, ROUGHS_1, ROUGHS_2, RCOMP_1, RVSUM_1, ROUGHS_5;
 registrations XBOOLE_0, SUBSET_1, FINSET_1, NAT_1, STRUCT_0, ORDERS_2,
      ROUGHS_1, CARD_1, ORDINAL1, XXREAL_0, XREAL_0, MEMBERED, FUZNORM1,
      XCMPLX_0;
 requirements BOOLE, SUBSET, NUMERALS, REAL, ARITHM;
 equalities SUBSET_1, STRUCT_0, ROUGHS_5;
 expansions TARSKI, XBOOLE_0;
 theorems XBOOLE_1, SUBSET_1, ZFMISC_1, CARD_1, XXREAL_1, NAT_1, XREAL_1,
      XCMPLX_1, CARD_2, BINOP_1, ENUMSET1, PRE_TOPC, TDLAT_1, ROUGHS_5,
      XXREAL_0;
 schemes BINOP_1;

begin :: Preliminaries

theorem Lemacik:
  for a,b,c being Real st a <= b & b > 0 & c >= 0
     holds a / b <= (a + c) / (b + c)
  proof
    let a,b,c be Real;
    assume
A1: a <= b & b > 0 & c >= 0; then
    a * c <= b * c by XREAL_1:64; then
    a * b + a * c <= a * b + b * c by XREAL_1:6; then
    a * (b + c) <= b * (a + c);
    hence thesis by XREAL_1:102,A1;
  end;

registration
  cluster strict finite for Approximation_Space;
  existence
  proof
    set R = RelStr (# {{}}, id {{}} #);
    take R;
    thus thesis;
  end;
end;

registration let R be finite 1-sorted;
  cluster -> finite for Subset of R;
  coherence;
end;

 reserve R for 1-sorted;
 reserve X,Y for Subset of R;

theorem LemmaSet:
  X c= Y iff X` \/ Y = [#]R
  proof
    thus X c= Y implies X` \/ Y = [#]R
    proof
      assume X c= Y; then
      X \ Y = {} by XBOOLE_1:37; then
      (X \ Y)` = [#]R;
      hence thesis by SUBSET_1:14;
    end;
    assume X` \/ Y = [#]R; then
    (X \ Y)`` = ({}R)`` by SUBSET_1:14;
    hence thesis by XBOOLE_1:37;
  end;

 reserve R for finite 1-sorted;
 reserve X,Y for Subset of R;

theorem LemmaCard:
  card (X \/ Y) = card Y iff X c= Y
  proof
    X c= X \/ Y & Y c= X \/ Y by XBOOLE_1:7;
    hence card (X \/ Y) = card Y implies X c= Y by CARD_2:102;
    assume X c= Y;
    hence thesis by XBOOLE_1:12;
  end;

theorem LemmaCard2:
  card (X` \/ Y) = card [#]R implies X` \/ Y = [#]R by CARD_2:102;

registration let R be non empty 1-sorted;
             let X be Subset of R;
  reduce [#]R \/ X to [#]R;
  reducibility by XBOOLE_1:12;
  reduce [#]R /\ X to X;
  reducibility by XBOOLE_1:28;
end;

begin :: Standard Rough Inclusion Function

 reserve R for finite Approximation_Space;
 reserve X,Y,Z,W for Subset of R;

definition let R be finite Approximation_Space;
           let X,Y be Subset of R;
  func kappa (X,Y) -> Element of [.0,1.] equals :KappaDef:
     card (X /\ Y) / card X if X <> {}
     otherwise 1;
  coherence
  proof
AA: card (X /\ Y) <= card X by NAT_1:43,XBOOLE_1:17;
    card (X /\ Y) / card X <= 1 by AA,XREAL_1:185;
    hence thesis by XXREAL_1:1;
  end;
  consistency;
end;

theorem
  kappa ({}R,X) = 1 by KappaDef;

theorem Prop1a: :: Proposition 1 a)
  kappa (X,Y) = 1 iff X c= Y
  proof
    per cases;
    suppose
A1: X <> {};
    thus kappa (X,Y) = 1 implies X c= Y
    proof
      assume kappa (X,Y) = 1; then
      card (X /\ Y) / card X = 1 by KappaDef,A1; then
      card (X /\ Y) = card X by XCMPLX_1:58; then
      X /\ Y = X by CARD_2:102,XBOOLE_1:17;
      hence thesis by XBOOLE_1:17;
    end;
    assume X c= Y; then
    X /\ Y = X by XBOOLE_1:28; then
    kappa (X,Y) = card X / card X by A1,KappaDef;
    hence thesis by XCMPLX_1:60,A1;
    end;
    suppose
      X = {};
      hence thesis by KappaDef;
    end;
  end;

theorem Prop1b: :: Proposition 1 b)
  Y c= Z implies kappa (X,Y) <= kappa (X,Z)
  proof
    assume
A0: Y c= Z;
    per cases;
    suppose
A1:   X <> {};
      card (X /\ Y) <= card (X /\ Z) by NAT_1:43,A0,XBOOLE_1:26; then
      card (X /\ Y) / card X <= card (X /\ Z) / card X by XREAL_1:72; then
      kappa (X,Y) <= card (X /\ Z) / card X by A1,KappaDef;
      hence thesis by A1,KappaDef;
    end;
    suppose X = {}; then
      kappa (X,Y) = 1 & kappa (X,Z) = 1 by KappaDef;
      hence thesis;
    end;
  end;

theorem :: Proposition 1 c)
  Z c= Y c= X implies kappa (X,Z) <= kappa (Y,Z)
  proof
    assume
AA: Z c= Y c= X;
    per cases;
    suppose
A1:   X <> {} & Y <> {}; then
      kappa (Y,Z) = card (Y /\ Z) / card Y by KappaDef; then
F1:   kappa (Y,Z) = card Z / card Y by AA,XBOOLE_1:28;
      Z c= X by AA; then
e2:   X /\ Z = Z by XBOOLE_1:28;
      kappa (X,Z) = card Z / card X by e2,A1,KappaDef;
      hence thesis by A1,XREAL_1:118,F1,AA,NAT_1:43;
    end;
    suppose X = {} & Y <> {};
      hence thesis by AA;
    end;
    suppose X = {} & Y = {};
      hence thesis;
    end;
    suppose X <> {} & Y = {}; then
      kappa (Y,Z) = 1 by KappaDef;
      hence thesis by XXREAL_1:1;
    end;
  end;

theorem Prop1d: :: binary variant of Proposition 1 d)
  kappa (X, Y \/ Z) <= kappa (X,Y) + kappa (X,Z)
  proof
    per cases;
    suppose
A0:   X <> {}; then
A1:   kappa (X, Y \/ Z) = card (X /\ (Y \/ Z)) / card X by KappaDef;
A2:   kappa (X, Y) = card (X /\ Y) / card X by A0,KappaDef;
A3:   kappa (X, Z) = card (X /\ Z) / card X by A0,KappaDef;
      X /\ (Y \/ Z) = (X /\ Y) \/ (X /\ Z) by XBOOLE_1:23; then
      card (X /\ (Y \/ Z)) / card X <=
        (card (X /\ Y) + card (X /\ Z)) / card X by XREAL_1:72,CARD_2:43;
      hence thesis by A2,A3,A1,XCMPLX_1:62;
    end;
    suppose
A2:   X = {}; then
A3:   kappa (X, Y \/ Z) = 1 by KappaDef;
      kappa (X, Y) = 1 & kappa (X, Z) = 1 by A2,KappaDef;
      hence thesis by A3;
    end;
  end;

theorem Prop1e: :: binary variant of Proposition 1 e)
  X <> {} & Y misses Z implies
    kappa (X,Y \/ Z) = kappa (X,Y) + kappa (X,Z)
  proof
    assume
A0: X <> {} & Y misses Z; then
A1: kappa (X,Y \/ Z) = card (X /\ (Y \/ Z)) / card X by KappaDef
       .= card ((X /\ Y) \/ (X /\ Z)) / card X by XBOOLE_1:23;
A2: kappa (X,Y) = card (X /\ Y) / card X &
      kappa (X,Z) = card (X /\ Z) / card X by A0,KappaDef;
    card ((X /\ Y) \/ (X /\ Z)) = card (X /\ Y) + card (X /\ Z)
      by CARD_2:40,A0,XBOOLE_1:76;
    hence thesis by A2,A1,XCMPLX_1:62;
  end;

begin :: Rough Inclusion Functions

definition let R be 1-sorted;
  mode preRoughInclusionFunction of R is
    Function of [:bool the carrier of R, bool the carrier of R:],
      [.0,1.];
end;

definition let R be 1-sorted;
  mode preRIF of R is preRoughInclusionFunction of R;
end;

scheme BinOpEq {R() -> non empty 1-sorted,
  F(Subset of R(), Subset of R()) -> Element of [.0,1.]} :
  for f1, f2 being preRIF of R() st
    (for x,y being Subset of R() holds f1.(x,y) = F(x,y)) &
    (for x,y being Subset of R() holds f2.(x,y) = F(x,y)) holds
      f1 = f2
    proof
      let f1, f2 be preRIF of R() such that
A1:   (for x,y being Subset of R() holds f1.(x,y) = F(x,y)) and
A2:   (for x,y being Subset of R() holds f2.(x,y) = F(x,y));
      for x,y being Element of bool the carrier of R() holds
         f2.(x,y) = f1.(x,y)
      proof
        let x,y be Element of bool the carrier of R();
        f1.(x,y) = F(x,y) by A1
                .= f2.(x,y) by A2;
        hence thesis;
      end;
      hence thesis by BINOP_1:2;
    end;

definition let R be finite Approximation_Space;
  func kappa R -> preRIF of R means :DefKappa:
  for x,y being Subset of R holds it.(x,y) = kappa (x,y);
  existence
  proof
    deffunc F(Subset of R,Subset of R) = kappa ($1,$2);
    ex f being preRIF of R st
    for x,y being Element of bool the carrier of R holds
      f.(x,y) = F(x,y) from BINOP_1:sch 4; then
    consider f being
    Function of [:bool the carrier of R, bool the carrier of R:],
      [.0,1.] such that
A1: for x,y being Element of bool the carrier of R holds
      f.(x,y) = F(x,y);
    take f;
    thus thesis by A1;
  end;
  uniqueness
  proof
    deffunc F(Subset of R,Subset of R) = kappa($1,$2);
    for f1, f2 being preRIF of R st
    (for x,y being Subset of R holds f1.(x,y) = F(x,y)) &
    (for x,y being Subset of R holds f2.(x,y) = F(x,y)) holds
      f1 = f2 from BinOpEq;
    hence thesis;
  end;
end;

begin :: Defining Two New RIFs

definition let R be finite Approximation_Space;
           let X,Y be Subset of R;
  func kappa_1 (X,Y) -> Element of [.0,1.] equals :Kappa1:
     card Y / card (X \/ Y) if X \/ Y <> {}
     otherwise 1;
  coherence
  proof
    card Y / card (X \/ Y) in [.0,1.]
    proof
      card Y <= card (X \/ Y) by NAT_1:43,XBOOLE_1:7; then
      card Y / card (X \/ Y) <= 1 by XREAL_1:183;
      hence thesis by XXREAL_1:1;
    end;
    hence thesis by XXREAL_1:1;
  end;
  consistency;
  func kappa_2 (X,Y) -> Element of [.0,1.] equals
     card (X` \/ Y) / card ([#]R);
  coherence
  proof
    card (X` \/ Y) / card ([#]R) in [.0,1.]
    proof
      card (X` \/ Y) / card ([#]R) <= 1 by XREAL_1:183,NAT_1:43;
      hence thesis by XXREAL_1:1;
    end;
    hence thesis;
  end;
end;

definition let R be finite Approximation_Space;
  func kappa_1 R -> preRIF of R means :DefKappa1:
  for x,y being Subset of R holds it.(x,y) = kappa_1 (x,y);
  existence
  proof
    deffunc F(Subset of R,Subset of R) = kappa_1 ($1,$2);
    ex f being Function of [:bool the carrier of R, bool the carrier of R:],
      [.0,1.] st
    for x,y being Element of bool the carrier of R holds
      f.(x,y) = F(x,y) from BINOP_1:sch 4; then
    consider f being
    Function of [:bool the carrier of R, bool the carrier of R:],
      [.0,1.] such that
A1: for x,y being Element of bool the carrier of R holds
      f.(x,y) = F(x,y);
    take f;
    thus thesis by A1;
  end;
  uniqueness
  proof
    deffunc F(Subset of R,Subset of R) = kappa_1($1,$2);
    for f1, f2 being
     Function of [:bool the carrier of R, bool the carrier of R:],
      [.0,1.] st
    (for x,y being Subset of R holds f1.(x,y) = F(x,y)) &
    (for x,y being Subset of R holds f2.(x,y) = F(x,y)) holds
      f1 = f2 from BinOpEq;
    hence thesis;
  end;
  func kappa_2 R -> preRIF of R means :DefKappa2:
  for x,y being Subset of R holds it.(x,y) = kappa_2 (x,y);
  existence
  proof
    deffunc F(Subset of R,Subset of R) = kappa_2 ($1,$2);
    ex f being Function of [:bool the carrier of R, bool the carrier of R:],
      [.0,1.] st
    for x,y being Element of bool the carrier of R holds
      f.(x,y) = F(x,y) from BINOP_1:sch 4; then
    consider f being
    Function of [:bool the carrier of R, bool the carrier of R:],
      [.0,1.] such that
A1: for x,y being Element of bool the carrier of R holds
      f.(x,y) = F(x,y);
    take f;
    thus thesis by A1;
  end;
  uniqueness
  proof
    deffunc F(Subset of R,Subset of R) = kappa_2($1,$2);
    for f1, f2 being
     Function of [:bool the carrier of R, bool the carrier of R:],
      [.0,1.] st
    (for x,y being Subset of R holds f1.(x,y) = F(x,y)) &
    (for x,y being Subset of R holds f2.(x,y) = F(x,y)) holds
      f1 = f2 from BinOpEq;
    hence thesis;
  end;
end;

theorem Prop11a: :: rif_1 for kappa_1
  kappa_1 (X,Y) = 1 iff X c= Y
  proof
    per cases;
    suppose
A1:   X \/ Y <> {} & Y <> {}; then
B1:   kappa_1 (X,Y) = card Y / card (X \/ Y) by Kappa1;
      thus kappa_1 (X,Y) = 1 implies X c= Y
      proof
        assume kappa_1 (X,Y) = 1; then
        card Y = card (X \/ Y) by XCMPLX_1:58,B1;
        hence thesis by LemmaCard;
      end;
      assume X c= Y; then
      card (X \/ Y) = card Y by XBOOLE_1:12;
      hence thesis by A1,XCMPLX_1:60,B1;
    end;
    suppose
A1:   X \/ Y <> {} & Y = {}; then
      kappa_1 (X,Y) = card Y / card (X \/ Y) by Kappa1
        .= 0 by A1;
      hence thesis by A1;
    end;
    suppose
      X \/ Y = {};
      hence thesis by Kappa1;
    end;
  end;

theorem Prop11b: :: rif_1 for kappa_2
  kappa_2 (X,Y) = 1 iff X c= Y
  proof
    thus kappa_2 (X,Y) = 1 implies X c= Y
    proof
      assume kappa_2 (X,Y) = 1; then
      card (X` \/ Y) = card ([#]R) by XCMPLX_1:58;
      hence thesis by LemmaSet,LemmaCard2;
    end;
    assume X c= Y; then
    X` \/ Y = [#]R by LemmaSet;
    hence thesis by XCMPLX_1:60;
  end;

theorem LemmaProp4a:
  kappa_1 (X,Y) = 0 implies Y = {}
  proof
    assume kappa_1 (X,Y) = 0; then
    card Y / card (X \/ Y) = 0 by Kappa1;
    hence thesis;
  end;

theorem Prop4a: :: Proposition 4 a)
  X <> {} implies (kappa_1 (X,Y) = 0 iff Y = {})
  proof
    assume
a3: X <> {};
    thus kappa_1 (X,Y) = 0 implies Y = {} by LemmaProp4a;
    assume
A2: Y = {};
    kappa_1 (X,Y) = card Y / card (X \/ Y) by Kappa1,a3
       .= 0 / card (X \/ Y) by A2;
    hence thesis;
  end;

theorem Prop4b: :: Proposition 4 b)
  kappa_2(X,Y) = 0 iff X = [#]R & Y = {}
  proof
    thus kappa_2(X,Y) = 0 implies X = [#]R & Y = {}
    proof
      assume
ac:   kappa_2(X,Y) = 0; then
      X` = {} & Y = {}; then
      X`` = ({}R)`;
      hence thesis by ac;
    end;
    assume
A2: X = [#]R & Y = {}; then
    X` = ({}R)``;
    hence thesis by A2;
  end;

theorem Prop2b:
  Y c= Z implies kappa_1 (X,Y) <= kappa_1 (X,Z)
  proof
    assume
A0: Y c= Z; then
B3: card Z = card (Y \/ (Z \ Y)) by XBOOLE_1:45
          .= card Y + card (Z \ Y) by XBOOLE_1:79,CARD_2:40;
ZA: card Y <= card (X \/ Y) by NAT_1:43,XBOOLE_1:7;
ZC: X \/ Z = X \/ (Y \/ (Z \ Y)) by A0,XBOOLE_1:45
          .= X \/ Y \/ (Z \ Y) by XBOOLE_1:4;
    per cases;
    suppose
AA:   X \/ Y <> {}; then
      kappa_1 (X,Y) = card Y / card (X \/ Y) by Kappa1; then
ss:   kappa_1 (X,Y) <= (card Y + card (Z \ Y)) /
        (card (X \/ Y) + card (Z \ Y)) by AA,Lemacik,ZA;
      card Z / (card (X \/ Y) + card (Z \ Y)) <=
        card Z / card ((X \/ Y) \/ (Z \ Y)) by CARD_2:43,AA,XREAL_1:118; then
      kappa_1 (X,Y) <= card Z / card ((X \/ Y) \/ (Z \ Y))
        by ss,B3,XXREAL_0:2;
      hence thesis by Kappa1,AA,ZC;
    end;
    suppose
      X = {} & Z = {};
      hence thesis by A0;
    end;
    suppose
T1:   X \/ Y = {} & Z <> {}; then
T3:   X \/ Z <> {} & X = {};
      kappa_1 (X,Z) = card Z / card (X \/ Z) by Kappa1,T1
         .= 1 by XCMPLX_1:60,T3;
      hence thesis by T1,Kappa1;
    end;
  end;

theorem Prop3b:
  Y c= Z implies kappa_2 (X,Y) <= kappa_2 (X,Z)
  proof
    assume Y c= Z; then
    X` \/ Y c= X` \/ Z by XBOOLE_1:9;
    hence thesis by XREAL_1:72,NAT_1:43;
  end;

theorem Lemma2:
  kappa_1 ({}R,X) = 1
proof
  {}R c= X;
  hence thesis by Prop11a;
end;

theorem Lemma3:
  kappa_2 ({}R,X) = 1
proof
  {}R c= X;
  hence thesis by Prop11b;
end;

definition let R be non empty RelStr;
           let f be preRIF of R;
  attr f is satisfying_RIF1 means :RIF1Def:
    for X,Y being Subset of R holds f.(X,Y) = 1 iff X c= Y;
  attr f is satisfying_RIF2 means
    for X,Y,Z being Subset of R st
      Y c= Z holds f.(X,Y) <= f.(X,Z);
  attr f is satisfying_RIF3 means
    for X being Subset of R st
      X <> {} holds f.(X,{}R) = 0;
  attr f is satisfying_RIF4 means
    for X,Y being Subset of R st
      f.(X,Y) = 0 holds X misses Y;
end;

:: Towards weak quasi-RIFs, will be developed later on

definition let R be non empty RelStr;
           let f be preRIF of R;
  attr f is satisfying_RIF0 means
    for X,Y being Subset of R st X c= Y holds f.(X,Y) = 1;
  attr f is satisfying_RIF01 means
    for X,Y being Subset of R st f.(X,Y) = 1 holds X c= Y;
  attr f is satisfying_RIF2* means
    for X,Y,Z being Subset of R st
      f.(Y,Z) = 1 holds f.(X,Y) <= f.(X,Z);
end;

:: rif1 -> (rif2 iff rif2*)
:: qRifs are rif0 and rif2*
:: weak qRIFs are rif0 and rif2

registration let R be non empty RelStr;
  cluster satisfying_RIF1 -> satisfying_RIF0 satisfying_RIF01
    for preRIF of R;
  coherence;
  cluster satisfying_RIF0 satisfying_RIF01 -> satisfying_RIF1
    for preRIF of R;
  coherence;
end;

registration let R be finite Approximation_Space;
  cluster kappa R -> satisfying_RIF1;
  coherence
  proof
    set f = kappa R;
    for X,Y being Subset of R holds f.(X,Y) = 1 iff X c= Y
    proof
      let X,Y be Subset of R;
      thus f.(X,Y) = 1 implies X c= Y
      proof
        assume f.(X,Y) = 1; then
        kappa(X,Y) = 1 by DefKappa;
        hence thesis by Prop1a;
      end;
      assume X c= Y; then
      kappa(X,Y) = 1 by Prop1a;
      hence thesis by DefKappa;
    end;
    hence thesis;
  end;
  cluster kappa R -> satisfying_RIF2;
  coherence
  proof
    set f = kappa R;
    let X,Y,Z be Subset of R;
    assume Y c= Z; then
    kappa (X,Y) <= kappa (X,Z) by Prop1b; then
    f.(X,Y) <= kappa (X,Z) by DefKappa;
    hence thesis by DefKappa;
  end;
  cluster kappa_1 R -> satisfying_RIF1; :: Proposition 3
  coherence
  proof
    set f = kappa_1 R;
    for X,Y being Subset of R holds f.(X,Y) = 1 iff X c= Y
    proof
      let X,Y be Subset of R;
      thus f.(X,Y) = 1 implies X c= Y
      proof
        assume f.(X,Y) = 1; then
        kappa_1 (X,Y) = 1 by DefKappa1;
        hence thesis by Prop11a;
      end;
      assume X c= Y; then
      kappa_1 (X,Y) = 1 by Prop11a;
      hence thesis by DefKappa1;
    end;
    hence thesis;
  end;
  cluster kappa_1 R -> satisfying_RIF2; :: Proposition 3
  coherence
  proof
    set f = kappa_1 R;
    let X,Y,Z be Subset of R;
    assume Y c= Z; then
    kappa_1 (X,Y) <= kappa_1 (X,Z) by Prop2b; then
    f.(X,Y) <= kappa_1 (X,Z) by DefKappa1;
    hence thesis by DefKappa1;
  end;
  cluster kappa_2 R -> satisfying_RIF1; :: Proposition 3
  coherence
  proof
    set f = kappa_2 R;
    for X,Y being Subset of R holds f.(X,Y) = 1 iff X c= Y
    proof
      let X,Y be Subset of R;
      thus f.(X,Y) = 1 implies X c= Y
      proof
        assume f.(X,Y) = 1; then
        kappa_2 (X,Y) = 1 by DefKappa2;
        hence thesis by Prop11b;
      end;
      assume X c= Y; then
      kappa_2 (X,Y) = 1 by Prop11b;
      hence thesis by DefKappa2;
    end;
    hence thesis;
  end;
  cluster kappa_2 R -> satisfying_RIF2; :: Proposition 3
  coherence
  proof
    set f = kappa_2 R;
    let X,Y,Z be Subset of R;
    assume Y c= Z; then
    kappa_2 (X,Y) <= kappa_2 (X,Z) by Prop3b; then
    f.(X,Y) <= kappa_2 (X,Z) by DefKappa2;
    hence thesis by DefKappa2;
  end;
end;

registration let R;
  cluster satisfying_RIF1 satisfying_RIF2 for preRIF of R;
  existence
  proof
    take kappa R;
    thus thesis;
  end;
end;

theorem RIF2Iff:
  for f being satisfying_RIF1 preRIF of R holds
   f is satisfying_RIF2 iff f is satisfying_RIF2*
  proof
    let f be satisfying_RIF1 preRIF of R;
    thus f is satisfying_RIF2 implies f is satisfying_RIF2*
    proof
       assume
A1:    f is satisfying_RIF2;
       let X,Y,Z be Subset of R;
       assume f.(Y,Z) = 1; then
       Y c= Z by RIF1Def;
       hence thesis by A1;
    end;
    assume
A2: f is satisfying_RIF2*;
    let X,Y,Z be Subset of R;
    assume Y c= Z; then
    f.(Y,Z) = 1 by RIF1Def;
    hence thesis by A2;
  end;

registration let R;
  cluster satisfying_RIF2 -> satisfying_RIF2* for
    satisfying_RIF1 preRIF of R;
  coherence by RIF2Iff;
  cluster satisfying_RIF2* -> satisfying_RIF2 for
    satisfying_RIF1 preRIF of R;
  coherence by RIF2Iff;
end;

registration let R;
  cluster kappa R -> satisfying_RIF0 satisfying_RIF2*;
  coherence;
end;

registration let R;
  cluster satisfying_RIF0 satisfying_RIF1 satisfying_RIF2 satisfying_RIF2* for
    preRoughInclusionFunction of R;
  existence
  proof
    take kappa R;
    thus thesis;
  end;
end;

definition let R;
  mode RoughInclusionFunction of R is
   satisfying_RIF1 satisfying_RIF2 preRoughInclusionFunction of R;
end;

definition let R;
  mode quasi-RoughInclusionFunction of R is
   satisfying_RIF0 satisfying_RIF2* preRIF of R;
  mode weak_quasi-RoughInclusionFunction of R is
   satisfying_RIF0 satisfying_RIF2 preRIF of R;
end;

definition let R;
  mode RIF of R is RoughInclusionFunction of R;
  mode qRIF of R is quasi-RoughInclusionFunction of R;
  mode wqRIF of R is weak_quasi-RoughInclusionFunction of R;
end;

begin :: Proposition 2
:: The following three should be obvious (Proposition 3)
::  kappa R is RIF of R;
::  kappa_1 R is RIF of R;
::  kappa_2 R is RIF of R;

theorem :: Proposition 2 a), binary case
  X <> {} & Z \/ W = [#]R & Z misses W implies
    kappa (X,Z) + kappa (X,W) = 1
  proof
    assume
A1: X <> {} & Z \/ W = [#]R & Z misses W;
A3: kappa (X,W) = card (X /\ W) / card X by A1,KappaDef;
A6: X = X /\ (Z \/ W) by A1
     .= X /\ Z \/ X /\ W by XBOOLE_1:23;
A4: card (X /\ Z) + card (X /\ W) = card X by A6,A1,CARD_2:40,XBOOLE_1:76;
    kappa (X,Z) + kappa (X,W) =
         card (X /\ Z) / card X + card (X /\ W) / card X by A1,A3,KappaDef
      .= card X / card X by A4,XCMPLX_1:62;
    hence thesis by XCMPLX_1:60,A1;
  end;

theorem LemmaProp2b: :: Proposition 2 b) from left to right, without X <> {}
  kappa (X,Y) = 0 implies X misses Y
  proof
     assume
A1:  kappa (X,Y) = 0;
     per cases;
     suppose
A2:    X <> {}; then
       kappa (X,Y) = card (X /\ Y) / card X by KappaDef;
       hence thesis by A1,A2;
     end;
     suppose X = {};
       hence thesis;
     end;
   end;

theorem Prop2b: ::: Proposition 2 b)
  X <> {} implies (kappa (X,Y) = 0 iff X misses Y)
  proof
    assume
AA: X <> {};
    thus kappa (X,Y) = 0 implies X misses Y by LemmaProp2b;
    assume X misses Y; then
    card (X /\ Y) / card X = 0;
    hence thesis by AA,KappaDef;
  end;

theorem Prop2c: :: Proposition 2 c)
  X <> {} implies kappa (X,{}R) = 0
  proof
    assume X <> {}; then
    kappa (X,{}R) = card (X /\ {}R) / card X by KappaDef;
    hence thesis;
  end;

theorem :: Proposition 2 d)
  X <> {} & X misses Y implies
    kappa (X, Z \ Y) = kappa (X, Z \/ Y) = kappa (X,Z)
  proof
    assume
A1: X <> {} & X misses Y; then
D1: kappa (X,Y) = 0 by Prop2b;
D3: kappa (X,Z) = kappa (X, (Z /\ Y) \/ (Z \ Y)) by XBOOLE_1:51
               .= kappa (X, Z /\ Y) + kappa (X, Z \ Y)
                   by Prop1e,A1,XBOOLE_1:89;
    kappa (X,Z /\ Y) <= 0 by D1,Prop1b,XBOOLE_1:17; then
D5: kappa (X,Z /\ Y) = 0 by XXREAL_1:1;
e1: kappa (X, Z \/ Y) <= kappa (X,Z) + kappa (X,Y) by Prop1d;
    kappa (X,Z) <= kappa (X, Z \/ Y) by Prop1b,XBOOLE_1:7;
    hence thesis by D5,D3,e1,D1,XXREAL_0:1;
  end;

Test1:
  Z misses W implies kappa (Y \/ Z, W) <= kappa (Y, W)
  proof
    assume
A0: Z misses W;
    per cases;
    suppose
S3: Y /\ W <> {};
A1: Y <> {} by S3;
A3: (Y \/ Z) /\ W = Y /\ W by XBOOLE_1:78,A0;
    card Y <= card (Y \/ Z) by NAT_1:43,XBOOLE_1:7; then
    card (Y /\ W) / card (Y \/ Z) <= card (Y /\ W) / card Y
      by A1,XREAL_1:118; then
    card ((Y \/ Z) /\ W) / card (Y \/ Z) <= kappa (Y, W) by A1,KappaDef,A3;
    hence kappa (Y \/ Z, W) <= kappa (Y, W) by A1,KappaDef;
    end;
    suppose
Z0:   Y /\ W = {} & Y \/ Z <> {} & Y <> {}; then
Z1:   Y misses W; then
      Y \/ Z misses W by A0,XBOOLE_1:70; then
      kappa (Y \/ Z, W) = 0 by Z0,Prop2b;
      hence thesis by Z1,Z0,Prop2b;
    end;
    suppose
Z0:   Y /\ W = {} & Y \/ Z <> {} & Y = {}; then
      kappa (Y \/ Z, W) = 0 by A0,Prop2b;
      hence thesis by Z0,KappaDef;
    end;
    suppose
      Y /\ W = {} & Y \/ Z = {}; then
      Y = {} & Z = {};
      hence thesis;
    end;
  end;

Test2: :: Proposition 2 e)
  Z misses W implies kappa (Y, W) <= kappa (Y \ Z,W)
  proof
    assume
A0: Z misses W;
    per cases;
    suppose
S3: Y /\ W <> {};
A1: Y <> {} by S3;
    per cases;
    suppose
      Y c= Z; then
      kappa (Y \ Z,W) = 1 by KappaDef,XBOOLE_1:37;
      hence thesis by XXREAL_1:1;
    end;
    suppose
b1:   not Y c= Z; then
B1:   Y \ Z <> {} by XBOOLE_1:37;
B2:   (Y \ Z) /\ W = (Y /\ W) \ (Z /\ W) by XBOOLE_1:111
           .= Y /\ W by A0;
      card (Y \ Z) <= card Y by NAT_1:43,XBOOLE_1:36; then
      card (Y /\ W) / card Y <= card (Y /\ W) / card (Y \ Z)
        by XREAL_1:118,B1; then
      kappa (Y,W) <= card ((Y \ Z) /\ W) / card (Y \ Z) by A1,KappaDef,B2;
      hence kappa (Y,W) <= kappa (Y \ Z,W) by KappaDef,b1,XBOOLE_1:37;
    end;
    end;
    suppose
Z0:   Y /\ W = {} & Y \/ Z <> {} & Y <> {}; then
      Y misses W; then
      kappa (Y, W) = 0 by Z0,Prop2b;
      hence thesis by XXREAL_1:1;
    end;
    suppose
      Y /\ W = {} & Y \/ Z <> {} & Y = {};
      hence thesis;
    end;
    suppose
      Y /\ W = {} & Y \/ Z = {}; then
      Y = {} & Z = {};
      hence thesis;
    end;
  end;

theorem :: Proposition 2 e)
  Z misses W implies
    kappa (Y \/ Z, W) <= kappa (Y, W) <= kappa (Y \ Z,W) by Test1,Test2;

Test1AAA:
  Y misses Z & Z c= W implies kappa (Y \/ Z, W) >= kappa (Y, W)
  proof
    assume
A0: Y misses Z & Z c= W;
    per cases;
    suppose
AA:   Y <> {};
      Y /\ W c= Y by XBOOLE_1:17; then
T2:   card (Y /\ W) / card Y <= (card (Y /\ W) + card Z) / (card Y + card Z)
        by Lemacik,AA,NAT_1:43;
T4:   card Y + card Z = card (Y \/ Z) by A0,CARD_2:40;
      Z misses Y /\ W by A0,XBOOLE_1:63,17; then
T3:   card (Y /\ W) + card Z = card ((Y /\ W) \/ Z) by CARD_2:40;
T1:   (Y \/ Z) /\ W = (Y /\ W) \/ (Z /\ W) by XBOOLE_1:23
                   .= (Y /\ W) \/ Z by A0,XBOOLE_1:28;
      kappa (Y,W) <= card ((Y /\ W) \/ Z) / card (Y \/ Z)
        by T4,KappaDef,AA,T2,T3;
      hence thesis by KappaDef,AA,T1;
    end;
    suppose
      Y = {}; then
      kappa (Y \/ Z, W) = 1 by Prop1a,A0;
      hence thesis by XXREAL_1:1;
    end;
    end;

Test2AAA:
  Y misses Z & Z c= W implies kappa (Y, W) >= kappa (Y \ Z, W)
  proof
    assume
A0: Y misses Z & Z c= W;
    per cases;
    suppose
      Y <> {};
      thus thesis by A0,XBOOLE_1:83;
    end;
    suppose
      Y = {};
      hence thesis;
    end;
  end;

theorem :: Proposition 2 f)
  Z misses Y & Z c= W implies
    kappa (Y \ Z, W) <= kappa (Y, W) <= kappa (Y \/ Z,W) by Test1AAA,Test2AAA;

begin :: Proposition 4

registration let R;
  let X be non empty Subset of R;
  cluster kappa (X,{}R) -> empty;
  coherence by Prop2c;
end;

theorem Kappa1RIF4:
  kappa_1 (X,Y) = 0 implies X misses Y
  proof
    assume
A1: kappa_1 (X,Y) = 0;
    per cases;
    suppose X <> {}; then
      Y = {} by A1,Prop4a;
      hence thesis;
    end;
    suppose X = {};
      hence thesis;
    end;
  end;

theorem Kappa2RIF4:
  kappa_2 (X,Y) = 0 implies X misses Y
  proof
    assume kappa_2 (X,Y) = 0; then
    X = [#]R & Y = {} by Prop4b;
    hence thesis;
  end;

registration let R; :: Proposition 4 c)
  cluster kappa R -> satisfying_RIF4;
  coherence
  proof
    let X,Y be Subset of R;
    assume (kappa R).(X,Y) = 0; then
    kappa (X,Y) = 0 by DefKappa;
    hence thesis by LemmaProp2b;
  end;
  cluster kappa_1 R -> satisfying_RIF4;
  coherence
  proof
    let X,Y be Subset of R;
    assume (kappa_1 R).(X,Y) = 0; then
    kappa_1 (X,Y) = 0 by DefKappa1;
    hence thesis by Kappa1RIF4;
  end;
  cluster kappa_2 R -> satisfying_RIF4;
  coherence
  proof
    let X,Y be Subset of R;
    assume (kappa_2 R).(X,Y) = 0; then
    kappa_2 (X,Y) = 0 by DefKappa2;
    hence thesis by Kappa2RIF4;
  end;
end;

theorem :: Proposition 4 d)
  kappa(X,Y) <= kappa_1(X,Y) <= kappa_2(X,Y)
  proof
    per cases;
    suppose
A0:   X <> {}; then
WA:   kappa_1(X,Y) = card Y / card (X \/ Y) by Kappa1;
U1:   card (X /\ Y) <= card X by NAT_1:43,XBOOLE_1:17;
J0:   card Y <= card (X \/ Y) by NAT_1:43,XBOOLE_1:7;
      X \/ Y = X \/ (Y \ X) by XBOOLE_1:39; then
D3:   card (X \/ Y) = card X + card (Y \ X) by CARD_2:40,XBOOLE_1:85;
d4:   Y = (X /\ Y) \/ (Y \ X) by XBOOLE_1:51;
     (X /\ Y) misses (Y \ X) by XBOOLE_1:85,17; then
D4:  card Y = card (X /\ Y) + card (Y \ X) by d4,CARD_2:40;
     (X \/ Y)` = X` /\ Y` by XBOOLE_1:53; then
     (X \/ Y)` \/ Y = (X` \/ Y) /\ (Y` \/ Y) by XBOOLE_1:24
                   .= (X` \/ Y) /\ [#]R by PRE_TOPC:2
                   .= (X` \ Y) \/ Y by XBOOLE_1:39; then
d5:   X` \/ Y = (X` \ Y) \/ Y = (X \/ Y)` \/ Y by XBOOLE_1:39;
      (X \/ Y)` c= Y` by SUBSET_1:12,XBOOLE_1:7; then
      (X \/ Y)` misses Y by XBOOLE_1:63,79; then
D5:   card (X` \/ Y) = card ((X \/ Y)`) + card Y by d5,CARD_2:40;
      card (X /\ Y) / card X <= (card (X /\ Y) + card (Y \ X)) /
         (card X + card (Y \ X)) by Lemacik,A0,U1; then
      kappa (X,Y) <= (card (X /\ Y) + card (Y \ X)) /
        card (X \/ Y) by A0,KappaDef,D3;
      hence kappa(X,Y) <= kappa_1(X,Y) by A0,Kappa1,D4;
      (X \/ Y)` \/ (X \/ Y) = [#]R by PRE_TOPC:2; then
      card ((X \/ Y)`) + card (X \/ Y) = card [#]R by TDLAT_1:2,CARD_2:40;
      hence thesis by D5,A0,J0,Lemacik,WA;
    end;
    suppose
      X = {}; then
b3:   X = {}R; then
      kappa_1(X,Y) = 1 by Lemma2;
      hence thesis by b3,Lemma3,KappaDef;
    end;
  end;

theorem :: Proposition 4 e)
  kappa_1 (X,Y) = kappa (X \/ Y,Y)
  proof
    per cases;
    suppose
A1:   X \/ Y <> {}; then
      kappa (X \/ Y,Y) = card ((X \/ Y) /\ Y) / card (X \/ Y) by KappaDef
         .= card Y / card (X \/ Y) by XBOOLE_1:21;
      hence thesis by A1,Kappa1;
    end;
    suppose
A1:   X = {}; then
AA:   X c= Y;
      kappa (X \/ Y, Y) = 1 by Prop1a,A1;
      hence thesis by Prop11a,AA;
    end;
  end;

LemmaKap1:
  kappa(X,Y) = kappa(X,X /\ Y)
  proof
    per cases;
    suppose
S0:   X <> {}; then
      kappa (X,X /\ Y) = card (X /\ (X /\ Y)) / card X by KappaDef
             .= card (X /\ X /\ Y) / card X by XBOOLE_1:16;
      hence thesis by S0,KappaDef;
    end;
    suppose
S1:   X = {}; then
      kappa (X,Y) = 1 by KappaDef;
      hence thesis by S1,KappaDef;
    end;
  end;

LemmaKap2:
  kappa_1(X,X /\ Y) = kappa_1(X \ Y,X /\ Y)
  proof
    per cases;
    suppose
S0:   X \/ (X /\ Y) <> {}; then
S2:   X <> {};
S3:   kappa_1 (X,X /\ Y) = card (X /\ Y) / card (X \/ (X /\ Y))
        by Kappa1,S0
           .= card (X /\ Y) / card X by XBOOLE_1:22;
      (X \ Y) \/ (X /\ Y) = X by XBOOLE_1:51;
      hence thesis by S3,S2,Kappa1;
    end;
    suppose
S0:   X \/ (X /\ Y) = {}; then
S4:   kappa_1(X,X /\ Y) = 1 by Kappa1;
      (X \ Y) \/ (X /\ Y) = X by XBOOLE_1:51
          .= X \/ (X /\ Y) by XBOOLE_1:22;
      hence thesis by S4,S0,Kappa1;
    end;
  end;

LemmaKap3:
  kappa(X,X /\ Y) = kappa_1(X,X /\ Y)
  proof
    per cases;
    suppose
S0:   X \/ (X /\ Y) <> {}; then
S3:   kappa_1 (X,X /\ Y) = card (X /\ Y) / card (X \/ (X /\ Y))
        by Kappa1
           .= card (X /\ Y) / card X by XBOOLE_1:22;
      X <> {} by S0; then
      kappa(X,X /\ Y) = card (X /\ (X /\ Y)) / card X by KappaDef
             .= card (X /\ X /\ Y) / card X by XBOOLE_1:16;
      hence thesis by S3;
    end;
    suppose
S0:   X \/ (X /\ Y) = {}; then
S3:   kappa_1 (X,X /\ Y) = 1 by Kappa1;
      X = {} by S0;
      hence thesis by S3,KappaDef;
    end;
  end;

Lemma4f1:
  kappa_2 (X,Y) = kappa ([#]R, X` \/ Y)
  proof
    kappa ([#]R, X` \/ Y) = card ([#]R /\ (X` \/ Y)) / card [#]R
      by KappaDef
       .= card (X` \/ Y) / card ([#]R);
    hence thesis;
  end;

Lemma4f2:
  kappa ([#]R, X` \/ Y) = kappa ([#]R,X`) + kappa ([#]R, X /\ Y)
  proof
a0: X` misses X by XBOOLE_1:85;
    X` \/ Y = [#]R /\ (X` \/ Y)
      .= (X` \/ X) /\ (X` \/ Y) by PRE_TOPC:2
      .= X` \/ (X /\ Y) by XBOOLE_1:24; then
A1: card (X` \/ Y) = card (X`) + card (X /\ Y) by a0,CARD_2:40,XBOOLE_1:74;
    kappa ([#]R, X` \/ Y) = card ([#]R /\ (X` \/ Y)) / card [#]R by KappaDef
      .= (card ([#]R /\ X`) / card [#]R) + card (X /\ Y) / card [#]R
          by XCMPLX_1:62,A1
      .= kappa ([#]R,X`) + card (X /\ Y /\ [#]R) / card [#]R by KappaDef
      .= kappa ([#]R,X`) + kappa ([#]R, X /\ Y) by KappaDef;
    hence thesis;
  end;

theorem :: Proposition 4 f)
  kappa_2 (X,Y) = kappa ([#]R, X` \/ Y) =
    kappa ([#]R,X`) + kappa ([#]R, X /\ Y) by Lemma4f1,Lemma4f2;

theorem :: Proposition 4 g)
  kappa(X,Y) = kappa(X,X /\ Y) = kappa_1(X,X /\ Y) = kappa_1(X \ Y,X /\ Y)
    by LemmaKap1,LemmaKap2,LemmaKap3;

theorem :: Proposition 4 h)
  X \/ Y = [#]R implies kappa_1(X,Y) = kappa_2(X,Y)
  proof
    assume
AB: X \/ Y = [#]R;
    X`` \/ Y = [#]R by AB; then
F1: card Y = card (X` \/ Y) by XBOOLE_1:12,LemmaSet;
    per cases;
    suppose
      X \/ Y <> {};
      thus thesis by F1,AB,Kappa1;
    end;
    suppose X \/ Y = {};
      hence thesis by AB;
    end;
  end;

theorem :: false for X = {}!
  X <> {} implies 1 - kappa (X,Y) = kappa (X,Y`)
  proof
    assume
A1: X <> {};
a2: Y \/ ([#]R \ Y) = [#]R by XBOOLE_1:45;
    kappa (X,Y \/ Y`) = kappa (X,Y) + kappa (X,Y`)
      by A1,Prop1e,SUBSET_1:23; then
    kappa (X,Y) + kappa (X,Y`) = 1 by a2,Prop1a;
    hence thesis;
  end;

begin :: An Example of Aproximation Space where all three kappa mappings
:: are distinct -- Example 1 and 2 translated
:: calculations in Mizar seem to be too complex, my propositions are a bit
:: shorter than in the original

definition let X be set;
  func DiscreteApproxSpace X -> strict RelStr equals
    RelStr (# X, id X #);
  coherence;
end;

registration let X be set;
  cluster DiscreteApproxSpace X -> with_equivalence;
  coherence;
end;

registration let X be non empty set;
  cluster DiscreteApproxSpace X -> non empty;
  coherence;
end;

registration let X be finite set;
  cluster DiscreteApproxSpace X -> finite;
  coherence;
end;

definition
  func ExampleRIFSpace -> strict finite Approximation_Space equals
    DiscreteApproxSpace {1,2,3,4,5};
  correctness;
end;

theorem :: Example 1, kappa is not symmetric
  for X,Y being Subset of ExampleRIFSpace
  st X = {1,2} & Y = {2,3,4} holds
    kappa (X,Y) <> kappa (Y,X)
  proof
    let X,Y be Subset of ExampleRIFSpace;
    assume
A1: X = {1,2} & Y = {2,3,4}; then
A3: card Y = 3 by CARD_2:58;
Z1: kappa (Y,X) = card (Y /\ X) / card Y by KappaDef,A1;
    set U = the carrier of ExampleRIFSpace;
    2 in Y & not 1 in Y by A1,ENUMSET1:def 1; then
    X /\ Y = {2} by ZFMISC_1:54,A1; then
A4: card (X /\ Y) = 1 by CARD_1:30;
    kappa (X,Y) = card (X /\ Y) / card X by KappaDef,A1
       .= 1 / 2 by A4,A1,CARD_2:57;
    hence thesis by A3,Z1,A4;
  end;

theorem :: Example 1, kappa is not monotone wrt 1st coordinate
  for X,Y,U being Subset of ExampleRIFSpace
  st X = {1,2} & Y = {1,2,3} & U = {2,4,5} holds
    not kappa (X,U) <= kappa (Y,U)
  proof
    let X,Y,U be Subset of ExampleRIFSpace;
    assume
A1: X = {1,2} & Y = {1,2,3} & U = {2,4,5}; then
A3: card Y = 3 by CARD_2:58;
    2 in U & not 1 in U by A1,ENUMSET1:def 1; then
    X /\ U = {2} by A1,ZFMISC_1:54; then
R1: card (X /\ U) = 1 by CARD_1:30;
R2: card X = 2 by CARD_2:57,A1;
R0: U = {2} \/ {4,5} by A1,ENUMSET1:2;
ro: 2 in Y by A1,ENUMSET1:def 1;
w1: not 4 in Y by A1,ENUMSET1:def 1;
    not 5 in Y by A1,ENUMSET1:def 1; then
rr: Y misses {4,5} by ZFMISC_1:51,w1;
    Y /\ U = Y /\ {2} \/ (Y /\ {4,5}) by R0,XBOOLE_1:23
      .= Y /\ {2} by rr; then
    Y /\ U = {2} by XBOOLE_1:28,ro,ZFMISC_1:31; then
R3: card (Y /\ U) = 1 by CARD_1:30;
W4: kappa (X,U) = 1 / 2 by R1,R2,A1,KappaDef;
    kappa (Y,U) = 1 / 3 by A3,R3,A1,KappaDef;
    hence thesis by W4;
  end;

theorem :: Example 2, simplified: all three RIFs are different
  for X,Y being Subset of ExampleRIFSpace
  st X = {1,2} & Y = {2,3,4} holds
    kappa (X,Y), kappa_1 (X,Y), kappa_2 (X,Y) are_mutually_distinct
  proof
    let X,Y be Subset of ExampleRIFSpace;
    assume
A1: X = {1,2} & Y = {2,3,4}; then
A3: card Y = 3 by CARD_2:58;
    set U = the carrier of ExampleRIFSpace;
    1,2,3,4,5 are_mutually_distinct by ZFMISC_1:def 7; then
a1: card U = 5 by CARD_2:63;
    2 in Y & not 1 in Y by A1,ENUMSET1:def 1; then
    X /\ Y = {2} by ZFMISC_1:54,A1; then
A4: card (X /\ Y) = 1 by CARD_1:30;
a5: X \/ Y = {1,2} \/ ({2} \/ {3,4}) by A1,ENUMSET1:2
      .= {1,2} \/ {2} \/ {3,4} by XBOOLE_1:4
      .= {1,2} \/ {3,4} by ZFMISC_1:9
      .= {1,2,3,4} by ENUMSET1:5;
    not 1 in {3,4,5} & not 2 in {3,4,5} by ENUMSET1:def 1; then
W2: {1,2} misses {3,4,5} by ZFMISC_1:51;
WW: 3 in {3,4,5} & 4 in {3,4,5} by ENUMSET1:def 1;
    X` = {1,2} \/ {3,4,5} \ {1,2} by A1,ENUMSET1:8
      .= {3,4,5} by XBOOLE_1:88,W2; then
    X` \/ Y = {3,4,5} \/ ({2} \/ {3,4}) by A1,ENUMSET1:2
           .= {2} \/ ({3,4} \/ {3,4,5}) by XBOOLE_1:4
           .= {2} \/ {3,4,5} by ZFMISC_1:42,WW; then
    X` \/ Y = {2,3,4,5} by ENUMSET1:4; then
W3: card (X` \/ Y) / card U = 4 / 5 by a1,CARD_2:59;
W4: kappa (X,Y) = card (X /\ Y) / card X by KappaDef,A1
       .= 1 / 2 by A4,A1,CARD_2:57;
    kappa_1 (X,Y) = card Y / card (X \/ Y) by Kappa1,A1
       .= 3 / 4 by A3,a5,CARD_2:59;
    hence thesis by ZFMISC_1:def 5,W4,W3;
  end;

begin :: Continuing Formalization of Theorem 4.1 from Anna Gomolinska's
:: A Comparative Study of Some Generalized Rough Approximations"
:: Fundamenta Informaticae, 51(2002), pp. 103-119

theorem ::: Theorem 4.1 c) from Gomolinska's "A Comparative Study..."
  for R being finite Approximation_Space,
      u being Element of R,
      x,y being Subset of R st
   u in (f_1 R).x & (UncertaintyMap R).u = y
    holds kappa (y, x) > 0
  proof
    let R be finite Approximation_Space,
        u be Element of R,
        x,y be Subset of R;
    assume
AA: u in (f_1 R).x & (UncertaintyMap R).u = y;
    (f_1 R).x = { u where u is Element of R :
       (UncertaintyMap R).u meets x } by ROUGHS_5:def 5; then
    consider uu being Element of R such that
AB: uu = u & (UncertaintyMap R).uu meets x by AA;
    kappa (y,x) <> 0 by AB,AA,LemmaProp2b;
    hence thesis by XXREAL_1:1;
  end;

theorem  ::: Theorem 4.1 d) from Gomolinska's "A Comparative Study..."
  for R being finite Approximation_Space,
      u being Element of R,
      x,y being Subset of R st
   u in (Flip f_1 R).x & (UncertaintyMap R).u = y
    holds kappa (y, x) = 1
  proof
    let R be finite Approximation_Space,
        u be Element of R,
        x,y be Subset of R;
    assume
A0: u in (Flip f_1 R).x & (UncertaintyMap R).u = y;
    (Flip f_1 R).x = { w where w is Element of R :
       (UncertaintyMap R).w c= x } by ROUGHS_5:30; then
    consider v being Element of R such that
A3: u = v & (UncertaintyMap R).v c= x by A0;
    thus thesis by Prop1a,A0,A3;
  end;