roughif1.miz



    begin

    theorem :: ROUGHIF1:1

    

     Lemacik: for a,b,c be 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 :: ROUGHIF1:2

    

     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 :: ROUGHIF1:3

    

     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 :: ROUGHIF1:4

    

     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

    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;

      :: ROUGHIF1:def1

      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 :: ROUGHIF1:5

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

    theorem :: ROUGHIF1:6

    

     Prop1a: ( 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 :: ROUGHIF1:7

    

     Prop1b: 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 :: ROUGHIF1:8

    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 :: ROUGHIF1:9

    

     Prop1d: ( 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 :: ROUGHIF1:10

    

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

    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 :: ROUGHIF1:sch1

    BinOpEq { R() -> non empty 1-sorted , F( Subset of R(), Subset of R()) -> Element of [. 0 , 1.] } :

for f1,f2 be preRIF of R() st (for x,y be Subset of R() holds (f1 . (x,y)) = F(x,y)) & (for x,y be Subset of R() holds (f2 . (x,y)) = F(x,y)) holds f1 = f2;

      let f1,f2 be preRIF of R() such that

       A1: (for x,y be Subset of R() holds (f1 . (x,y)) = F(x,y)) and

       A2: (for x,y be Subset of R() holds (f2 . (x,y)) = F(x,y));

      for x,y be 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;

      :: ROUGHIF1:def2

      func kappa R -> preRIF of R means

      : DefKappa: for x,y be 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 be preRIF of R st for x,y be Element of ( bool the carrier of R) holds (f . (x,y)) = F(x,y) from BINOP_1:sch 4;

        then

        consider f be Function of [:( bool the carrier of R), ( bool the carrier of R):], [. 0 , 1.] such that

         A1: for x,y be 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 be preRIF of R st (for x,y be Subset of R holds (f1 . (x,y)) = F(x,y)) & (for x,y be Subset of R holds (f2 . (x,y)) = F(x,y)) holds f1 = f2 from BinOpEq;

        hence thesis;

      end;

    end

    begin

    definition

      let R be finite Approximation_Space;

      let X,Y be Subset of R;

      :: ROUGHIF1:def3

      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 ;

      :: ROUGHIF1:def4

      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;

      :: ROUGHIF1:def5

      func kappa_1 R -> preRIF of R means

      : DefKappa1: for x,y be 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 be Function of [:( bool the carrier of R), ( bool the carrier of R):], [. 0 , 1.] st for x,y be Element of ( bool the carrier of R) holds (f . (x,y)) = F(x,y) from BINOP_1:sch 4;

        then

        consider f be Function of [:( bool the carrier of R), ( bool the carrier of R):], [. 0 , 1.] such that

         A1: for x,y be 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 be Function of [:( bool the carrier of R), ( bool the carrier of R):], [. 0 , 1.] st (for x,y be Subset of R holds (f1 . (x,y)) = F(x,y)) & (for x,y be Subset of R holds (f2 . (x,y)) = F(x,y)) holds f1 = f2 from BinOpEq;

        hence thesis;

      end;

      :: ROUGHIF1:def6

      func kappa_2 R -> preRIF of R means

      : DefKappa2: for x,y be 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 be Function of [:( bool the carrier of R), ( bool the carrier of R):], [. 0 , 1.] st for x,y be Element of ( bool the carrier of R) holds (f . (x,y)) = F(x,y) from BINOP_1:sch 4;

        then

        consider f be Function of [:( bool the carrier of R), ( bool the carrier of R):], [. 0 , 1.] such that

         A1: for x,y be 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 be Function of [:( bool the carrier of R), ( bool the carrier of R):], [. 0 , 1.] st (for x,y be Subset of R holds (f1 . (x,y)) = F(x,y)) & (for x,y be Subset of R holds (f2 . (x,y)) = F(x,y)) holds f1 = f2 from BinOpEq;

        hence thesis;

      end;

    end

    theorem :: ROUGHIF1:11

    

     Prop11a: ( 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 :: ROUGHIF1:12

    

     Prop11b: ( 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 :: ROUGHIF1:13

    

     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 :: ROUGHIF1:14

    

     Prop4a: 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 :: ROUGHIF1:15

    

     Prop4b: ( 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 :: ROUGHIF1:16

    

     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 :: ROUGHIF1:17

    

     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 :: ROUGHIF1:18

    

     Lemma2: ( kappa_1 (( {} R),X)) = 1

    proof

      ( {} R) c= X;

      hence thesis by Prop11a;

    end;

    theorem :: ROUGHIF1:19

    

     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;

      :: ROUGHIF1:def7

      attr f is satisfying_RIF1 means

      : RIF1Def: for X,Y be Subset of R holds (f . (X,Y)) = 1 iff X c= Y;

      :: ROUGHIF1:def8

      attr f is satisfying_RIF2 means for X,Y,Z be Subset of R st Y c= Z holds (f . (X,Y)) <= (f . (X,Z));

      :: ROUGHIF1:def9

      attr f is satisfying_RIF3 means for X be Subset of R st X <> {} holds (f . (X,( {} R))) = 0 ;

      :: ROUGHIF1:def10

      attr f is satisfying_RIF4 means for X,Y be Subset of R st (f . (X,Y)) = 0 holds X misses Y;

    end

    definition

      let R be non empty RelStr;

      let f be preRIF of R;

      :: ROUGHIF1:def11

      attr f is satisfying_RIF0 means for X,Y be Subset of R st X c= Y holds (f . (X,Y)) = 1;

      :: ROUGHIF1:def12

      attr f is satisfying_RIF01 means for X,Y be Subset of R st (f . (X,Y)) = 1 holds X c= Y;

      :: ROUGHIF1:def13

      attr f is satisfying_RIF2* means for X,Y,Z be Subset of R st (f . (Y,Z)) = 1 holds (f . (X,Y)) <= (f . (X,Z));

    end

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

      coherence

      proof

        set f = ( kappa_1 R);

        for X,Y be 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;

      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;

      coherence

      proof

        set f = ( kappa_2 R);

        for X,Y be 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;

      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 :: ROUGHIF1:20

    

     RIF2Iff: for f be 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

    theorem :: ROUGHIF1:21

    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 :: ROUGHIF1:22

    

     LemmaProp2b: ( 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 :: ROUGHIF1:23

    

     Prop2b: 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 :: ROUGHIF1:24

    

     Prop2c: X <> {} implies ( kappa (X,( {} R))) = 0

    proof

      assume X <> {} ;

      then ( kappa (X,( {} R))) = (( card (X /\ ( {} R))) / ( card X)) by KappaDef;

      hence thesis;

    end;

    theorem :: ROUGHIF1:25

    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: 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 :: ROUGHIF1:26

    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, XBOOLE_1: 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 :: ROUGHIF1:27

    Z misses Y & Z c= W implies ( kappa ((Y \ Z),W)) <= ( kappa (Y,W)) <= ( kappa ((Y \/ Z),W)) by Test1AAA, Test2AAA;

    begin

    registration

      let R;

      let X be non empty Subset of R;

      cluster ( kappa (X,( {} R))) -> empty;

      coherence by Prop2c;

    end

    theorem :: ROUGHIF1:28

    

     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 :: ROUGHIF1:29

    

     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;

      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 :: ROUGHIF1:30

    ( 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, XBOOLE_1: 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, XBOOLE_1: 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 :: ROUGHIF1:31

    ( 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 :: ROUGHIF1:32

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

    theorem :: ROUGHIF1:33

    ( kappa (X,Y)) = ( kappa (X,(X /\ Y))) = ( kappa_1 (X,(X /\ Y))) = ( kappa_1 ((X \ Y),(X /\ Y))) by LemmaKap1, LemmaKap2, LemmaKap3;

    theorem :: ROUGHIF1:34

    (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 :: ROUGHIF1:35

    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

    definition

      let X be set;

      :: ROUGHIF1:def14

      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

      :: ROUGHIF1:def15

      func ExampleRIFSpace -> strict finite Approximation_Space equals ( DiscreteApproxSpace {1, 2, 3, 4, 5});

      correctness ;

    end

    theorem :: ROUGHIF1:36

    for X,Y be 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 :: ROUGHIF1:37

    for X,Y,U be 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 :: ROUGHIF1:38

    for X,Y be 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

    theorem :: ROUGHIF1:39

    for R be finite Approximation_Space, u be Element of R, x,y be 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 be Element of R : (( UncertaintyMap R) . u) meets x } by ROUGHS_5:def 5;

      then

      consider uu be 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 :: ROUGHIF1:40

    for R be finite Approximation_Space, u be Element of R, x,y be 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 be Element of R : (( UncertaintyMap R) . w) c= x } by ROUGHS_5: 30;

      then

      consider v be Element of R such that

       A3: u = v & (( UncertaintyMap R) . v) c= x by A0;

      thus thesis by Prop1a, A0, A3;

    end;