roughif2.miz



    begin

    theorem :: ROUGHIF2:1

    

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

    theorem :: ROUGHIF2:2

    for x1,x2 be finite set holds ( card (x1 \+\ x2)) = (( card (x1 \ x2)) + ( card (x2 \ x1))) by CARD_2: 40, XBOOLE_1: 82;

    theorem :: ROUGHIF2:3

    

     HoHo: for x1,x2 be finite set holds ((2 * ( card (x1 \+\ x2))) / ((( card x1) + ( card x2)) + ( card (x1 \+\ x2)))) = (( card (x1 \+\ x2)) / ( card (x1 \/ x2)))

    proof

      let x1,x2 be finite set;

      set p = ( card (x1 \/ x2));

      set q = ((( card x1) + ( card x2)) + ( card (x1 \+\ x2)));

      set r = ( card (x1 \+\ x2));

      (x1 \/ x2) = (x1 \/ (x2 \ x1)) by XBOOLE_1: 39;

      then

       HH: p = (( card x1) + ( card (x2 \ x1))) by XBOOLE_1: 79, CARD_2: 40;

      x1 = ((x1 \ x2) \/ (x1 /\ x2)) by XBOOLE_1: 51;

      then

       g1: ( card x1) = (( card (x1 \ x2)) + ( card (x1 /\ x2))) by CARD_2: 40, XBOOLE_1: 89;

      x2 = ((x2 \ x1) \/ (x1 /\ x2)) by XBOOLE_1: 51;

      then

       g2: ( card x2) = (( card (x2 \ x1)) + ( card (x1 /\ x2))) by CARD_2: 40, XBOOLE_1: 89;

      q = (((( card (x1 \ x2)) + ( card (x1 /\ x2))) + (( card (x2 \ x1)) + ( card (x1 /\ x2)))) + (( card (x1 \ x2)) + ( card (x2 \ x1)))) by CARD_2: 40, XBOOLE_1: 82, g1, g2

      .= (2 * p) by g1, HH;

      hence thesis by XCMPLX_1: 91;

    end;

    theorem :: ROUGHIF2:4

    

     Jajo: for A,B,C be set holds (A \+\ C) = ((A \+\ B) \+\ (B \+\ C))

    proof

      let A,B,C be set;

      ((A \+\ B) \+\ B) = (A \+\ (B \+\ B)) by XBOOLE_1: 91

      .= (A \+\ {} ) by XBOOLE_1: 92

      .= A;

      hence thesis by XBOOLE_1: 91;

    end;

    theorem :: ROUGHIF2:5

    

     Lemacik: for A,B be finite set st (A \/ B) <> {} holds (1 - (( card (A /\ B)) / ( card (A \/ B)))) = (( card (A \+\ B)) / ( card (A \/ B)))

    proof

      let A,B be finite set;

      assume

       A1: (A \/ B) <> {} ;

      

       B1: (A /\ B) c= A by XBOOLE_1: 17;

      A c= (A \/ B) by XBOOLE_1: 7;

      then

       B2: (A /\ B) c= (A \/ B) by B1;

      (A \+\ B) = ((A \/ B) \ (A /\ B)) by XBOOLE_1: 101;

      then

       B3: ( card (A \+\ B)) = (( card (A \/ B)) - ( card (A /\ B))) by CARD_2: 44, B2;

      (1 - (( card (A /\ B)) / ( card (A \/ B)))) = ((( card (A \/ B)) / ( card (A \/ B))) - (( card (A /\ B)) / ( card (A \/ B)))) by A1, XCMPLX_1: 60

      .= (( card (A \+\ B)) / ( card (A \/ B))) by B3, XCMPLX_1: 120;

      hence thesis;

    end;

    theorem :: ROUGHIF2:6

    

     LemmaCard: for R be finite set holds for X,Y be Subset of R holds ( card (X \/ Y)) = ( card (X /\ Y)) iff X = Y

    proof

      let R be finite set;

      let X,Y be Subset of R;

      hereby

        assume ( card (X \/ Y)) = ( card (X /\ Y));

        then

         A2: (X /\ Y) = (X \/ Y) by CARD_2: 102, XBOOLE_1: 29;

        then X = (X \/ (X \/ Y)) by XBOOLE_1: 22;

        then X = (X \/ Y) by XBOOLE_1: 6;

        hence X = Y by XBOOLE_1: 21, A2;

      end;

      assume X = Y;

      hence thesis;

    end;

    registration

      cluster finite non empty for MetrSpace;

      existence

      proof

        set A = {1};

        take S = ( DiscreteSpace A);

        S = MetrStruct (# A, ( discrete_dist A) #) by METRIC_1:def 11;

        hence thesis;

      end;

    end

    begin

    reserve R for finite Approximation_Space;

    reserve X,Y,Z for Subset of R;

    definition

      let R be finite Approximation_Space;

      let f be preRIF of R;

      :: ROUGHIF2:def1

      func CMap f -> preRIF of R means

      : CDef: for x,y be Subset of R holds (it . (x,y)) = (1 - (f . (x,y)));

      existence

      proof

        deffunc F( Subset of R, Subset of R) = ( In ((1 - (f . ($1,$2))), [. 0 , 1.]));

        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 ff 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 (ff . (x,y)) = F(x,y);

        take ff;

        let x,y be Subset of R;

        (ff . (x,y)) = ( In ((1 - (f . (x,y))), [. 0 , 1.])) by A1

        .= (1 - (f . (x,y))) by FUZNORM1: 7, SUBSET_1:def 8;

        hence thesis;

      end;

      uniqueness

      proof

        deffunc G( Subset of R, Subset of R) = (1 - (f . ($1,$2)));

        let f1,f2 be preRIF of R such that

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

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

        for x,y be Subset of R holds (f1 . (x,y)) = (f2 . (x,y))

        proof

          let x,y be Subset of R;

          (f1 . (x,y)) = G(x,y) by A1

          .= (f2 . (x,y)) by A2;

          hence thesis;

        end;

        hence thesis by BINOP_1: 2;

      end;

    end

    theorem :: ROUGHIF2:7

    

     CMapMap: for f be preRIF of R holds ( CMap ( CMap f)) = f

    proof

      let f be preRIF of R;

      set g = ( CMap f);

      for x be Element of [:( bool the carrier of R), ( bool the carrier of R):] holds (( CMap g) . x) = (f . x)

      proof

        let x be Element of [:( bool the carrier of R), ( bool the carrier of R):];

        reconsider x1 = (x `1 ), x2 = (x `2 ) as Subset of R;

        (( CMap g) . x) = (( CMap g) . (x1,x2)) by MCART_1: 21

        .= (1 - (g . (x1,x2))) by CDef

        .= (1 - (1 - (f . (x1,x2)))) by CDef

        .= (f . x) by MCART_1: 21;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: ROUGHIF2:8

    

     PropEx3k: X <> {} implies (( CMap ( kappa R)) . (X,Y)) = (( card (X \ Y)) / ( card X))

    proof

      assume

       A1: X <> {} ;

      (X \ Y) = (X \ (X /\ Y)) by XBOOLE_1: 47;

      then

       T1: ( card (X \ Y)) = (( card X) - ( card (X /\ Y))) by XBOOLE_1: 17, CARD_2: 44;

      (( CMap ( kappa R)) . (X,Y)) = (1 - (( kappa R) . (X,Y))) by CDef

      .= (1 - ( kappa (X,Y))) by ROUGHIF1:def 2

      .= (1 - (( card (X /\ Y)) / ( card X))) by A1, ROUGHIF1:def 1

      .= ((( card X) / ( card X)) - (( card (X /\ Y)) / ( card X))) by A1, XCMPLX_1: 60

      .= (( card (X \ Y)) / ( card X)) by T1, XCMPLX_1: 120;

      hence thesis;

    end;

    theorem :: ROUGHIF2:9

    

     PropEx3k0: X = {} implies (( CMap ( kappa R)) . (X,Y)) = 0

    proof

      assume

       A1: X = {} ;

      

       G1: ( kappa (X,Y)) = 1 by ROUGHIF1: 6, A1, XBOOLE_1: 2;

      (( CMap ( kappa R)) . (X,Y)) = (1 - (( kappa R) . (X,Y))) by CDef

      .= (1 - ( kappa (X,Y))) by ROUGHIF1:def 2

      .= 0 by G1;

      hence thesis;

    end;

    theorem :: ROUGHIF2:10

    X <> {} implies (( CMap ( kappa R)) . (X,Y)) = ( kappa (X,(Y ` )))

    proof

      assume

       A0: X <> {} ;

      (( CMap ( kappa R)) . (X,Y)) = (1 - (( kappa R) . (X,Y))) by CDef

      .= (1 - ( kappa (X,Y))) by ROUGHIF1:def 2;

      hence thesis by A0, ROUGHIF1: 35;

    end;

    theorem :: ROUGHIF2:11

    

     PropEx3: (X \/ Y) <> {} implies (( CMap ( kappa_1 R)) . (X,Y)) = (( card (X \ Y)) / ( card (X \/ Y)))

    proof

      assume

       A0: (X \/ Y) <> {} ;

      

       A1: (( CMap ( kappa_1 R)) . (X,Y)) = (1 - (( kappa_1 R) . (X,Y))) by CDef

      .= (1 - ( kappa_1 (X,Y))) by ROUGHIF1:def 5;

      (X \ Y) = ((X \/ Y) \ Y) by XBOOLE_1: 40;

      then

       X1: ( card (X \ Y)) = (( card (X \/ Y)) - ( card Y)) by CARD_2: 44, XBOOLE_1: 7;

      (1 - (( card Y) / ( card (X \/ Y)))) = ((( card (X \/ Y)) / ( card (X \/ Y))) - (( card Y) / ( card (X \/ Y)))) by A0, XCMPLX_1: 60

      .= (( card (X \ Y)) / ( card (X \/ Y))) by X1, XCMPLX_1: 120;

      hence thesis by A1, A0, ROUGHIF1:def 3;

    end;

    theorem :: ROUGHIF2:12

    

     PropEx30: (X \/ Y) = {} implies (( CMap ( kappa_1 R)) . (X,Y)) = 0

    proof

      assume

       AA: (X \/ Y) = {} ;

      

       A1: (( kappa_1 R) . (X,Y)) = ( kappa_1 (X,Y)) by ROUGHIF1:def 5

      .= 1 by AA, ROUGHIF1:def 3;

      (( CMap ( kappa_1 R)) . (X,Y)) = (1 - (( kappa_1 R) . (X,Y))) by CDef

      .= 0 by A1;

      hence thesis;

    end;

    theorem :: ROUGHIF2:13

    

     PropEx31: (( CMap ( kappa_2 R)) . (X,Y)) = (( card (X \ Y)) / ( card ( [#] R)))

    proof

      (((X ` ) \/ Y) ` ) = (((X \ Y) ` ) ` ) by SUBSET_1: 14;

      then

       A3: (( card ( [#] R)) - ( card ((X ` ) \/ Y))) = ( card (X \ Y)) by CARD_2: 44;

      (( CMap ( kappa_2 R)) . (X,Y)) = (1 - (( kappa_2 R) . (X,Y))) by CDef

      .= (1 - ( kappa_2 (X,Y))) by ROUGHIF1:def 6

      .= ((( card ( [#] R)) / ( card ( [#] R))) - (( card ((X ` ) \/ Y)) / ( card ( [#] R)))) by XCMPLX_1: 60

      .= (( card (X \ Y)) / ( card ( [#] R))) by A3, XCMPLX_1: 120;

      hence thesis;

    end;

    

     Lemma1: X <> {} implies ( kappa (X,Y)) = ((( CMap ( kappa_1 R)) . (X,(Y ` ))) / ( kappa_1 ((Y ` ),X)))

    proof

      assume

       A0: X <> {} ;

      

       c1: (X \ (Y ` )) = (X /\ ((Y ` ) ` )) by SUBSET_1: 13;

      

       A2: (( CMap ( kappa_1 R)) . (X,(Y ` ))) = (( card (X \ (Y ` ))) / ( card (X \/ (Y ` )))) by A0, PropEx3;

      ( kappa_1 ((Y ` ),X)) = (( card X) / ( card ((Y ` ) \/ X))) by A0, ROUGHIF1:def 3;

      

      then ((( CMap ( kappa_1 R)) . (X,(Y ` ))) / ( kappa_1 ((Y ` ),X))) = (( card (X \ (Y ` ))) / ( card X)) by A0, XCMPLX_1: 55, A2

      .= ( kappa (X,Y)) by A0, ROUGHIF1:def 1, c1;

      hence thesis;

    end;

    

     Lemma2: X <> {} implies ( kappa (X,Y)) = ((( CMap ( kappa_2 R)) . (X,(Y ` ))) / ( kappa_2 (( [#] R),X)))

    proof

      assume

       a1: X <> {} ;

      

       VV: (X /\ ((Y ` ) ` )) = (X \ (Y ` )) by SUBSET_1: 13;

      ((( CMap ( kappa_2 R)) . (X,(Y ` ))) / ( kappa_2 (( [#] R),X))) = ((( card (X \ (Y ` ))) / ( card ( [#] R))) / (( card ((( [#] R) ` ) \/ X)) / ( card ( [#] R)))) by PropEx31

      .= (( card (X \ (Y ` ))) / ( card (((( {} R) ` ) ` ) \/ X))) by XCMPLX_1: 55

      .= ( kappa (X,Y)) by ROUGHIF1:def 1, a1, VV;

      hence thesis;

    end;

    theorem :: ROUGHIF2:14

    X <> {} implies ( kappa (X,Y)) = ((( CMap ( kappa_1 R)) . (X,(Y ` ))) / ( kappa_1 ((Y ` ),X))) = ((( CMap ( kappa_2 R)) . (X,(Y ` ))) / ( kappa_2 (( [#] R),X)))

    proof

      assume

       A0: X <> {} ;

      then ( kappa (X,Y)) = ((( CMap ( kappa_1 R)) . (X,(Y ` ))) / ( kappa_1 ((Y ` ),X))) by Lemma1;

      hence thesis by A0, Lemma2;

    end;

    begin

    definition

      let R;

      let f be preRIF of R;

      :: ROUGHIF2:def2

      attr f is co-RIF-like means ( CMap f) is RIF of R;

    end

    registration

      let R;

      let f be RIF of R;

      cluster ( CMap f) -> co-RIF-like;

      coherence by CMapMap;

    end

    registration

      let R;

      cluster co-RIF-like for preRIF of R;

      existence

      proof

        take ( CMap ( kappa R));

        thus thesis;

      end;

    end

    definition

      let R;

      mode co-RIF of R is co-RIF-like preRIF of R;

    end

    begin

    reserve kap for RIF of R;

    theorem :: ROUGHIF2:15

    

     Prop6a: (( CMap kap) . (X,Y)) = 0 iff X c= Y

    proof

      thus (( CMap kap) . (X,Y)) = 0 implies X c= Y

      proof

        assume (( CMap kap) . (X,Y)) = 0 ;

        then (1 - (kap . (X,Y))) = 0 by CDef;

        hence thesis by ROUGHIF1:def 7;

      end;

      assume X c= Y;

      then

       A1: (kap . (X,Y)) = 1 by ROUGHIF1:def 7;

      (( CMap kap) . (X,Y)) = (1 - 1) by A1, CDef;

      hence thesis;

    end;

    theorem :: ROUGHIF2:16

    (( CMap ( kappa R)) . (X,Y)) = 0 iff X c= Y

    proof

      thus (( CMap ( kappa R)) . (X,Y)) = 0 implies X c= Y

      proof

        assume (( CMap ( kappa R)) . (X,Y)) = 0 ;

        then (1 - (( kappa R) . (X,Y))) = 0 by CDef;

        then ( kappa (X,Y)) = 1 by ROUGHIF1:def 2;

        hence thesis by ROUGHIF1: 6;

      end;

      assume X c= Y;

      then

       A1: ( kappa (X,Y)) = 1 by ROUGHIF1: 6;

      (( CMap ( kappa R)) . (X,Y)) = (1 - (( kappa R) . (X,Y))) by CDef

      .= (1 - 1) by A1, ROUGHIF1:def 2;

      hence thesis;

    end;

    theorem :: ROUGHIF2:17

    Y c= Z implies (( CMap kap) . (X,Z)) <= (( CMap kap) . (X,Y))

    proof

      assume Y c= Z;

      then (1 - (kap . (X,Y))) >= (1 - (kap . (X,Z))) by XREAL_1: 10, ROUGHIF1:def 8;

      then (( CMap kap) . (X,Y)) >= (1 - (kap . (X,Z))) by CDef;

      hence thesis by CDef;

    end;

    theorem :: ROUGHIF2:18

    Y c= Z implies (( CMap ( kappa R)) . (X,Z)) <= (( CMap ( kappa R)) . (X,Y))

    proof

      assume Y c= Z;

      then (1 - ( kappa (X,Y))) >= (1 - ( kappa (X,Z))) by XREAL_1: 10, ROUGHIF1: 7;

      then (1 - (( kappa R) . (X,Y))) >= (1 - ( kappa (X,Z))) by ROUGHIF1:def 2;

      then (1 - (( kappa R) . (X,Y))) >= (1 - (( kappa R) . (X,Z))) by ROUGHIF1:def 2;

      then (( CMap ( kappa R)) . (X,Y)) >= (1 - (( kappa R) . (X,Z))) by CDef;

      hence thesis by CDef;

    end;

    

     Lemma6c1: (( CMap ( kappa_2 R)) . (X,Y)) <= (( CMap ( kappa_1 R)) . (X,Y))

    proof

      ( kappa_1 (X,Y)) <= ( kappa_2 (X,Y)) by ROUGHIF1: 30;

      then (( kappa_1 R) . (X,Y)) <= ( kappa_2 (X,Y)) by ROUGHIF1:def 5;

      then (( kappa_1 R) . (X,Y)) <= (( kappa_2 R) . (X,Y)) by ROUGHIF1:def 6;

      then (1 - (( kappa_1 R) . (X,Y))) >= (1 - (( kappa_2 R) . (X,Y))) by XREAL_1: 10;

      then (( CMap ( kappa_1 R)) . (X,Y)) >= (1 - (( kappa_2 R) . (X,Y))) by CDef;

      hence thesis by CDef;

    end;

    

     Lemma6c2: (( CMap ( kappa_1 R)) . (X,Y)) <= (( CMap ( kappa R)) . (X,Y))

    proof

      ( kappa (X,Y)) <= ( kappa_1 (X,Y)) by ROUGHIF1: 30;

      then (( kappa R) . (X,Y)) <= ( kappa_1 (X,Y)) by ROUGHIF1:def 2;

      then (( kappa R) . (X,Y)) <= (( kappa_1 R) . (X,Y)) by ROUGHIF1:def 5;

      then (1 - (( kappa R) . (X,Y))) >= (1 - (( kappa_1 R) . (X,Y))) by XREAL_1: 10;

      then (( CMap ( kappa R)) . (X,Y)) >= (1 - (( kappa_1 R) . (X,Y))) by CDef;

      hence thesis by CDef;

    end;

    theorem :: ROUGHIF2:19

    (( CMap ( kappa_2 R)) . (X,Y)) <= (( CMap ( kappa_1 R)) . (X,Y)) <= (( CMap ( kappa R)) . (X,Y)) by Lemma6c1, Lemma6c2;

    theorem :: ROUGHIF2:20

    

     LemacikX: for a,b,c be Real st a <= b & b > 0 & c >= 0 & b > c holds (a / b) >= ((a - c) / (b - c))

    proof

      let a,b,c be Real;

      assume

       A1: a <= b & b > 0 & c >= 0 & b > c;

      then (b - 0 ) > c;

      then

       SS: (b - c) > 0 by XREAL_1: 12;

      (a * c) <= (b * c) by A1, XREAL_1: 64;

      then ((a * b) - (a * c)) >= ((a * b) - (b * c)) by XREAL_1: 10;

      then (a * (b - c)) >= (b * (a - c));

      hence thesis by XREAL_1: 102, A1, SS;

    end;

    

     Jaga1: X <> {} & Y <> {} & Z <> {} implies ((( CMap ( kappa_1 R)) . (X,Y)) + (( CMap ( kappa_1 R)) . (Y,Z))) >= (( CMap ( kappa_1 R)) . (X,Z))

    proof

      assume

       ZZ: X <> {} & Y <> {} & Z <> {} ;

      set m = ( card ((X \/ Y) \/ Z));

      set m0 = ( card (X \ (Y \/ Z)));

      set m1 = ( card (Y \ (X \/ Z)));

      set m2 = ( card ((X /\ Y) \ Z));

      set m3 = ( card ((X /\ Z) \ Y));

      set m4 = ( card (Z \ (X \/ Y)));

      

       D1: (X \ (Y \/ Z)) = ((X \ Y) /\ (X \ Z)) by XBOOLE_1: 53;

      (X /\ Z) misses (X \ Z) by XBOOLE_1: 89;

      then ((X /\ Z) \ Y) misses (X \ Z) by XBOOLE_1: 80;

      then

       D3b: (m0 + m3) = ( card ((X \ (Y \/ Z)) \/ ((X /\ Z) \ Y))) by CARD_2: 40, D1, XBOOLE_1: 74;

      Y = ((Y \ Z) \/ Y) by XBOOLE_1: 12, XBOOLE_1: 36

      .= (((Y \/ Z) \ Z) \/ Y) by XBOOLE_1: 40

      .= (((Y \/ Z) \ Z) \/ ((Y \/ Z) /\ Y)) by XBOOLE_1: 21

      .= ((Y \/ Z) \ (Z \ Y)) by XBOOLE_1: 52;

      then

       u1: ((X \ (Y \/ Z)) \/ (X /\ (Z \ Y))) = (X \ Y) by XBOOLE_1: 52;

      (X \ (Y \/ Z)) misses (X /\ Y) by D1, XBOOLE_1: 74, XBOOLE_1: 89;

      then

       D2: (X \ (Y \/ Z)) misses ((X /\ Y) \ Z) by XBOOLE_1: 63, XBOOLE_1: 36;

      

       D3: (m0 + m2) = ( card ((X \ (Y \/ Z)) \/ ((X /\ Y) \ Z))) by D2, CARD_2: 40;

      Z = ((Z \ Y) \/ Z) by XBOOLE_1: 12, XBOOLE_1: 36

      .= (((Y \/ Z) \ Y) \/ Z) by XBOOLE_1: 40

      .= (((Y \/ Z) \ Y) \/ ((Y \/ Z) /\ Z)) by XBOOLE_1: 21

      .= ((Y \/ Z) \ (Y \ Z)) by XBOOLE_1: 52;

      then ((X \ (Y \/ Z)) \/ (X /\ (Y \ Z))) = (X \ Z) by XBOOLE_1: 52;

      then

       Z2: ( card (X \ Z)) = (m0 + m2) by D3, XBOOLE_1: 49;

      

       d1: (Y \ (X \/ Z)) c= (Y \ X) by XBOOLE_1: 34, XBOOLE_1: 7;

      (X /\ Y) misses (Y \ X) by XBOOLE_1: 89;

      then (Y \ (X \/ Z)) misses (X /\ Y) by d1, XBOOLE_1: 63;

      then

       D2: (Y \ (X \/ Z)) misses ((X /\ Y) \ Z) by XBOOLE_1: 63, XBOOLE_1: 36;

      

       D3a: (m1 + m2) = ( card ((Y \ (X \/ Z)) \/ ((X /\ Y) \ Z))) by D2, CARD_2: 40;

      Z = ((Z \ X) \/ Z) by XBOOLE_1: 12, XBOOLE_1: 36

      .= (((X \/ Z) \ X) \/ Z) by XBOOLE_1: 40

      .= (((X \/ Z) \ X) \/ ((X \/ Z) /\ Z)) by XBOOLE_1: 21

      .= ((X \/ Z) \ (X \ Z)) by XBOOLE_1: 52;

      then

       aa: ((Y \ (X \/ Z)) \/ (Y /\ (X \ Z))) = (Y \ Z) by XBOOLE_1: 52;

      then

       Z3: ( card (Y \ Z)) = (m1 + m2) by D3a, XBOOLE_1: 49;

      ((Z \ (X \/ Y)) \/ (X \/ Y)) = ((X \/ Y) \/ Z) by XBOOLE_1: 39;

      then

       x4: (( card (Z \ (X \/ Y))) + ( card (X \/ Y))) = m by XBOOLE_1: 79, CARD_2: 40;

      ((Y \ (X \/ Z)) \/ (X \/ Z)) = (Y \/ (X \/ Z)) by XBOOLE_1: 39

      .= ((X \/ Y) \/ Z) by XBOOLE_1: 4;

      then

       z5: (( card (Y \ (X \/ Z))) + ( card (X \/ Z))) = m by XBOOLE_1: 79, CARD_2: 40;

      then ( card (X \/ Z)) = (m - m1);

      then

       U3: m > ( 0 + m1) by XREAL_1: 20, ZZ;

      ((X \ (Y \/ Z)) \/ (Y \/ Z)) = (X \/ (Y \/ Z)) by XBOOLE_1: 39

      .= ((X \/ Y) \/ Z) by XBOOLE_1: 4;

      then

       Z6: (( card (X \ (Y \/ Z))) + ( card (Y \/ Z))) = m by XBOOLE_1: 79, CARD_2: 40;

      

       T1: (( CMap ( kappa_1 R)) . (X,Y)) = (( card (X \ Y)) / ( card (X \/ Y))) by ZZ, PropEx3

      .= ((m0 + m3) / (m - m4)) by u1, x4, XBOOLE_1: 49, D3b;

      

       T2: (( CMap ( kappa_1 R)) . (Y,Z)) = (( card (Y \ Z)) / ( card (Y \/ Z))) by ZZ, PropEx3

      .= ((m1 + m2) / (m - m0)) by aa, Z6, XBOOLE_1: 49, D3a;

      

       T3: (( CMap ( kappa_1 R)) . (X,Z)) = ((m0 + m2) / (m - m1)) by Z2, z5, ZZ, PropEx3;

       0 <= m4;

      then (m - m) <= m4;

      then (m - m4) <= m by XREAL_1: 12;

      then

       V1: ((m0 + m3) / (m - m4)) >= ((m0 + m3) / m) by XREAL_1: 118, x4, ZZ;

       0 <= m0;

      then (m - m) <= m0;

      then (m - m0) <= m by XREAL_1: 12;

      then

       V2: ((m1 + m2) / (m - m0)) >= ((m1 + m2) / m) by XREAL_1: 118, Z6, ZZ;

      (m0 + m3) >= (m0 + 0 ) by XREAL_1: 6;

      then

       V3: ((m0 + m3) + (m1 + m2)) >= ((m0 + 0 ) + (m1 + m2)) by XREAL_1: 6;

      

       B2: (((m0 + m3) / (m - m4)) + ((m1 + m2) / (m - m0))) >= (((m0 + m3) / m) + ((m1 + m2) / m)) by V1, V2, XREAL_1: 7;

      (((m0 + m3) / m) + ((m1 + m2) / m)) = (((m0 + m3) + (m1 + m2)) / m) by XCMPLX_1: 62;

      then

       B3: (((m0 + m3) / m) + ((m1 + m2) / m)) >= (((m0 + m1) + m2) / m) by V3, XREAL_1: 72;

      set a = ((m0 + m1) + m2);

      set b = m;

      

       F2: a = (( card (X \ (Y \/ Z))) + ( card (Y \ Z))) by Z3;

      (X \ Y) misses Y by XBOOLE_1: 79;

      then (X \ Y) misses (Y \ Z) by XBOOLE_1: 63, XBOOLE_1: 36;

      then ((X \ Y) /\ (X \ Z)) misses (Y \ Z) by XBOOLE_1: 74;

      then

       F5: (X \ (Y \/ Z)) misses (Y \ Z) by XBOOLE_1: 53;

      (X \ (Y \/ Z)) c= X & (Y \ Z) c= Y by XBOOLE_1: 36;

      then

       F4: ((X \ (Y \/ Z)) \/ (Y \ Z)) c= (X \/ Y) by XBOOLE_1: 13;

      (X \/ Y) c= ((X \/ Y) \/ Z) by XBOOLE_1: 7;

      then

       f6: ((X \ (Y \/ Z)) \/ (Y \ Z)) c= ((X \/ Y) \/ Z) by F4;

      ( card ((X \ (Y \/ Z)) \/ (Y \ Z))) = a by F2, F5, CARD_2: 40;

      then (a / b) >= ((a - m1) / (b - m1)) by f6, U3, LemacikX, NAT_1: 43;

      then (((m0 + m3) / m) + ((m1 + m2) / m)) >= ((m0 + m2) / (m - m1)) by B3, XXREAL_0: 2;

      hence thesis by T1, T2, T3, B2, XXREAL_0: 2;

    end;

    

     Lack: for X,Y be set holds (X \+\ Y) c= (X \/ Y)

    proof

      let X,Y be set;

      (X \+\ Y) = ((X \/ Y) \ (X /\ Y)) by XBOOLE_1: 101;

      hence thesis;

    end;

    

     Lemma6f1: (X = {} & Y <> {} ) or (X <> {} & Y = {} ) implies ((( CMap ( kappa_1 R)) . (X,Y)) + (( CMap ( kappa_1 R)) . (Y,X))) = 1

    proof

      assume (X = {} & Y <> {} ) or (X <> {} & Y = {} );

      per cases ;

        suppose

         A0: X = {} & Y <> {} ;

        

        then ((( CMap ( kappa_1 R)) . (X,Y)) + (( CMap ( kappa_1 R)) . (Y,X))) = ((( card (X \ Y)) / ( card (X \/ Y))) + (( CMap ( kappa_1 R)) . (Y,X))) by PropEx3

        .= ((( card (X \ Y)) / ( card (X \/ Y))) + (( card (Y \ X)) / ( card (X \/ Y)))) by PropEx3, A0

        .= (( card Y) / ( card Y)) by A0;

        hence thesis by A0, XCMPLX_1: 60;

      end;

        suppose

         A0: Y = {} & X <> {} ;

        

        then ((( CMap ( kappa_1 R)) . (X,Y)) + (( CMap ( kappa_1 R)) . (Y,X))) = ((( card (X \ Y)) / ( card (X \/ Y))) + (( CMap ( kappa_1 R)) . (Y,X))) by PropEx3

        .= ((( card (X \ Y)) / ( card (X \/ Y))) + (( card (Y \ X)) / ( card (X \/ Y)))) by PropEx3, A0

        .= (( card X) / ( card X)) by A0;

        hence thesis by A0, XCMPLX_1: 60;

      end;

    end;

    theorem :: ROUGHIF2:21

    

     Ble1: X <> {} & Y = {} implies (( CMap ( kappa_1 R)) . (X,Y)) = 1

    proof

      assume

       A1: X <> {} & Y = {} ;

      

      then (( CMap ( kappa_1 R)) . (X,Y)) = (( card (X \ Y)) / ( card (X \/ Y))) by PropEx3

      .= 1 by A1, XCMPLX_1: 60;

      hence thesis;

    end;

    theorem :: ROUGHIF2:22

    X = {} & Y <> {} implies (( CMap ( kappa_1 R)) . (X,Y)) = 0

    proof

      assume

       A1: X = {} & Y <> {} ;

      

      then (( CMap ( kappa_1 R)) . (X,Y)) = (( card (X \ Y)) / ( card (X \/ Y))) by PropEx3

      .= 0 by A1;

      hence thesis;

    end;

    theorem :: ROUGHIF2:23

    

     Prop6d1: ((( CMap ( kappa_1 R)) . (X,Y)) + (( CMap ( kappa_1 R)) . (Y,Z))) >= (( CMap ( kappa_1 R)) . (X,Z))

    proof

      per cases ;

        suppose

         F1: X = {} ;

        then X c= Y;

        then

         F2: (( CMap ( kappa_1 R)) . (X,Y)) = 0 by Prop6a;

        (( CMap ( kappa_1 R)) . (X,Z)) = 0 by Prop6a, F1, XBOOLE_1: 2;

        hence thesis by F2, XXREAL_1: 1;

      end;

        suppose

         F1: X <> {} & Y = {} & Z <> {} ;

        then Y c= Z;

        then

         F2: (( CMap ( kappa_1 R)) . (Y,Z)) = 0 by Prop6a;

        (( CMap ( kappa_1 R)) . (X,Y)) = 1 by F1, Ble1;

        hence thesis by F2, XXREAL_1: 1;

      end;

        suppose

         F1: X <> {} & Y <> {} & Z = {} ;

        then

         F3: (( CMap ( kappa_1 R)) . (X,Z)) = 1 by Ble1;

        (( CMap ( kappa_1 R)) . (X,Y)) >= 0 by XXREAL_1: 1;

        then ((( CMap ( kappa_1 R)) . (X,Y)) + 1) >= ( 0 + 1) by XREAL_1: 6;

        hence thesis by F1, F3, Ble1;

      end;

        suppose

         F1: X <> {} & Y = {} & Z = {} ;

        then

         F3: (( CMap ( kappa_1 R)) . (X,Y)) = 1 by Ble1;

        (( CMap ( kappa_1 R)) . (Y,Z)) >= 0 by XXREAL_1: 1;

        then (1 + (( CMap ( kappa_1 R)) . (Y,Z))) >= (1 + 0 ) by XREAL_1: 6;

        hence thesis by F1, F3;

      end;

        suppose X <> {} & Y <> {} & Z <> {} ;

        hence thesis by Jaga1;

      end;

    end;

    theorem :: ROUGHIF2:24

     0 <= (( CMap ( kappa R)) . (X,Y)) <= 1 by XXREAL_1: 1;

    theorem :: ROUGHIF2:25

    

     Prop6e1: 0 <= ((( CMap ( kappa_1 R)) . (X,Y)) + (( CMap ( kappa_1 R)) . (Y,X))) <= 1

    proof

      per cases ;

        suppose (X \/ Y) = {} ;

        then (( CMap ( kappa_1 R)) . (X,Y)) = 0 & (( CMap ( kappa_1 R)) . (Y,X)) = 0 by PropEx30;

        hence thesis;

      end;

        suppose

         B1: (X \/ Y) <> {} ;

        

        then

         A1: ((( CMap ( kappa_1 R)) . (X,Y)) + (( CMap ( kappa_1 R)) . (Y,X))) = ((( card (X \ Y)) / ( card (X \/ Y))) + (( CMap ( kappa_1 R)) . (Y,X))) by PropEx3

        .= ((( card (X \ Y)) / ( card (X \/ Y))) + (( card (Y \ X)) / ( card (X \/ Y)))) by PropEx3, B1

        .= ((( card (X \ Y)) + ( card (Y \ X))) / ( card (X \/ Y))) by XCMPLX_1: 62

        .= (( card (X \+\ Y)) / ( card (X \/ Y))) by CARD_2: 40, XBOOLE_1: 82;

        ( card (X \+\ Y)) <= ( card (X \/ Y)) by Lack, NAT_1: 43;

        hence thesis by A1, XREAL_1: 183;

      end;

    end;

    theorem :: ROUGHIF2:26

    

     Prop6e2: 0 <= ((( CMap ( kappa_2 R)) . (X,Y)) + (( CMap ( kappa_2 R)) . (Y,X))) <= 1

    proof

      ((( CMap ( kappa_2 R)) . (X,Y)) + (( CMap ( kappa_2 R)) . (Y,X))) = ((( card (X \ Y)) / ( card ( [#] R))) + (( CMap ( kappa_2 R)) . (Y,X))) by PropEx31

      .= ((( card (X \ Y)) / ( card ( [#] R))) + (( card (Y \ X)) / ( card ( [#] R)))) by PropEx31

      .= ((( card (X \ Y)) + ( card (Y \ X))) / ( card ( [#] R))) by XCMPLX_1: 62

      .= (( card (X \+\ Y)) / ( card ( [#] R))) by CARD_2: 40, XBOOLE_1: 82;

      hence thesis by NAT_1: 43, XREAL_1: 183;

    end;

    

     Lemma6f: (X = {} & Y <> {} ) or (X <> {} & Y = {} ) implies ((( CMap ( kappa R)) . (X,Y)) + (( CMap ( kappa R)) . (Y,X))) = 1

    proof

      assume (X = {} & Y <> {} ) or (X <> {} & Y = {} );

      per cases ;

        suppose

         A0: X = {} & Y <> {} ;

        

        then ((( CMap ( kappa R)) . (X,Y)) + (( CMap ( kappa R)) . (Y,X))) = ( 0 + (( CMap ( kappa R)) . (Y,X))) by PropEx3k0

        .= (( card (Y \ X)) / ( card Y)) by A0, PropEx3k

        .= (( card Y) / ( card Y)) by A0;

        hence thesis by A0, XCMPLX_1: 60;

      end;

        suppose

         A0: Y = {} & X <> {} ;

        

        then ((( CMap ( kappa R)) . (X,Y)) + (( CMap ( kappa R)) . (Y,X))) = ((( card (X \ Y)) / ( card (X \/ Y))) + (( CMap ( kappa R)) . (Y,X))) by PropEx3k

        .= ((( card (X \ Y)) / ( card (X \/ Y))) + 0 ) by PropEx3k0, A0

        .= (( card X) / ( card X)) by A0;

        hence thesis by A0, XCMPLX_1: 60;

      end;

    end;

    theorem :: ROUGHIF2:27

    (X = {} & Y <> {} ) or (X <> {} & Y = {} ) implies ((( CMap ( kappa R)) . (X,Y)) + (( CMap ( kappa R)) . (Y,X))) = ((( CMap ( kappa_1 R)) . (X,Y)) + (( CMap ( kappa_1 R)) . (Y,X))) = 1

    proof

      assume

       A1: (X = {} & Y <> {} ) or (X <> {} & Y = {} );

      then ((( CMap ( kappa R)) . (X,Y)) + (( CMap ( kappa R)) . (Y,X))) = 1 by Lemma6f;

      hence thesis by A1, Lemma6f1;

    end;

    definition

      let R;

      :: ROUGHIF2:def3

      func delta_L R -> preRIF of R means

      : DeltaL: for x,y be Subset of R holds (it . (x,y)) = (((( CMap ( kappa R)) . (x,y)) + (( CMap ( kappa R)) . (y,x))) / 2);

      existence

      proof

        deffunc F( Subset of R, Subset of R) = ( In ((((( CMap ( kappa R)) . ($1,$2)) + (( CMap ( kappa R)) . ($2,$1))) / 2), [. 0 , 1.]));

        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 ff 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 (ff . (x,y)) = F(x,y);

        take ff;

        let x,y be Subset of R;

        

         b1: 0 <= (( CMap ( kappa R)) . (x,y)) & 0 <= (( CMap ( kappa R)) . (y,x)) by XXREAL_1: 1;

        (( CMap ( kappa R)) . (x,y)) <= 1 & (( CMap ( kappa R)) . (y,x)) <= 1 by XXREAL_1: 1;

        then ((( CMap ( kappa R)) . (x,y)) + (( CMap ( kappa R)) . (y,x))) <= (1 + 1) by XREAL_1: 7;

        then

         bb: (((( CMap ( kappa R)) . (x,y)) + (( CMap ( kappa R)) . (y,x))) / 2) <= (2 / 2) by XREAL_1: 72;

        (ff . (x,y)) = ( In ((((( CMap ( kappa R)) . (x,y)) + (( CMap ( kappa R)) . (y,x))) / 2), [. 0 , 1.])) by A1

        .= (((( CMap ( kappa R)) . (x,y)) + (( CMap ( kappa R)) . (y,x))) / 2) by bb, SUBSET_1:def 8, b1, XXREAL_1: 1;

        hence thesis;

      end;

      uniqueness

      proof

        deffunc G( Subset of R, Subset of R) = (((( CMap ( kappa R)) . ($1,$2)) + (( CMap ( kappa R)) . ($2,$1))) / 2);

        let f1,f2 be preRIF of R such that

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

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

        for x,y be Subset of R holds (f1 . (x,y)) = (f2 . (x,y))

        proof

          let x,y be Subset of R;

          (f1 . (x,y)) = G(x,y) by A1

          .= (f2 . (x,y)) by A2;

          hence thesis;

        end;

        hence thesis by BINOP_1: 2;

      end;

      :: ROUGHIF2:def4

      func delta_1 R -> preRIF of R means

      : Delta1: for x,y be Subset of R holds (it . (x,y)) = ((( CMap ( kappa_1 R)) . (x,y)) + (( CMap ( kappa_1 R)) . (y,x)));

      existence

      proof

        deffunc F( Subset of R, Subset of R) = ( In (((( CMap ( kappa_1 R)) . ($1,$2)) + (( CMap ( kappa_1 R)) . ($2,$1))), [. 0 , 1.]));

        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 ff 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 (ff . (x,y)) = F(x,y);

        take ff;

        let x,y be Subset of R;

        

         B1: 0 <= ((( CMap ( kappa_1 R)) . (x,y)) + (( CMap ( kappa_1 R)) . (y,x))) <= 1 by Prop6e1;

        (ff . (x,y)) = ( In (((( CMap ( kappa_1 R)) . (x,y)) + (( CMap ( kappa_1 R)) . (y,x))), [. 0 , 1.])) by A1

        .= ((( CMap ( kappa_1 R)) . (x,y)) + (( CMap ( kappa_1 R)) . (y,x))) by B1, XXREAL_1: 1, SUBSET_1:def 8;

        hence thesis;

      end;

      uniqueness

      proof

        deffunc G( Subset of R, Subset of R) = ((( CMap ( kappa_1 R)) . ($1,$2)) + (( CMap ( kappa_1 R)) . ($2,$1)));

        let f1,f2 be preRIF of R such that

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

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

        for x,y be Subset of R holds (f1 . (x,y)) = (f2 . (x,y))

        proof

          let x,y be Subset of R;

          (f1 . (x,y)) = G(x,y) by A1

          .= (f2 . (x,y)) by A2;

          hence thesis;

        end;

        hence thesis by BINOP_1: 2;

      end;

      :: ROUGHIF2:def5

      func delta_2 R -> preRIF of R means

      : Delta2: for x,y be Subset of R holds (it . (x,y)) = ((( CMap ( kappa_2 R)) . (x,y)) + (( CMap ( kappa_2 R)) . (y,x)));

      existence

      proof

        deffunc F( Subset of R, Subset of R) = ( In (((( CMap ( kappa_2 R)) . ($1,$2)) + (( CMap ( kappa_2 R)) . ($2,$1))), [. 0 , 1.]));

        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 ff 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 (ff . (x,y)) = F(x,y);

        take ff;

        let x,y be Subset of R;

        

         B1: 0 <= ((( CMap ( kappa_2 R)) . (x,y)) + (( CMap ( kappa_2 R)) . (y,x))) <= 1 by Prop6e2;

        (ff . (x,y)) = ( In (((( CMap ( kappa_2 R)) . (x,y)) + (( CMap ( kappa_2 R)) . (y,x))), [. 0 , 1.])) by A1

        .= ((( CMap ( kappa_2 R)) . (x,y)) + (( CMap ( kappa_2 R)) . (y,x))) by B1, XXREAL_1: 1, SUBSET_1:def 8;

        hence thesis;

      end;

      uniqueness

      proof

        deffunc G( Subset of R, Subset of R) = ((( CMap ( kappa_2 R)) . ($1,$2)) + (( CMap ( kappa_2 R)) . ($2,$1)));

        let f1,f2 be preRIF of R such that

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

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

        for x,y be Subset of R holds (f1 . (x,y)) = (f2 . (x,y))

        proof

          let x,y be Subset of R;

          (f1 . (x,y)) = G(x,y) by A1

          .= (f2 . (x,y)) by A2;

          hence thesis;

        end;

        hence thesis by BINOP_1: 2;

      end;

    end

    theorem :: ROUGHIF2:28

    (( delta_L R) . (X,Y)) = 0 iff X = Y

    proof

      

       B1: (( CMap ( kappa R)) . (X,Y)) >= 0 & (( CMap ( kappa R)) . (Y,X)) >= 0 by XXREAL_1: 1;

      hereby

        assume (( delta_L R) . (X,Y)) = 0 ;

        then (((( CMap ( kappa R)) . (X,Y)) + (( CMap ( kappa R)) . (Y,X))) / 2) = 0 by DeltaL;

        then (( CMap ( kappa R)) . (X,Y)) = 0 & (( CMap ( kappa R)) . (Y,X)) = 0 by B1;

        hence X = Y by Prop6a;

      end;

      assume

       A1: X = Y;

      (( delta_L R) . (X,Y)) = (((( CMap ( kappa R)) . (X,Y)) + (( CMap ( kappa R)) . (Y,X))) / 2) by DeltaL

      .= (( 0 + 0 ) / 2) by Prop6a, A1;

      hence thesis;

    end;

    theorem :: ROUGHIF2:29

    (( delta_L R) . (X,Y)) = (( delta_L R) . (Y,X))

    proof

      (( delta_L R) . (X,Y)) = (((( CMap ( kappa R)) . (X,Y)) + (( CMap ( kappa R)) . (Y,X))) / 2) by DeltaL;

      hence thesis by DeltaL;

    end;

    theorem :: ROUGHIF2:30

    (X <> {} & Y = {} ) or (X = {} & Y <> {} ) implies (( delta_L R) . (X,Y)) = (1 / 2)

    proof

      assume (X <> {} & Y = {} ) or (X = {} & Y <> {} );

      then ((( CMap ( kappa R)) . (X,Y)) + (( CMap ( kappa R)) . (Y,X))) = 1 by Lemma6f;

      hence thesis by DeltaL;

    end;

    theorem :: ROUGHIF2:31

    X <> {} & Y <> {} implies (( delta_L R) . (X,Y)) = (((( card (X \ Y)) / ( card X)) + (( card (Y \ X)) / ( card Y))) / 2)

    proof

      assume

       A1: X <> {} & Y <> {} ;

      then

       A2: (( CMap ( kappa R)) . (X,Y)) = (( card (X \ Y)) / ( card X)) by PropEx3k;

      (( CMap ( kappa R)) . (Y,X)) = (( card (Y \ X)) / ( card Y)) by A1, PropEx3k;

      hence thesis by DeltaL, A2;

    end;

    theorem :: ROUGHIF2:32

    

     For191: (( delta_1 R) . (X,Y)) = (( card (X \+\ Y)) / ( card (X \/ Y)))

    proof

      per cases ;

        suppose

         A0: (X \/ Y) <> {} ;

        then

         A2: (( CMap ( kappa_1 R)) . (Y,X)) = (( card (Y \ X)) / ( card (X \/ Y))) by PropEx3;

        (( delta_1 R) . (X,Y)) = ((( CMap ( kappa_1 R)) . (X,Y)) + (( CMap ( kappa_1 R)) . (Y,X))) by Delta1

        .= ((( card (X \ Y)) / ( card (X \/ Y))) + (( card (Y \ X)) / ( card (X \/ Y)))) by A0, PropEx3, A2

        .= ((( card (X \ Y)) + ( card (Y \ X))) / ( card (X \/ Y))) by XCMPLX_1: 62

        .= (( card (X \+\ Y)) / ( card (X \/ Y))) by XBOOLE_1: 82, CARD_2: 40;

        hence thesis;

      end;

        suppose

         A0: (X \/ Y) = {} ;

        then X = {} & Y = {} ;

        then (( CMap ( kappa_1 R)) . (X,Y)) = 0 & (( CMap ( kappa_1 R)) . (Y,X)) = 0 by Prop6a;

        then (( delta_1 R) . (X,Y)) = ( 0 + 0 ) by Delta1;

        hence thesis by A0;

      end;

    end;

    theorem :: ROUGHIF2:33

    (( delta_2 R) . (X,Y)) = (( card (X \+\ Y)) / ( card ( [#] R)))

    proof

      

       A1: (( CMap ( kappa_2 R)) . (X,Y)) = (( card (X \ Y)) / ( card ( [#] R))) by PropEx31;

      

       A2: (( CMap ( kappa_2 R)) . (Y,X)) = (( card (Y \ X)) / ( card ( [#] R))) by PropEx31;

      (( delta_2 R) . (X,Y)) = ((( CMap ( kappa_2 R)) . (X,Y)) + (( CMap ( kappa_2 R)) . (Y,X))) by Delta2

      .= ((( card (X \ Y)) + ( card (Y \ X))) / ( card ( [#] R))) by XCMPLX_1: 62, A1, A2

      .= (( card (X \+\ Y)) / ( card ( [#] R))) by XBOOLE_1: 82, CARD_2: 40;

      hence thesis;

    end;

    theorem :: ROUGHIF2:34

    ((( delta_1 R) . (X,Y)) + (( delta_1 R) . (Y,Z))) >= (( delta_1 R) . (X,Z))

    proof

      set m1 = (( CMap ( kappa_1 R)) . (X,Y)), m2 = (( CMap ( kappa_1 R)) . (Y,Z));

      set m3 = (( CMap ( kappa_1 R)) . (X,Z)), m4 = (( CMap ( kappa_1 R)) . (Z,Y)), m5 = (( CMap ( kappa_1 R)) . (Y,X)), m6 = (( CMap ( kappa_1 R)) . (Z,X));

      

       A1: (m1 + m2) >= m3 by Prop6d1;

      (m4 + m5) >= m6 by Prop6d1;

      then ((m1 + m2) + (m4 + m5)) >= (m3 + m6) by A1, XREAL_1: 7;

      then ((m1 + m5) + (m2 + m4)) >= (m3 + m6);

      then ((( delta_1 R) . (X,Y)) + (m2 + m4)) >= (m3 + m6) by Delta1;

      then ((( delta_1 R) . (X,Y)) + (( delta_1 R) . (Y,Z))) >= (m3 + m6) by Delta1;

      hence thesis by Delta1;

    end;

    theorem :: ROUGHIF2:35

    (( delta_1 R) . (X,Y)) = 0 iff X = Y

    proof

      

       B1: (( CMap ( kappa_1 R)) . (X,Y)) >= 0 & (( CMap ( kappa_1 R)) . (Y,X)) >= 0 by XXREAL_1: 1;

      hereby

        assume (( delta_1 R) . (X,Y)) = 0 ;

        then ((( CMap ( kappa_1 R)) . (X,Y)) + (( CMap ( kappa_1 R)) . (Y,X))) = 0 by Delta1;

        then (( CMap ( kappa_1 R)) . (X,Y)) = 0 & (( CMap ( kappa_1 R)) . (Y,X)) = 0 by B1;

        hence X = Y by Prop6a;

      end;

      assume

       A1: X = Y;

      (( delta_1 R) . (X,Y)) = ((( CMap ( kappa_1 R)) . (X,Y)) + (( CMap ( kappa_1 R)) . (Y,X))) by Delta1

      .= ((( CMap ( kappa_1 R)) . (X,X)) + 0 ) by Prop6a, A1

      .= ( 0 + 0 ) by Prop6a;

      hence thesis;

    end;

    theorem :: ROUGHIF2:36

    (( delta_1 R) . (X,Y)) = (( delta_1 R) . (Y,X))

    proof

      (( delta_1 R) . (X,Y)) = ((( CMap ( kappa_1 R)) . (X,Y)) + (( CMap ( kappa_1 R)) . (Y,X))) by Delta1;

      hence thesis by Delta1;

    end;

    theorem :: ROUGHIF2:37

    (( delta_2 R) . (X,Y)) = 0 iff X = Y

    proof

      

       B1: (( CMap ( kappa_2 R)) . (X,Y)) >= 0 & (( CMap ( kappa_2 R)) . (Y,X)) >= 0 by XXREAL_1: 1;

      hereby

        assume (( delta_2 R) . (X,Y)) = 0 ;

        then ((( CMap ( kappa_2 R)) . (X,Y)) + (( CMap ( kappa_2 R)) . (Y,X))) = 0 by Delta2;

        then (( CMap ( kappa_2 R)) . (X,Y)) = 0 & (( CMap ( kappa_2 R)) . (Y,X)) = 0 by B1;

        hence X = Y by Prop6a;

      end;

      assume

       A1: X = Y;

      (( delta_2 R) . (X,Y)) = ((( CMap ( kappa_2 R)) . (X,Y)) + (( CMap ( kappa_2 R)) . (Y,X))) by Delta2

      .= ((( CMap ( kappa_2 R)) . (X,X)) + 0 ) by Prop6a, A1

      .= ( 0 + 0 ) by Prop6a;

      hence thesis;

    end;

    theorem :: ROUGHIF2:38

    (( delta_2 R) . (X,Y)) = (( delta_2 R) . (Y,X))

    proof

      (( delta_2 R) . (X,Y)) = ((( CMap ( kappa_2 R)) . (X,Y)) + (( CMap ( kappa_2 R)) . (Y,X))) by Delta2;

      hence thesis by Delta2;

    end;

    theorem :: ROUGHIF2:39

    

     Prop6d2: ((( CMap ( kappa_2 R)) . (X,Y)) + (( CMap ( kappa_2 R)) . (Y,Z))) >= (( CMap ( kappa_2 R)) . (X,Z))

    proof

      

       B1: (( CMap ( kappa_2 R)) . (X,Y)) = (( card (X \ Y)) / ( card ( [#] R))) by PropEx31;

      

       B2: (( CMap ( kappa_2 R)) . (Y,Z)) = (( card (Y \ Z)) / ( card ( [#] R))) by PropEx31;

      

       B3: (( CMap ( kappa_2 R)) . (X,Z)) = (( card (X \ Z)) / ( card ( [#] R))) by PropEx31;

      

       A1: (Y \ Z) c= Y by XBOOLE_1: 36;

      (X \ Y) misses Y by XBOOLE_1: 79;

      then

       A2: ( card ((X \ Y) \/ (Y \ Z))) = (( card (X \ Y)) + ( card (Y \ Z))) by CARD_2: 40, A1, XBOOLE_1: 63;

      (X \ Z) c= ((X \ Y) \/ (Y \ Z))

      proof

        let x be object;

        assume x in (X \ Z);

        then

         A3: x in X & not x in Z by XBOOLE_0:def 5;

        per cases ;

          suppose x in Y;

          then x in (Y \ Z) by A3, XBOOLE_0:def 5;

          hence thesis by XBOOLE_0:def 3;

        end;

          suppose not x in Y;

          then x in (X \ Y) by A3, XBOOLE_0:def 5;

          hence thesis by XBOOLE_0:def 3;

        end;

      end;

      then ((( card (X \ Y)) + ( card (Y \ Z))) / ( card ( [#] R))) >= (( card (X \ Z)) / ( card ( [#] R))) by A2, XREAL_1: 72, NAT_1: 43;

      hence thesis by B1, B2, B3, XCMPLX_1: 62;

    end;

    theorem :: ROUGHIF2:40

    ((( delta_2 R) . (X,Y)) + (( delta_2 R) . (Y,Z))) >= (( delta_2 R) . (X,Z))

    proof

      set m1 = (( CMap ( kappa_2 R)) . (X,Y)), m2 = (( CMap ( kappa_2 R)) . (Y,Z));

      set m3 = (( CMap ( kappa_2 R)) . (X,Z)), m4 = (( CMap ( kappa_2 R)) . (Z,Y)), m5 = (( CMap ( kappa_2 R)) . (Y,X)), m6 = (( CMap ( kappa_2 R)) . (Z,X));

      

       A1: (m1 + m2) >= m3 by Prop6d2;

      (m4 + m5) >= m6 by Prop6d2;

      then ((m1 + m2) + (m4 + m5)) >= (m3 + m6) by A1, XREAL_1: 7;

      then ((m1 + m5) + (m2 + m4)) >= (m3 + m6);

      then ((( delta_2 R) . (X,Y)) + (m2 + m4)) >= (m3 + m6) by Delta2;

      then ((( delta_2 R) . (X,Y)) + (( delta_2 R) . (Y,Z))) >= (m3 + m6) by Delta2;

      hence thesis by Delta2;

    end;

    begin

    definition

      let R be finite set;

      let A,B be Subset of R;

      :: ROUGHIF2:def6

      func JaccardIndex (A,B) -> Element of [. 0 , 1.] equals

      : JacInd: (( card (A /\ B)) / ( card (A \/ B))) if (A \/ B) <> {}

      otherwise 1;

      coherence

      proof

        (( card (A /\ B)) / ( card (A \/ B))) in [. 0 , 1.]

        proof

          

           B1: (A /\ B) c= A by XBOOLE_1: 17;

          A c= (A \/ B) by XBOOLE_1: 7;

          then (A /\ B) c= (A \/ B) by B1;

          then (( card (A /\ B)) / ( card (A \/ B))) <= 1 by XREAL_1: 185, NAT_1: 43;

          hence thesis by XXREAL_1: 1;

        end;

        hence thesis by XXREAL_1: 1;

      end;

      correctness ;

    end

    theorem :: ROUGHIF2:41

    

     JacRefl: for R be finite set holds for A,B be Subset of R holds ( JaccardIndex (A,B)) = 1 iff A = B

    proof

      let R be finite set;

      let A,B be Subset of R;

      hereby

        assume

         T1: ( JaccardIndex (A,B)) = 1;

        per cases ;

          suppose (A \/ B) = {} ;

          then A = {} & B = {} ;

          hence A = B;

        end;

          suppose (A \/ B) <> {} ;

          then ( JaccardIndex (A,B)) = (( card (A /\ B)) / ( card (A \/ B))) by JacInd;

          then ( card (A /\ B)) = ( card (A \/ B)) by XCMPLX_1: 58, T1;

          hence A = B by LemmaCard;

        end;

      end;

      assume

       A0: A = B;

      per cases ;

        suppose A = {} ;

        then (A \/ B) = {} by A0;

        hence thesis by JacInd;

      end;

        suppose

         B1: A <> {} ;

        

        then ( JaccardIndex (A,B)) = (( card (A /\ A)) / ( card (A \/ A))) by JacInd, A0

        .= (( card A) / ( card A));

        hence thesis by B1, XCMPLX_1: 60;

      end;

    end;

    theorem :: ROUGHIF2:42

    

     JacSym: for R be finite set holds for A,B be Subset of R holds ( JaccardIndex (A,B)) = ( JaccardIndex (B,A))

    proof

      let R be finite set;

      let A,B be Subset of R;

      per cases ;

        suppose

         A1: (A \/ B) = {} ;

        

        hence ( JaccardIndex (A,B)) = 1 by JacInd

        .= ( JaccardIndex (B,A)) by A1, JacInd;

      end;

        suppose

         A1: (A \/ B) <> {} ;

        

        hence ( JaccardIndex (A,B)) = (( card (A /\ B)) / ( card (A \/ B))) by JacInd

        .= ( JaccardIndex (B,A)) by A1, JacInd;

      end;

    end;

    begin

    definition

      let R be finite set;

      :: ROUGHIF2:def7

      func JaccardDist R -> Function of [:( bool R), ( bool R):], REAL means

      : JacDef2: for A,B be Subset of R holds (it . (A,B)) = (1 - ( JaccardIndex (A,B)));

      existence

      proof

        deffunc F( Subset of R, Subset of R) = ( In ((1 - ( JaccardIndex ($1,$2))), REAL ));

        ex f be Function of [:( bool R), ( bool R):], REAL st for x,y be Element of ( bool R) holds (f . (x,y)) = F(x,y) from BINOP_1:sch 4;

        then

        consider ff be Function of [:( bool R), ( bool R):], REAL such that

         A1: for x,y be Element of ( bool R) holds (ff . (x,y)) = F(x,y);

        take ff;

        let x,y be Subset of R;

        (ff . (x,y)) = ( In ((1 - ( JaccardIndex (x,y))), REAL )) by A1

        .= (1 - ( JaccardIndex (x,y)));

        hence thesis;

      end;

      uniqueness

      proof

        deffunc G( Subset of R, Subset of R) = (1 - ( JaccardIndex ($1,$2)));

        let f1,f2 be Function of [:( bool R), ( bool R):], REAL such that

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

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

        for x,y be Subset of R holds (f1 . (x,y)) = (f2 . (x,y))

        proof

          let x,y be Subset of R;

          (f1 . (x,y)) = G(x,y) by A1

          .= (f2 . (x,y)) by A2;

          hence thesis;

        end;

        hence thesis by BINOP_1: 2;

      end;

      correctness ;

    end

    definition

      let R be finite 1-sorted;

      :: ROUGHIF2:def8

      func MarczewskiDistance R -> Function of [:( bool the carrier of R), ( bool the carrier of R):], REAL equals ( JaccardDist ( [#] R));

      coherence ;

    end

    begin

    definition

      let X be non empty set, f be Function of [:X, X:], REAL ;

      :: original: nonnegative-yielding

      redefine

      :: ROUGHIF2:def9

      attr f is nonnegative-yielding means

      : Non: for x,y be Element of X holds (f . (x,y)) >= 0 ;

      compatibility

      proof

        hereby

          assume

           A1: f is nonnegative-yielding;

          let x,y be Element of X;

          ( dom f) = [:X, X:] by FUNCT_2:def 1;

          then [x, y] in ( dom f);

          then (f . (x,y)) in ( rng f) by FUNCT_1: 3;

          hence (f . (x,y)) >= 0 by A1, PARTFUN3:def 4;

        end;

        assume

         A1: for x,y be Element of X holds (f . (x,y)) >= 0 ;

        let r be Real;

        assume r in ( rng f);

        then

        consider x be Element of [:X, X:] such that

         A2: r = (f . x) by FUNCT_2: 113;

        consider x1,x2 be object such that

         A3: x1 in X & x2 in X & x = [x1, x2] by ZFMISC_1:def 2;

        reconsider x1, x2 as Element of X by A3;

        r = (f . (x1,x2)) by A3, A2;

        hence thesis by A1;

      end;

    end

    registration

      let X be non empty set;

      cluster discerning symmetric Reflexive triangle for Function of [:X, X:], REAL ;

      existence

      proof

        take ( discrete_dist X);

        ( DiscreteSpace X) = MetrStruct (# X, ( discrete_dist X) #) by METRIC_1:def 11;

        hence thesis by METRIC_1:def 6, METRIC_1:def 7, METRIC_1:def 8, METRIC_1:def 9;

      end;

    end

    registration

      let X be non empty set;

      cluster Reflexive symmetric triangle -> nonnegative-yielding for Function of [:X, X:], REAL ;

      coherence

      proof

        let f be Function of [:X, X:], REAL ;

        assume

         AA: f is Reflexive symmetric triangle;

        now

          let a,b be Element of X;

          (f . (a,a)) <= ((f . (a,b)) + (f . (b,a))) by AA, METRIC_1:def 5;

          then 0 <= ((f . (a,b)) + (f . (b,a))) by AA, METRIC_1:def 2;

          then 0 <= ((f . (a,b)) + (f . (a,b))) by AA, METRIC_1:def 4;

          hence (f . (a,b)) >= 0 ;

        end;

        hence thesis;

      end;

    end

    theorem :: ROUGHIF2:43

    

     ME7: for X be non empty set holds for f be nonnegative-yielding discerning triangle Reflexive Function of [:X, X:], REAL , x,y be Element of X st x <> y holds (f . (x,y)) > 0

    proof

      let X be non empty set;

      let f be nonnegative-yielding discerning triangle Reflexive Function of [:X, X:], REAL , x,y be Element of X;

      assume x <> y;

      then (f . (x,y)) <> 0 by METRIC_1:def 3;

      hence thesis by Non;

    end;

    begin

    definition

      let X be non empty set, p be Element of X;

      let f be Function of [:X, X:], REAL ;

      :: ROUGHIF2:def10

      func SteinhausGen (f,p) -> Function of [:X, X:], REAL means

      : SteinGen: for x,y be Element of X holds (it . (x,y)) = ((2 * (f . (x,y))) / (((f . (x,p)) + (f . (y,p))) + (f . (x,y))));

      existence

      proof

        deffunc F( Element of X, Element of X) = ( In (((2 * (f . ($1,$2))) / (((f . ($1,p)) + (f . ($2,p))) + (f . ($1,$2)))), REAL ));

        ex ff be Function of [:X, X:], REAL st for x,y be Element of X holds (ff . (x,y)) = F(x,y) from BINOP_1:sch 4;

        then

        consider fg be Function of [:X, X:], REAL such that

         A1: for x,y be Element of X holds (fg . (x,y)) = F(x,y);

        take fg;

        let x,y be Element of X;

        (fg . (x,y)) = ( In (((2 * (f . (x,y))) / (((f . (x,p)) + (f . (y,p))) + (f . (x,y)))), REAL )) by A1

        .= ((2 * (f . (x,y))) / (((f . (x,p)) + (f . (y,p))) + (f . (x,y))));

        hence thesis;

      end;

      uniqueness

      proof

        deffunc G( Element of X, Element of X) = ((2 * (f . ($1,$2))) / (((f . ($1,p)) + (f . ($2,p))) + (f . ($1,$2))));

        let f1,f2 be Function of [:X, X:], REAL such that

         A1: (for x,y be Element of X holds (f1 . (x,y)) = G(x,y)) and

         A2: (for x,y be Element of X holds (f2 . (x,y)) = G(x,y));

        for x,y be Element of X holds (f1 . (x,y)) = (f2 . (x,y))

        proof

          let x,y be Element of X;

          (f1 . (x,y)) = G(x,y) by A1

          .= (f2 . (x,y)) by A2;

          hence thesis;

        end;

        hence thesis by BINOP_1: 2;

      end;

    end

    

     ZeZo: for X be non empty set, f be nonnegative-yielding Function of [:X, X:], REAL , p,x,y be Element of X holds (( SteinhausGen (f,p)) . (x,y)) >= 0

    proof

      let X be non empty set, f be nonnegative-yielding Function of [:X, X:], REAL , p,x,y be Element of X;

      set ff = ( SteinhausGen (f,p));

      

       A1: (ff . (x,y)) = ((2 * (f . (x,y))) / (((f . (x,p)) + (f . (y,p))) + (f . (x,y)))) by SteinGen;

      

       A3: (f . (x,y)) >= 0 by Non;

      (f . (x,p)) >= 0 & (f . (y,p)) >= 0 by Non;

      hence thesis by A1, A3;

    end;

    registration

      let X be non empty set, f be nonnegative-yielding Function of [:X, X:], REAL , p be Element of X;

      cluster ( SteinhausGen (f,p)) -> nonnegative-yielding;

      coherence by ZeZo;

    end

    registration

      let X be non empty set, f be nonnegative-yielding Reflexive Function of [:X, X:], REAL , p be Element of X;

      cluster ( SteinhausGen (f,p)) -> Reflexive;

      coherence

      proof

        set ff = ( SteinhausGen (f,p));

        for a be Element of X holds (ff . (a,a)) = 0

        proof

          let a be Element of X;

          (ff . (a,a)) = ((2 * (f . (a,a))) / (((f . (a,p)) + (f . (a,p))) + (f . (a,a)))) by SteinGen

          .= ((2 * 0 ) / (((f . (a,p)) + (f . (a,p))) + (f . (a,a)))) by METRIC_1:def 2

          .= 0 ;

          hence thesis;

        end;

        hence thesis by METRIC_1:def 2;

      end;

    end

    registration

      let X be non empty set, f be nonnegative-yielding discerning Function of [:X, X:], REAL , p be Element of X;

      cluster ( SteinhausGen (f,p)) -> discerning;

      coherence

      proof

        set ff = ( SteinhausGen (f,p));

        for a,b be Element of X st (ff . (a,b)) = 0 holds a = b

        proof

          let a,b be Element of X;

          (f . (a,p)) >= 0 & (f . (b,p)) >= 0 by Non;

          then

           A0: ((f . (a,p)) + (f . (b,p))) >= 0 & (f . (a,b)) >= 0 by Non;

          assume

           A1: (ff . (a,b)) = 0 ;

          (ff . (a,b)) = ((2 * (f . (a,b))) / (((f . (a,p)) + (f . (b,p))) + (f . (a,b)))) by SteinGen;

          then (f . (a,b)) = 0 or (((f . (a,p)) + (f . (b,p))) = 0 & (f . (a,b)) = 0 ) by A0, A1;

          hence thesis by METRIC_1:def 3;

        end;

        hence thesis by METRIC_1:def 3;

      end;

    end

    registration

      let X be non empty set, f be nonnegative-yielding symmetric Function of [:X, X:], REAL , p be Element of X;

      cluster ( SteinhausGen (f,p)) -> symmetric;

      coherence

      proof

        set ff = ( SteinhausGen (f,p));

        for a,b be Element of X holds (ff . (a,b)) = (ff . (b,a))

        proof

          let a,b be Element of X;

          (ff . (a,b)) = ((2 * (f . (a,b))) / (((f . (a,p)) + (f . (b,p))) + (f . (a,b)))) by SteinGen

          .= ((2 * (f . (b,a))) / (((f . (a,p)) + (f . (b,p))) + (f . (a,b)))) by METRIC_1:def 4

          .= ((2 * (f . (b,a))) / (((f . (b,p)) + (f . (a,p))) + (f . (b,a)))) by METRIC_1:def 4

          .= (ff . (b,a)) by SteinGen;

          hence thesis;

        end;

        hence thesis by METRIC_1:def 4;

      end;

    end

    registration

      let X be non empty set, f be discerning symmetric triangle Reflexive Function of [:X, X:], REAL , p be Element of X;

      cluster ( SteinhausGen (f,p)) -> triangle;

      coherence

      proof

        set ff = ( SteinhausGen (f,p));

        for x,z,y be Element of X holds ((ff . (x,z)) + (ff . (z,y))) >= (ff . (x,y))

        proof

          let x,z,y be Element of X;

          set b = (2 * (f . (x,y)));

          set cc = (((f . (x,p)) + (f . (y,p))) + (f . (x,y)));

          set dxz = (2 * (f . (x,z)));

          set dyz = (2 * (f . (y,z)));

          set pp = (f . (x,y));

          set q = ((f . (x,y)) + ((f . (x,p)) + (f . (y,p))));

          set r = (((f . (x,z)) + (f . (y,z))) - (f . (x,y)));

          per cases ;

            suppose x = y;

            then

             F1: (ff . (x,y)) = 0 by METRIC_1:def 2;

            (ff . (x,z)) >= 0 & (ff . (z,y)) >= 0 by ZeZo;

            hence thesis by F1;

          end;

            suppose

             F0: x = z;

            then (ff . (x,z)) = 0 by METRIC_1:def 2;

            hence thesis by F0;

          end;

            suppose

             F0: y = z;

            then (ff . (y,z)) = 0 by METRIC_1:def 2;

            hence thesis by F0;

          end;

            suppose

             TT: x <> y & x <> z & y <> z;

            then

             TX: (f . (x,y)) > 0 by ME7;

            (f . (y,p)) = (f . (p,y)) by METRIC_1:def 4;

            then ((f . (x,p)) + (f . (y,p))) > 0 by TX, METRIC_1:def 5;

            then

             Y1: pp < q by XREAL_1: 29;

            

             E1: (f . (x,y)) > 0 by TT, ME7;

            (f . (y,z)) = (f . (z,y)) by METRIC_1:def 4;

            then (((f . (x,z)) + (f . (y,z))) - (f . (x,y))) >= ((f . (x,y)) - (f . (x,y))) by XREAL_1: 9, METRIC_1:def 5;

            then

             XX: (pp / cc) <= ((pp + r) / (cc + r)) by LemacikX1, Y1, E1;

            

             S3: (ff . (x,y)) = (b / cc) by SteinGen;

            (2 * (pp / cc)) <= (2 * (((f . (x,z)) + (f . (y,z))) / ((((f . (x,p)) + (f . (y,p))) + (f . (x,z))) + (f . (y,z))))) by XX, XREAL_1: 64;

            then (b / cc) <= (2 * (((f . (x,z)) + (f . (y,z))) / ((((f . (x,p)) + (f . (y,p))) + (f . (x,z))) + (f . (y,z))))) by XCMPLX_1: 74;

            then

             ds: (b / cc) <= ((2 * ((f . (x,z)) + (f . (y,z)))) / ((((f . (x,p)) + (f . (y,p))) + (f . (x,z))) + (f . (y,z)))) by XCMPLX_1: 74;

            

             Sc: (f . (x,z)) > 0 by ME7, TT;

            

             SC: (f . (y,z)) > 0 by TT, ME7;

            

             S0: ((dxz + dyz) / ((((f . (x,p)) + (f . (y,p))) + (f . (x,z))) + (f . (y,z)))) = ((dxz / ((((f . (x,p)) + (f . (y,p))) + (f . (x,z))) + (f . (y,z)))) + (dyz / ((((f . (x,p)) + (f . (y,p))) + (f . (x,z))) + (f . (y,z))))) by XCMPLX_1: 62;

            

             R1: (ff . (x,z)) = ((2 * (f . (x,z))) / (((f . (x,p)) + (f . (z,p))) + (f . (x,z)))) by SteinGen;

            (f . (z,y)) = (f . (y,z)) by METRIC_1:def 4;

            then (((f . (y,z)) + (f . (y,p))) - (f . (z,p))) >= ((f . (z,p)) - (f . (z,p))) by XREAL_1: 9, METRIC_1:def 5;

            then ((f . (x,z)) + (((f . (y,z)) + (f . (y,p))) - (f . (z,p)))) >= ((f . (x,z)) + 0 ) by XREAL_1: 6;

            then

             D1: (((f . (x,p)) + (f . (z,p))) + ((((f . (x,z)) + (f . (y,z))) + (f . (y,p))) - (f . (z,p)))) >= (((f . (x,p)) + (f . (z,p))) + (f . (x,z))) by XREAL_1: 6;

            

             ss: (f . (z,p)) = (f . (p,z)) by METRIC_1:def 4;

            then ((f . (x,p)) + (f . (z,p))) > 0 by Sc, METRIC_1:def 5;

            then

             W3: (dxz / ((((((f . (x,p)) + (f . (z,p))) + (f . (x,z))) + (f . (y,z))) + (f . (y,p))) - (f . (z,p)))) <= (dxz / (((f . (x,p)) + (f . (z,p))) + (f . (x,z)))) by D1, XREAL_1: 118, Sc;

            

             f2: ((f . (y,p)) + (f . (z,p))) > 0 by SC, METRIC_1:def 5, ss;

            (f . (x,z)) = (f . (z,x)) by METRIC_1:def 4;

            then (((f . (x,z)) + (f . (x,p))) - (f . (z,p))) >= ((f . (z,p)) - (f . (z,p))) by XREAL_1: 9, METRIC_1:def 5;

            then ((((f . (x,z)) + (f . (x,p))) - (f . (z,p))) + (f . (y,z))) >= ( 0 + (f . (y,z))) by XREAL_1: 6;

            then (((f . (y,p)) + (f . (z,p))) + ((((f . (y,z)) + (f . (x,z))) + (f . (x,p))) - (f . (z,p)))) >= (((f . (y,p)) + (f . (z,p))) + (f . (y,z))) by XREAL_1: 6;

            then

             w3: (dyz / ((((((f . (y,p)) + (f . (z,p))) + (f . (y,z))) + (f . (x,z))) + (f . (x,p))) - (f . (z,p)))) <= (dyz / (((f . (y,p)) + (f . (z,p))) + (f . (y,z)))) by XREAL_1: 118, f2, SC;

            

             R2: (ff . (z,y)) = ((2 * (f . (z,y))) / (((f . (z,p)) + (f . (y,p))) + (f . (z,y)))) by SteinGen;

            (f . (y,p)) = (f . (p,y)) & (f . (z,p)) = (f . (p,z)) & (f . (y,z)) = (f . (z,y)) by METRIC_1:def 4;

            then ((dxz + dyz) / ((((f . (x,p)) + (f . (y,p))) + (f . (x,z))) + (f . (y,z)))) <= ((ff . (x,z)) + (ff . (z,y))) by R1, W3, S0, XREAL_1: 7, w3, R2;

            hence thesis by S3, ds, XXREAL_0: 2;

          end;

        end;

        hence thesis by METRIC_1:def 5;

      end;

    end

    begin

    definition

      let X be finite set;

      :: ROUGHIF2:def11

      func SymmetricDiffDist X -> Function of [:( bool X), ( bool X):], REAL means

      : SymDist: for x,y be Subset of X holds (it . (x,y)) = ( card (x \+\ y));

      existence

      proof

        deffunc F( Subset of X, Subset of X) = ( In (( card ($1 \+\ $2)), REAL ));

        ex f be Function of [:( bool X), ( bool X):], REAL st for x,y be Element of ( bool X) holds (f . (x,y)) = F(x,y) from STACKS_1:sch 2;

        then

        consider f be Function of [:( bool X), ( bool X):], REAL such that

         A1: for x,y be Subset of X holds (f . (x,y)) = F(x,y);

        take f;

        let x,y be Subset of X;

        (f . (x,y)) = ( In (( card (x \+\ y)), REAL )) by A1

        .= ( card (x \+\ y));

        hence thesis;

      end;

      uniqueness

      proof

        deffunc F( Subset of X, Subset of X) = ( card ($1 \+\ $2));

        let f1,f2 be Function of [:( bool X), ( bool X):], REAL such that

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

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

        for x be Element of [:( bool X), ( bool X):] holds (f1 . x) = (f2 . x)

        proof

          let x be Element of [:( bool X), ( bool X):];

          consider x1,x2 be object such that

           A3: [x1, x2] = x by XTUPLE_0:def 1, CARDFIL4: 4;

          reconsider x1, x2 as Subset of X by ZFMISC_1: 87, A3;

          

           A5: ( card (x1 \+\ x2)) = (f1 . (x1,x2)) by A1

          .= (f1 . x) by A3;

          ( card (x1 \+\ x2)) = (f2 . (x1,x2)) by A2

          .= (f2 . x) by A3;

          hence thesis by A5;

        end;

        hence thesis;

      end;

    end

    registration

      let X be finite set;

      cluster ( SymmetricDiffDist X) -> Reflexive discerning symmetric triangle;

      coherence

      proof

        set f = ( SymmetricDiffDist X);

        for x be Element of ( bool X) holds (f . (x,x)) = 0

        proof

          let x be Element of ( bool X);

          (f . (x,x)) = ( card (x \+\ x)) by SymDist

          .= ( card ( {} X)) by XBOOLE_1: 92

          .= 0 ;

          hence thesis;

        end;

        hence f is Reflexive by METRIC_1:def 2;

        for a,b be Element of ( bool X) st (f . (a,b)) = 0 holds a = b

        proof

          let a,b be Subset of X;

          assume (f . (a,b)) = 0 ;

          then ( card (a \+\ b)) = 0 by SymDist;

          then (a \ b) = {} & (b \ a) = {} ;

          hence thesis by XBOOLE_1: 37;

        end;

        hence f is discerning by METRIC_1:def 3;

        for a,b be Element of ( bool X) holds (f . (a,b)) = (f . (b,a))

        proof

          let a,b be Subset of X;

          (f . (a,b)) = ( card (a \+\ b)) by SymDist

          .= (f . (b,a)) by SymDist;

          hence thesis;

        end;

        hence f is symmetric by METRIC_1:def 4;

        for a,b,c be Element of ( bool X) holds (f . (a,c)) <= ((f . (a,b)) + (f . (b,c)))

        proof

          let a,b,c be Element of ( bool X);

          

           B1: (f . (a,c)) = ( card (a \+\ c)) by SymDist;

          

           B2: (f . (a,b)) = ( card (a \+\ b)) by SymDist;

          

           B3: (f . (b,c)) = ( card (b \+\ c)) by SymDist;

          (a \+\ c) = ((a \+\ b) \+\ (b \+\ c)) by Jajo;

          then

           A1: ( card (a \+\ c)) <= ( card ((a \+\ b) \/ (b \+\ c))) by NAT_1: 43, Lack;

          ( card ((a \+\ b) \/ (b \+\ c))) <= (( card (a \+\ b)) + ( card (b \+\ c))) by CARD_2: 43;

          hence thesis by B1, B2, B3, A1, XXREAL_0: 2;

        end;

        hence thesis by METRIC_1:def 5;

      end;

    end

    definition

      let X be finite set;

      :: ROUGHIF2:def12

      func SymDifMetrSpace X -> MetrStruct equals MetrStruct (# ( bool X), ( SymmetricDiffDist X) #);

      coherence ;

    end

    registration

      let X be finite set;

      cluster ( SymDifMetrSpace X) -> non empty;

      coherence ;

    end

    registration

      let X be finite set;

      cluster ( SymDifMetrSpace X) -> Reflexive discerning symmetric triangle;

      coherence by METRIC_1:def 6, METRIC_1:def 7, METRIC_1:def 8, METRIC_1:def 9;

    end

    begin

    theorem :: ROUGHIF2:44

    

     Similar2: for R be finite set holds for A,B be Subset of R holds (( JaccardDist R) . (A,B)) = (( card (A \+\ B)) / ( card (A \/ B)))

    proof

      let R be finite set;

      let A,B be Subset of R;

      per cases ;

        suppose

         A1: (A \/ B) <> {} ;

        (( JaccardDist R) . (A,B)) = (1 - ( JaccardIndex (A,B))) by JacDef2

        .= (1 - (( card (A /\ B)) / ( card (A \/ B)))) by JacInd, A1

        .= (( card (A \+\ B)) / ( card (A \/ B))) by A1, Lemacik;

        hence thesis;

      end;

        suppose

         A1: (A \/ B) = {} ;

        (( JaccardDist R) . (A,B)) = (1 - ( JaccardIndex (A,B))) by JacDef2

        .= (1 - 1) by JacInd, A1

        .= (( card (A \+\ B)) / ( card (A \/ B))) by A1;

        hence thesis;

      end;

    end;

    theorem :: ROUGHIF2:45

    

     LastLemma: for X be finite set holds ( JaccardDist X) = ( SteinhausGen (( SymmetricDiffDist X),( {} X)))

    proof

      let X be finite set;

      set f = ( JaccardDist X);

      set g = ( SteinhausGen (( SymmetricDiffDist X),( {} X)));

      for x be Element of [:( bool X), ( bool X):] holds (f . x) = (g . x)

      proof

        let x be Element of [:( bool X), ( bool X):];

        consider x1,x2 be object such that

         T1: x1 in ( bool X) & x2 in ( bool X) & x = [x1, x2] by ZFMISC_1:def 2;

        reconsider x1, x2 as Subset of X by T1;

        set h = ( SymmetricDiffDist X);

        set p = ( {} X);

        

         V1: (h . (x1,p)) = ( card (x1 \+\ p)) by SymDist

        .= ( card x1);

        

         V2: (h . (x2,p)) = ( card (x2 \+\ p)) by SymDist

        .= ( card x2);

        

         V3: (h . (x1,x2)) = ( card (x1 \+\ x2)) by SymDist;

        

         nn: (g . (x1,x2)) = ((2 * ( card (x1 \+\ x2))) / ((( card x1) + ( card x2)) + ( card (x1 \+\ x2)))) by V3, V2, V1, SteinGen;

        (f . (x1,x2)) = (( card (x1 \+\ x2)) / ( card (x1 \/ x2))) by Similar2

        .= (g . (x1,x2)) by HoHo, nn;

        hence thesis by T1;

      end;

      hence thesis;

    end;

    begin

    registration

      let M be finite non empty MetrSpace;

      cluster the distance of M -> symmetric Reflexive discerning triangle;

      coherence by METRIC_1:def 9, METRIC_1:def 6, METRIC_1:def 7, METRIC_1:def 8;

    end

    definition

      let M be finite non empty MetrStruct, p be Element of M;

      :: ROUGHIF2:def13

      func SteinhausMetrSpace (M,p) -> MetrStruct equals MetrStruct (# the carrier of M, ( SteinhausGen (the distance of M,p)) #);

      coherence ;

    end

    definition

      let M be MetrStruct;

      :: ROUGHIF2:def14

      attr M is with_nonnegative_distance means

      : NonDist: the distance of M is nonnegative-yielding;

    end

    registration

      let A be finite non empty set;

      cluster ( discrete_dist A) -> finite non empty nonnegative-yielding;

      coherence

      proof

        set S = ( DiscreteSpace A);

        for x,y be Element of A holds (( discrete_dist A) . (x,y)) >= 0

        proof

          let x,y be Element of A;

          per cases ;

            suppose x = y;

            hence thesis by METRIC_1:def 10;

          end;

            suppose x <> y;

            hence thesis by METRIC_1:def 10;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      cluster finite non empty with_nonnegative_distance for MetrSpace;

      existence

      proof

        set A = the finite non empty set;

        take S = ( DiscreteSpace A);

        S = MetrStruct (# A, ( discrete_dist A) #) by METRIC_1:def 11;

        hence thesis;

      end;

    end

    registration

      let M be finite non empty with_nonnegative_distance MetrStruct, p be Element of M;

      cluster ( SteinhausMetrSpace (M,p)) -> with_nonnegative_distance;

      coherence

      proof

        the distance of M is nonnegative-yielding by NonDist;

        hence thesis;

      end;

    end

    registration

      let M be finite non empty with_nonnegative_distance discerning MetrStruct, p be Element of M;

      cluster ( SteinhausMetrSpace (M,p)) -> discerning;

      coherence

      proof

        the distance of M is nonnegative-yielding discerning by NonDist, METRIC_1:def 7;

        hence thesis by METRIC_1:def 7;

      end;

    end

    registration

      let M be finite non empty with_nonnegative_distance Reflexive MetrStruct, p be Element of M;

      cluster ( SteinhausMetrSpace (M,p)) -> Reflexive;

      coherence

      proof

        the distance of M is nonnegative-yielding Reflexive by NonDist, METRIC_1:def 6;

        hence thesis by METRIC_1:def 6;

      end;

    end

    registration

      let M be finite non empty with_nonnegative_distance symmetric MetrStruct, p be Element of M;

      cluster ( SteinhausMetrSpace (M,p)) -> symmetric;

      coherence

      proof

        the distance of M is nonnegative-yielding symmetric by NonDist, METRIC_1:def 8;

        hence thesis by METRIC_1:def 8;

      end;

    end

    registration

      let M be finite non empty discerning symmetric Reflexive triangle MetrStruct, p be Element of M;

      cluster ( SteinhausMetrSpace (M,p)) -> triangle;

      coherence by METRIC_1:def 9;

    end

    registration

      let R be finite 1-sorted;

      cluster ( MarczewskiDistance R) -> Reflexive discerning symmetric;

      coherence

      proof

        set f = ( MarczewskiDistance R);

        for a be Subset of R holds (f . (a,a)) = 0

        proof

          let a be Subset of R;

          (f . (a,a)) = (1 - ( JaccardIndex (a,a))) by JacDef2

          .= (1 - 1) by JacRefl;

          hence thesis;

        end;

        hence f is Reflexive by METRIC_1:def 2;

        

         a1: for a,b be Subset of R st (f . (a,b)) = 0 holds a = b

        proof

          let a,b be Subset of R;

          assume (f . (a,b)) = 0 ;

          then (1 - ( JaccardIndex (a,b))) = 0 by JacDef2;

          hence thesis by JacRefl;

        end;

        set A = ( bool the carrier of R);

        for a,b be Element of A holds (f . (a,b)) = (f . (b,a))

        proof

          let a,b be Element of A;

          (f . (a,b)) = (1 - ( JaccardIndex (a,b))) by JacDef2

          .= (1 - ( JaccardIndex (b,a))) by JacSym

          .= (f . (b,a)) by JacDef2;

          hence thesis;

        end;

        hence thesis by a1, METRIC_1:def 4, METRIC_1:def 3;

      end;

    end

    theorem :: ROUGHIF2:46

    for R be finite Approximation_Space holds for A,B be Subset of R holds (( MarczewskiDistance R) . (A,B)) = (( delta_1 R) . (A,B))

    proof

      let R be finite Approximation_Space;

      let A,B be Subset of R;

      (( MarczewskiDistance R) . (A,B)) = (( card (A \+\ B)) / ( card (A \/ B))) by Similar2;

      hence thesis by For191;

    end;

    registration

      let R be finite 1-sorted;

      cluster ( MarczewskiDistance R) -> triangle;

      coherence

      proof

        set A = ( bool the carrier of R);

        set B = ( [#] R);

        set ff = ( SymmetricDiffDist ( [#] R));

        set p = ( {} B);

        ( JaccardDist B) = ( SteinhausGen (ff,p)) by LastLemma;

        hence thesis;

      end;

    end