roughs_1.miz



    begin

    registration

      let A be set;

      cluster RelStr (# A, ( id A) #) -> discrete;

      coherence by ORDERS_3:def 1;

    end

    theorem :: ROUGHS_1:1

    

     Th1: for X be set st ( Total X) c= ( id X) holds X is trivial

    proof

      let X be set;

      assume

       A1: ( Total X) c= ( id X);

      assume X is non trivial;

      then

      consider x,y be object such that

       A2: x in X & y in X and

       A3: x <> y by ZFMISC_1:def 10;

       [x, y] in ( Total X) by A2, TOLER_1: 2;

      hence thesis by A1, A3, RELAT_1:def 10;

    end;

    definition

      let A be RelStr;

      :: ROUGHS_1:def1

      attr A is diagonal means

      : Def1: the InternalRel of A c= ( id the carrier of A);

    end

    registration

      let A be non trivial set;

      cluster RelStr (# A, ( Total A) #) -> non diagonal;

      coherence by Th1;

    end

    theorem :: ROUGHS_1:2

    for L be reflexive RelStr holds ( id the carrier of L) c= the InternalRel of L

    proof

      let L be reflexive RelStr;

      for a,b be object st [a, b] in ( id the carrier of L) holds [a, b] in the InternalRel of L

      proof

        let a,b be object;

        assume [a, b] in ( id the carrier of L);

        then

         A1: a = b & a in the carrier of L by RELAT_1:def 10;

        the InternalRel of L is_reflexive_in the carrier of L by ORDERS_2:def 2;

        hence thesis by A1, RELAT_2:def 1;

      end;

      hence thesis by RELAT_1:def 3;

    end;

    

     Lm1: for A be RelStr st A is reflexive trivial holds A is discrete

    proof

      let A be RelStr;

      assume

       A1: A is reflexive trivial;

      per cases by A1, ZFMISC_1: 131;

        suppose

         A2: the carrier of A is empty;

        then the InternalRel of A = {} ;

        hence thesis by A2, ORDERS_3:def 1, RELAT_1: 55;

      end;

        suppose ex x be object st the carrier of A = {x};

        then

        consider x be object such that

         A3: the carrier of A = {x};

        the InternalRel of A c= [: {x}, {x}:] by A3;

        then the InternalRel of A c= { [x, x]} by ZFMISC_1: 29;

        then

         A4: the InternalRel of A = { [x, x]} or the InternalRel of A = {} by ZFMISC_1: 33;

        

         A5: the InternalRel of A is_reflexive_in the carrier of A by A1, ORDERS_2:def 2;

        x in the carrier of A by A3, TARSKI:def 1;

        then the InternalRel of A = ( id {x}) by A4, A5, RELAT_2:def 1, SYSREL: 13;

        hence thesis by A3, ORDERS_3:def 1;

      end;

    end;

    registration

      cluster non discrete -> non trivial for reflexive RelStr;

      coherence by Lm1;

      cluster reflexive trivial -> discrete for RelStr;

      coherence ;

    end

    theorem :: ROUGHS_1:3

    for X be set, R be Relation of X holds R is total reflexive iff ( id X) c= R

    proof

      let X be set, R be Relation of X;

      hereby

        assume R is total reflexive;

        then

         A1: ( dom R) = X & ( id ( field R)) c= R by PARTFUN1:def 2, RELAT_2: 1;

        then ( field R) = (X \/ ( rng R)) by RELAT_1:def 6;

        hence ( id X) c= R by A1, XBOOLE_1: 12;

      end;

      assume

       A2: ( id X) c= R;

      ( field R) c= (X \/ X) by RELSET_1: 8;

      then ( id ( field R)) c= ( id X) by FUNCT_4: 3;

      then

       A3: ( id ( field R)) c= R by A2;

      ( dom ( id X)) c= ( dom R) by A2, RELAT_1: 11;

      hence thesis by A3, XBOOLE_0:def 10, RELAT_2: 1, PARTFUN1:def 2;

    end;

    

     Lm2: for A be RelStr st A is discrete holds A is diagonal by ORDERS_3:def 1;

    registration

      cluster discrete -> diagonal for RelStr;

      coherence by Lm2;

      cluster non diagonal -> non discrete for RelStr;

      coherence ;

    end

    registration

      cluster non diagonal non empty for RelStr;

      existence

      proof

        set A = the non trivial set;

        take RelStr (# A, ( Total A) #);

        thus thesis;

      end;

    end

    theorem :: ROUGHS_1:4

    

     Th4: for A be non diagonal non empty RelStr holds ex x,y be Element of A st x <> y & [x, y] in the InternalRel of A

    proof

      let A be non diagonal non empty RelStr;

      now

        assume

         A1: for x,y be Element of A st [x, y] in the InternalRel of A holds x = y;

        for a,b be object st [a, b] in the InternalRel of A holds [a, b] in ( id the carrier of A)

        proof

          let a,b be object;

          assume

           A2: [a, b] in the InternalRel of A;

          then

           A3: a is Element of A by ZFMISC_1: 87;

          b is Element of A by A2, ZFMISC_1: 87;

          then a = b by A1, A2, A3;

          hence thesis by A3, RELAT_1:def 10;

        end;

        then the InternalRel of A c= ( id the carrier of A) by RELAT_1:def 3;

        hence thesis by Def1;

      end;

      hence thesis;

    end;

    theorem :: ROUGHS_1:5

    

     Th5: for D be set, p,q be FinSequence of D holds ( Union (p ^ q)) = (( Union p) \/ ( Union q))

    proof

      let D be set, p,q be FinSequence of D;

      ( union ( rng (p ^ q))) = ( union (( rng p) \/ ( rng q))) by FINSEQ_1: 31

      .= (( Union p) \/ ( Union q)) by ZFMISC_1: 78;

      hence thesis;

    end;

    theorem :: ROUGHS_1:6

    

     Th6: for p,q be Function st q is disjoint_valued & p c= q holds p is disjoint_valued

    proof

      let p,q be Function;

      assume that

       A1: q is disjoint_valued and

       A2: p c= q;

      for x,y be object st x <> y holds (p . x) misses (p . y)

      proof

        let x,y be object;

        assume

         A3: x <> y;

        assume

         A4: (p . x) meets (p . y);

        x in ( dom p) & y in ( dom p)

        proof

          assume not x in ( dom p) or not y in ( dom p);

          then (p . x) = {} or (p . y) = {} by FUNCT_1:def 2;

          hence thesis by A4;

        end;

        then (p . x) = (q . x) & (p . y) = (q . y) by A2, GRFUNC_1: 2;

        hence thesis by A1, A3, A4;

      end;

      hence thesis;

    end;

    registration

      cluster empty -> disjoint_valued for Function;

      coherence

      proof

        let X be Function;

        assume

         A1: X is empty;

        let x,y be object;

        assume x <> y;

        (X . x) = {} by A1, FUNCT_1:def 2, RELAT_1: 38;

        hence thesis;

      end;

    end

    registration

      let A be set;

      cluster disjoint_valued for FinSequence of A;

      existence

      proof

        set X = ( <*> A);

        X is disjoint_valued;

        hence thesis;

      end;

    end

    registration

      let A be non empty set;

      cluster non empty disjoint_valued for FinSequence of A;

      existence

      proof

        set a = the Element of A;

        reconsider X = (1 |-> a) as FinSequence of A;

        

         A1: X is disjoint_valued

        proof

          let x,y be object;

          assume

           A2: x <> y;

          per cases ;

            suppose

             A3: x in ( dom X) & y in ( dom X);

            then x in ( Seg 1) by FUNCOP_1: 13;

            then

             A4: x = 1 by FINSEQ_1: 2, TARSKI:def 1;

            y in ( Seg 1) by A3, FUNCOP_1: 13;

            hence thesis by A2, A4, FINSEQ_1: 2, TARSKI:def 1;

          end;

            suppose not x in ( dom X) or not y in ( dom X);

            then (X . x) = {} or (X . y) = {} by FUNCT_1:def 2;

            hence thesis;

          end;

        end;

        X is non empty by FUNCOP_1: 13, RELAT_1: 38;

        hence thesis by A1;

      end;

    end

    definition

      let A be set;

      let X be FinSequence of ( bool A);

      let n be Nat;

      :: original: .

      redefine

      func X . n -> Subset of A ;

      coherence

      proof

        per cases ;

          suppose not n in ( dom X);

          then (X . n) = {} by FUNCT_1:def 2;

          hence thesis by XBOOLE_1: 2;

        end;

          suppose n in ( dom X);

          hence thesis by FINSEQ_2: 11;

        end;

      end;

    end

    definition

      let A be set;

      let X be FinSequence of ( bool A);

      :: original: Union

      redefine

      func Union X -> Subset of A ;

      coherence

      proof

        ( union ( rng X)) c= A

        proof

          let x be object;

          assume x in ( union ( rng X));

          then ex Y be set st x in Y & Y in ( rng X) by TARSKI:def 4;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    registration

      let A be finite set;

      let R be Relation of A;

      cluster RelStr (# A, R #) -> finite;

      coherence ;

    end

    theorem :: ROUGHS_1:7

    

     Th7: for X be set, x,y be object, T be Tolerance of X st x in ( Class (T,y)) holds y in ( Class (T,x))

    proof

      let X be set, x,y be object, T be Tolerance of X;

      assume x in ( Class (T,y));

      then [x, y] in T by EQREL_1: 19;

      then [y, x] in T by EQREL_1: 6;

      hence thesis by EQREL_1: 19;

    end;

    begin

    definition

      let P be RelStr;

      :: ROUGHS_1:def2

      attr P is with_equivalence means

      : Def2: the InternalRel of P is Equivalence_Relation of the carrier of P;

      :: ROUGHS_1:def3

      attr P is with_tolerance means

      : Def3: the InternalRel of P is Tolerance of the carrier of P;

    end

    registration

      cluster with_equivalence -> with_tolerance for RelStr;

      coherence ;

    end

    registration

      let A be set;

      cluster RelStr (# A, ( id A) #) -> with_equivalence;

      coherence ;

    end

    registration

      cluster discrete finite with_equivalence non empty for RelStr;

      existence

      proof

        set E = RelStr (# { {} }, ( id { {} }) #);

        E is discrete;

        hence thesis;

      end;

      cluster non diagonal finite with_equivalence non empty for RelStr;

      existence

      proof

        set C = { 0 , 1};

        set R = ( Total C);

        set E = RelStr (# C, R #);

        reconsider E as non empty RelStr;

        E is with_equivalence & C is non trivial by CHAIN_1: 3;

        hence thesis;

      end;

    end

    definition

      mode Approximation_Space is with_equivalence non empty RelStr;

      mode Tolerance_Space is with_tolerance non empty RelStr;

    end

    registration

      let A be Tolerance_Space;

      cluster the InternalRel of A -> total reflexive symmetric;

      coherence by Def3;

    end

    registration

      let A be Approximation_Space;

      cluster the InternalRel of A -> transitive;

      coherence by Def2;

    end

    definition

      let A be non empty RelStr;

      let X be Subset of A;

      :: ROUGHS_1:def4

      func LAp X -> Subset of A equals { x where x be Element of A : ( Class (the InternalRel of A,x)) c= X };

      coherence

      proof

        { x where x be Element of A : ( Class (the InternalRel of A,x)) c= X } c= the carrier of A

        proof

          let y be object;

          assume y in { x where x be Element of A : ( Class (the InternalRel of A,x)) c= X };

          then ex x be Element of A st y = x & ( Class (the InternalRel of A,x)) c= X;

          hence thesis;

        end;

        hence thesis;

      end;

      :: ROUGHS_1:def5

      func UAp X -> Subset of A equals { x where x be Element of A : ( Class (the InternalRel of A,x)) meets X };

      coherence

      proof

        { x where x be Element of A : ( Class (the InternalRel of A,x)) meets X } c= the carrier of A

        proof

          let y be object;

          assume y in { x where x be Element of A : ( Class (the InternalRel of A,x)) meets X };

          then ex x be Element of A st y = x & ( Class (the InternalRel of A,x)) meets X;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    definition

      let A be non empty RelStr;

      let X be Subset of A;

      :: ROUGHS_1:def6

      func BndAp X -> Subset of A equals (( UAp X) \ ( LAp X));

      coherence ;

    end

    definition

      let A be non empty RelStr;

      let X be Subset of A;

      :: ROUGHS_1:def7

      attr X is rough means ( BndAp X) <> {} ;

    end

    notation

      let A be non empty RelStr;

      let X be Subset of A;

      antonym X is exact for X is rough;

    end

    reserve A for Tolerance_Space,

X,Y for Subset of A;

    theorem :: ROUGHS_1:8

    

     Th8: for x be object st x in ( LAp X) holds ( Class (the InternalRel of A,x)) c= X

    proof

      let x be object;

      assume x in ( LAp X);

      then ex x1 be Element of A st x = x1 & ( Class (the InternalRel of A,x1)) c= X;

      hence thesis;

    end;

    theorem :: ROUGHS_1:9

    for x be Element of A st ( Class (the InternalRel of A,x)) c= X holds x in ( LAp X);

    theorem :: ROUGHS_1:10

    

     Th10: for x be set st x in ( UAp X) holds ( Class (the InternalRel of A,x)) meets X

    proof

      let x be set;

      assume x in ( UAp X);

      then ex x1 be Element of A st x = x1 & ( Class (the InternalRel of A,x1)) meets X;

      hence thesis;

    end;

    theorem :: ROUGHS_1:11

    for x be Element of A st ( Class (the InternalRel of A,x)) meets X holds x in ( UAp X);

    theorem :: ROUGHS_1:12

    

     Th12: ( LAp X) c= X

    proof

      let x be object;

      assume x in ( LAp X);

      then

      consider y be Element of A such that

       A1: y = x & ( Class (the InternalRel of A,y)) c= X;

      y in ( Class (the InternalRel of A,y)) by EQREL_1: 20;

      hence thesis by A1;

    end;

    theorem :: ROUGHS_1:13

    

     Th13: X c= ( UAp X)

    proof

      let x be object;

      assume

       A1: x in X;

      then

      reconsider x9 = x as Element of A;

      x9 in ( Class (the InternalRel of A,x9)) by EQREL_1: 20;

      then ( Class (the InternalRel of A,x9)) meets X by A1, XBOOLE_0: 3;

      hence thesis;

    end;

    theorem :: ROUGHS_1:14

    

     Th14: ( LAp X) c= ( UAp X)

    proof

      ( LAp X) c= X & X c= ( UAp X) by Th12, Th13;

      hence thesis;

    end;

    theorem :: ROUGHS_1:15

    

     Th15: X is exact iff ( LAp X) = X

    proof

      

       A1: ( LAp X) c= ( UAp X) by Th14;

      hereby

        assume X is exact;

        then ( BndAp X) = {} ;

        then ( UAp X) c= ( LAp X) by XBOOLE_1: 37;

        then ( UAp X) = ( LAp X) by A1;

        then

         A2: X c= ( LAp X) by Th13;

        ( LAp X) c= X by Th12;

        hence ( LAp X) = X by A2;

      end;

      assume

       A3: ( LAp X) = X;

      ( UAp X) c= X

      proof

        let y be object;

        assume y in ( UAp X);

        then ( Class (the InternalRel of A,y)) meets X by Th10;

        then

        consider z be object such that

         A4: z in ( Class (the InternalRel of A,y)) & z in ( LAp X) by A3, XBOOLE_0: 3;

        ( Class (the InternalRel of A,z)) c= X & y in ( Class (the InternalRel of A,z)) by A4, Th7, Th8;

        hence thesis;

      end;

      then ( BndAp X) = {} by A3, XBOOLE_1: 37;

      hence thesis;

    end;

    theorem :: ROUGHS_1:16

    

     Th16: X is exact iff ( UAp X) = X

    proof

      hereby

        assume X is exact;

        then ( BndAp X) = {} ;

        then

         A1: ( UAp X) c= ( LAp X) by XBOOLE_1: 37;

        

         A2: X c= ( UAp X) by Th13;

        ( LAp X) c= X by Th12;

        then ( UAp X) c= X by A1;

        hence ( UAp X) = X by A2;

      end;

      assume

       A3: ( UAp X) = X;

      X c= ( LAp X)

      proof

        let x be object;

        assume

         A4: x in X;

        ( Class (the InternalRel of A,x)) c= X

        proof

          let y be object;

          assume

           A5: y in ( Class (the InternalRel of A,x));

          then [y, x] in the InternalRel of A by EQREL_1: 19;

          then [x, y] in the InternalRel of A by EQREL_1: 6;

          then x in ( Class (the InternalRel of A,y)) by EQREL_1: 19;

          then ( Class (the InternalRel of A,y)) meets X by A4, XBOOLE_0: 3;

          hence thesis by A3, A5;

        end;

        hence thesis by A4;

      end;

      then ( BndAp X) = {} by A3, XBOOLE_1: 37;

      hence thesis;

    end;

    theorem :: ROUGHS_1:17

    X = ( LAp X) iff X = ( UAp X) by Th15, Th16;

    theorem :: ROUGHS_1:18

    

     Th18: ( LAp ( {} A)) = {}

    proof

      assume ( LAp ( {} A)) <> {} ;

      then

      consider x be object such that

       A1: x in ( LAp ( {} A)) by XBOOLE_0:def 1;

      ex y be Element of A st y = x & ( Class (the InternalRel of A,y)) c= ( {} A) by A1;

      hence thesis by EQREL_1: 20;

    end;

    theorem :: ROUGHS_1:19

    

     Th19: ( UAp ( {} A)) = {}

    proof

      assume ( UAp ( {} A)) <> {} ;

      then

      consider x be object such that

       A1: x in ( UAp ( {} A)) by XBOOLE_0:def 1;

      ex y be Element of A st y = x & ( Class (the InternalRel of A,y)) meets ( {} A) by A1;

      hence thesis;

    end;

    theorem :: ROUGHS_1:20

    

     Th20: ( LAp ( [#] A)) = ( [#] A)

    proof

      thus ( LAp ( [#] A)) c= ( [#] A);

      let x be object;

      

       A1: ( Class (the InternalRel of A,x)) c= ( [#] A);

      assume x in ( [#] A);

      hence thesis by A1;

    end;

    theorem :: ROUGHS_1:21

    ( UAp ( [#] A)) = ( [#] A)

    proof

      ( LAp ( [#] A)) c= ( UAp ( [#] A)) by Th14;

      then ( [#] A) c= ( UAp ( [#] A)) by Th20;

      hence thesis;

    end;

    theorem :: ROUGHS_1:22

    ( LAp (X /\ Y)) = (( LAp X) /\ ( LAp Y))

    proof

      thus ( LAp (X /\ Y)) c= (( LAp X) /\ ( LAp Y))

      proof

        let x be object;

        assume

         A1: x in ( LAp (X /\ Y));

        then ( Class (the InternalRel of A,x)) c= Y by Th8, XBOOLE_1: 18;

        then

         A2: x in ( LAp Y) by A1;

        ( Class (the InternalRel of A,x)) c= X by A1, Th8, XBOOLE_1: 18;

        then x in ( LAp X) by A1;

        hence thesis by A2, XBOOLE_0:def 4;

      end;

      let x be object;

      assume

       A3: x in (( LAp X) /\ ( LAp Y));

      then x in ( LAp Y) by XBOOLE_0:def 4;

      then

       A4: ( Class (the InternalRel of A,x)) c= Y by Th8;

      x in ( LAp X) by A3, XBOOLE_0:def 4;

      then ( Class (the InternalRel of A,x)) c= X by Th8;

      then ( Class (the InternalRel of A,x)) c= (X /\ Y) by A4, XBOOLE_1: 19;

      hence thesis by A3;

    end;

    theorem :: ROUGHS_1:23

    ( UAp (X \/ Y)) = (( UAp X) \/ ( UAp Y))

    proof

      thus ( UAp (X \/ Y)) c= (( UAp X) \/ ( UAp Y))

      proof

        let x be object;

        assume

         A1: x in ( UAp (X \/ Y));

        then ( Class (the InternalRel of A,x)) meets (X \/ Y) by Th10;

        then ( Class (the InternalRel of A,x)) meets X or ( Class (the InternalRel of A,x)) meets Y by XBOOLE_1: 70;

        then x in ( UAp X) or x in ( UAp Y) by A1;

        hence thesis by XBOOLE_0:def 3;

      end;

      let x be object;

      assume

       A2: x in (( UAp X) \/ ( UAp Y));

      then x in ( UAp X) or x in ( UAp Y) by XBOOLE_0:def 3;

      then ( Class (the InternalRel of A,x)) meets X or ( Class (the InternalRel of A,x)) meets Y by Th10;

      then ( Class (the InternalRel of A,x)) meets (X \/ Y) by XBOOLE_1: 70;

      hence thesis by A2;

    end;

    theorem :: ROUGHS_1:24

    

     Th24: X c= Y implies ( LAp X) c= ( LAp Y)

    proof

      assume

       A1: X c= Y;

      let x be object;

      assume

       A2: x in ( LAp X);

      then ( Class (the InternalRel of A,x)) c= X by Th8;

      then ( Class (the InternalRel of A,x)) c= Y by A1;

      hence thesis by A2;

    end;

    theorem :: ROUGHS_1:25

    

     Th25: X c= Y implies ( UAp X) c= ( UAp Y)

    proof

      assume

       A1: X c= Y;

      let x be object;

      assume

       A2: x in ( UAp X);

      then ( Class (the InternalRel of A,x)) meets X by Th10;

      then ( Class (the InternalRel of A,x)) meets Y by A1, XBOOLE_1: 63;

      hence thesis by A2;

    end;

    theorem :: ROUGHS_1:26

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

    proof

      let x be object;

      assume

       A1: x in (( LAp X) \/ ( LAp Y));

      per cases by A1, XBOOLE_0:def 3;

        suppose x in ( LAp X);

        then ( Class (the InternalRel of A,x)) c= (X \/ Y) by Th8, XBOOLE_1: 10;

        hence thesis by A1;

      end;

        suppose x in ( LAp Y);

        then ( Class (the InternalRel of A,x)) c= (X \/ Y) by Th8, XBOOLE_1: 10;

        hence thesis by A1;

      end;

    end;

    theorem :: ROUGHS_1:27

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

    proof

      let x be object;

      assume

       A1: x in ( UAp (X /\ Y));

      then ( Class (the InternalRel of A,x)) meets Y by Th10, XBOOLE_1: 74;

      then

       A2: x in ( UAp Y) by A1;

      ( Class (the InternalRel of A,x)) meets X by A1, Th10, XBOOLE_1: 74;

      then x in ( UAp X) by A1;

      hence thesis by A2, XBOOLE_0:def 4;

    end;

    theorem :: ROUGHS_1:28

    

     Th28: ( LAp (X ` )) = (( UAp X) ` )

    proof

      ( LAp (X ` )) misses ( UAp X)

      proof

        assume ( LAp (X ` )) meets ( UAp X);

        then

        consider x be object such that

         A1: x in ( LAp (X ` )) & x in ( UAp X) by XBOOLE_0: 3;

        ( Class (the InternalRel of A,x)) meets X & ( Class (the InternalRel of A,x)) c= (X ` ) by A1, Th8, Th10;

        hence thesis by XBOOLE_1: 63, XBOOLE_1: 79;

      end;

      hence ( LAp (X ` )) c= (( UAp X) ` ) by SUBSET_1: 23;

      let x be object;

      assume

       A2: x in (( UAp X) ` );

      then not x in ( UAp X) by XBOOLE_0:def 5;

      then ( Class (the InternalRel of A,x)) misses X by A2;

      then ( Class (the InternalRel of A,x)) c= (X ` ) by SUBSET_1: 23;

      hence thesis by A2;

    end;

    theorem :: ROUGHS_1:29

    

     Th29: ( UAp (X ` )) = (( LAp X) ` )

    proof

      ((( UAp (X ` )) ` ) ` ) = (( LAp ((X ` ) ` )) ` ) by Th28;

      hence thesis;

    end;

    theorem :: ROUGHS_1:30

    ( UAp ( LAp ( UAp X))) = ( UAp X)

    proof

      thus ( UAp ( LAp ( UAp X))) c= ( UAp X)

      proof

        let x be object;

        assume x in ( UAp ( LAp ( UAp X)));

        then ( Class (the InternalRel of A,x)) meets ( LAp ( UAp X)) by Th10;

        then

        consider y be object such that

         A1: y in ( Class (the InternalRel of A,x)) and

         A2: y in ( LAp ( UAp X)) by XBOOLE_0: 3;

         [y, x] in the InternalRel of A by A1, EQREL_1: 19;

        then [x, y] in the InternalRel of A by EQREL_1: 6;

        then

         A3: x in ( Class (the InternalRel of A,y)) by EQREL_1: 19;

        ( Class (the InternalRel of A,y)) c= ( UAp X) by A2, Th8;

        hence thesis by A3;

      end;

      X c= ( LAp ( UAp X))

      proof

        let x be object;

        assume

         A4: x in X;

        ( Class (the InternalRel of A,x)) c= ( UAp X)

        proof

          let y be object;

          assume

           A5: y in ( Class (the InternalRel of A,x));

          then [y, x] in the InternalRel of A by EQREL_1: 19;

          then [x, y] in the InternalRel of A by EQREL_1: 6;

          then x in ( Class (the InternalRel of A,y)) by EQREL_1: 19;

          then ( Class (the InternalRel of A,y)) meets X by A4, XBOOLE_0: 3;

          hence thesis by A5;

        end;

        hence thesis by A4;

      end;

      hence ( UAp X) c= ( UAp ( LAp ( UAp X))) by Th25;

    end;

    theorem :: ROUGHS_1:31

    ( LAp ( UAp ( LAp X))) = ( LAp X)

    proof

      ( UAp ( LAp X)) c= X

      proof

        let y be object;

        assume y in ( UAp ( LAp X));

        then ( Class (the InternalRel of A,y)) meets ( LAp X) by Th10;

        then

        consider z be object such that

         A1: z in ( Class (the InternalRel of A,y)) and

         A2: z in ( LAp X) by XBOOLE_0: 3;

         [z, y] in the InternalRel of A by A1, EQREL_1: 19;

        then [y, z] in the InternalRel of A by EQREL_1: 6;

        then

         A3: y in ( Class (the InternalRel of A,z)) by EQREL_1: 19;

        ( Class (the InternalRel of A,z)) c= X by A2, Th8;

        hence thesis by A3;

      end;

      hence ( LAp ( UAp ( LAp X))) c= ( LAp X) by Th24;

      thus ( LAp X) c= ( LAp ( UAp ( LAp X)))

      proof

        let x be object;

        assume

         A4: x in ( LAp X);

        ( Class (the InternalRel of A,x)) c= ( UAp ( LAp X))

        proof

          let y be object;

          assume

           A5: y in ( Class (the InternalRel of A,x));

          then [y, x] in the InternalRel of A by EQREL_1: 19;

          then [x, y] in the InternalRel of A by EQREL_1: 6;

          then x in ( Class (the InternalRel of A,y)) by EQREL_1: 19;

          then ( Class (the InternalRel of A,y)) meets ( LAp X) by A4, XBOOLE_0: 3;

          hence thesis by A5;

        end;

        hence thesis by A4;

      end;

    end;

    theorem :: ROUGHS_1:32

    ( BndAp X) = ( BndAp (X ` ))

    proof

      thus ( BndAp X) c= ( BndAp (X ` ))

      proof

        let x be object;

        assume

         A1: x in ( BndAp X);

        then x in ( UAp X) by XBOOLE_0:def 5;

        then not x in (( UAp X) ` ) by XBOOLE_0:def 5;

        then

         A2: not x in ( LAp (X ` )) by Th28;

         not x in ( LAp X) by A1, XBOOLE_0:def 5;

        then x in (( LAp X) ` ) by A1, XBOOLE_0:def 5;

        then x in ( UAp (X ` )) by Th29;

        hence thesis by A2, XBOOLE_0:def 5;

      end;

      thus ( BndAp (X ` )) c= ( BndAp X)

      proof

        let x be object;

        assume

         A3: x in ( BndAp (X ` ));

        then x in ( UAp (X ` )) by XBOOLE_0:def 5;

        then x in (( LAp X) ` ) by Th29;

        then

         A4: not x in ( LAp X) by XBOOLE_0:def 5;

         not x in ( LAp (X ` )) by A3, XBOOLE_0:def 5;

        then not x in (( UAp X) ` ) by Th28;

        then x in ((( UAp X) ` ) ` ) by A3, SUBSET_1: 29;

        hence thesis by A4, XBOOLE_0:def 5;

      end;

    end;

    reserve A for Approximation_Space,

X for Subset of A;

    theorem :: ROUGHS_1:33

    ( LAp ( LAp X)) = ( LAp X)

    proof

      thus ( LAp ( LAp X)) c= ( LAp X) by Th12;

      let x be object;

      assume

       A1: x in ( LAp X);

      then

       A2: ( Class (the InternalRel of A,x)) c= X by Th8;

      ( Class (the InternalRel of A,x)) c= ( LAp X)

      proof

        let y be object;

        assume

         A3: y in ( Class (the InternalRel of A,x));

        then ( Class (the InternalRel of A,x)) = ( Class (the InternalRel of A,y)) by A1, EQREL_1: 23;

        hence thesis by A2, A3;

      end;

      hence thesis by A1;

    end;

    theorem :: ROUGHS_1:34

    

     Th34: ( LAp ( LAp X)) = ( UAp ( LAp X))

    proof

      thus ( LAp ( LAp X)) c= ( UAp ( LAp X)) by Th14;

      let x be object;

      assume

       A1: x in ( UAp ( LAp X));

      then ( Class (the InternalRel of A,x)) meets ( LAp X) by Th10;

      then

      consider z be object such that

       A2: z in ( Class (the InternalRel of A,x)) and

       A3: z in ( LAp X) by XBOOLE_0: 3;

      ( Class (the InternalRel of A,z)) c= X by A3, Th8;

      then

       A4: ( Class (the InternalRel of A,x)) c= X by A1, A2, EQREL_1: 23;

      ( Class (the InternalRel of A,x)) c= ( LAp X)

      proof

        let y be object;

        assume

         A5: y in ( Class (the InternalRel of A,x));

        then ( Class (the InternalRel of A,x)) = ( Class (the InternalRel of A,y)) by A1, EQREL_1: 23;

        hence thesis by A4, A5;

      end;

      hence thesis by A1;

    end;

    theorem :: ROUGHS_1:35

    ( UAp ( UAp X)) = ( UAp X)

    proof

      hereby

        let x be object;

        assume

         A1: x in ( UAp ( UAp X));

        then ( Class (the InternalRel of A,x)) meets ( UAp X) by Th10;

        then

        consider y be object such that

         A2: y in ( Class (the InternalRel of A,x)) and

         A3: y in ( UAp X) by XBOOLE_0: 3;

        

         A4: ( Class (the InternalRel of A,y)) = ( Class (the InternalRel of A,x)) by A1, A2, EQREL_1: 23;

        ( Class (the InternalRel of A,y)) meets X by A3, Th10;

        hence x in ( UAp X) by A1, A4;

      end;

      thus thesis by Th13;

    end;

    theorem :: ROUGHS_1:36

    

     Th36: ( UAp ( UAp X)) = ( LAp ( UAp X))

    proof

      thus ( UAp ( UAp X)) c= ( LAp ( UAp X))

      proof

        let x be object;

        assume

         A1: x in ( UAp ( UAp X));

        then ( Class (the InternalRel of A,x)) meets ( UAp X) by Th10;

        then

        consider z be object such that

         A2: z in ( Class (the InternalRel of A,x)) and

         A3: z in ( UAp X) by XBOOLE_0: 3;

        

         A4: ( Class (the InternalRel of A,z)) = ( Class (the InternalRel of A,x)) by A1, A2, EQREL_1: 23;

        

         A5: ( Class (the InternalRel of A,z)) meets X by A3, Th10;

        ( Class (the InternalRel of A,x)) c= ( UAp X)

        proof

          let y be object;

          assume

           A6: y in ( Class (the InternalRel of A,x));

          then ( Class (the InternalRel of A,x)) = ( Class (the InternalRel of A,y)) by A1, EQREL_1: 23;

          hence thesis by A5, A4, A6;

        end;

        hence thesis by A1;

      end;

      thus thesis by Th14;

    end;

    registration

      let A be Tolerance_Space;

      cluster exact for Subset of A;

      existence

      proof

        take ( {} A);

        ( LAp ( {} A)) = {} by Th18;

        hence thesis by Th15;

      end;

    end

    registration

      let A be Approximation_Space;

      let X be Subset of A;

      cluster ( LAp X) -> exact;

      coherence

      proof

        set Y = ( LAp X);

        ( UAp Y) = ( LAp Y) by Th34;

        then ( BndAp Y) = {} by XBOOLE_1: 37;

        hence thesis;

      end;

      cluster ( UAp X) -> exact;

      coherence

      proof

        set Y = ( UAp X);

        ( UAp Y) = ( LAp Y) by Th36;

        then ( BndAp Y) = {} by XBOOLE_1: 37;

        hence thesis;

      end;

    end

    theorem :: ROUGHS_1:37

    

     Th37: for A be Approximation_Space, X be Subset of A, x,y be set st x in ( UAp X) & [x, y] in the InternalRel of A holds y in ( UAp X)

    proof

      let A be Approximation_Space, X be Subset of A;

      let x,y be set;

      assume that

       A1: x in ( UAp X) and

       A2: [x, y] in the InternalRel of A;

       [y, x] in the InternalRel of A by A2, EQREL_1: 6;

      then y in ( Class (the InternalRel of A,x)) by EQREL_1: 19;

      then

       A3: ( Class (the InternalRel of A,x)) = ( Class (the InternalRel of A,y)) by A1, EQREL_1: 23;

      ( Class (the InternalRel of A,x)) meets X & y is Element of A by A1, A2, Th10, ZFMISC_1: 87;

      hence thesis by A3;

    end;

    registration

      let A be non diagonal Approximation_Space;

      cluster rough for Subset of A;

      existence

      proof

        consider x,y be Element of A such that

         A1: x <> y and

         A2: [x, y] in the InternalRel of A by Th4;

        set X = {x};

        x in X & X c= ( UAp X) by Th13, TARSKI:def 1;

        then y in ( UAp X) by A2, Th37;

        then ( UAp X) <> X by A1, TARSKI:def 1;

        then not X is exact by Th16;

        hence thesis;

      end;

    end

    definition

      let A be Approximation_Space;

      let X be Subset of A;

      :: ROUGHS_1:def8

      mode RoughSet of X -> set means it = [( LAp X), ( UAp X)];

      existence ;

    end

    begin

    registration

      let A be finite Tolerance_Space, x be Element of A;

      cluster ( card ( Class (the InternalRel of A,x))) -> non empty;

      coherence

      proof

        x in ( Class (the InternalRel of A,x)) by EQREL_1: 20;

        hence thesis;

      end;

    end

    definition

      let A be finite Tolerance_Space;

      let X be Subset of A;

      :: ROUGHS_1:def9

      func MemberFunc (X,A) -> Function of the carrier of A, REAL means

      : Def9: for x be Element of A holds (it . x) = (( card (X /\ ( Class (the InternalRel of A,x)))) / ( card ( Class (the InternalRel of A,x))));

      existence

      proof

        deffunc F( object) = (( card (X /\ ( Class (the InternalRel of A,$1)))) / ( card ( Class (the InternalRel of A,$1))));

        

         A1: for x be object st x in the carrier of A holds F(x) in REAL by XREAL_0:def 1;

        consider f be Function of the carrier of A, REAL such that

         A2: for x be object st x in the carrier of A holds (f . x) = F(x) from FUNCT_2:sch 2( A1);

        take f;

        let x be Element of A;

        thus thesis by A2;

      end;

      uniqueness

      proof

        deffunc F( Element of A) = (( card (X /\ ( Class (the InternalRel of A,$1)))) / ( card ( Class (the InternalRel of A,$1))));

        

         A3: for A1,A2 be Function of the carrier of A, REAL st (for x be Element of A holds (A1 . x) = F(x)) & (for x be Element of A holds (A2 . x) = F(x)) holds A1 = A2 from BINOP_2:sch 1;

        let A1,A2 be Function of the carrier of A, REAL ;

        assume (for x be Element of A holds (A1 . x) = F(x)) & for x be Element of A holds (A2 . x) = F(x);

        hence A1 = A2 by A3;

      end;

    end

    reserve A for finite Tolerance_Space,

X for Subset of A,

x for Element of A;

    theorem :: ROUGHS_1:38

    

     Th38: 0 <= (( MemberFunc (X,A)) . x) & (( MemberFunc (X,A)) . x) <= 1

    proof

      (( card (X /\ ( Class (the InternalRel of A,x)))) / ( card ( Class (the InternalRel of A,x)))) >= 0 ;

      hence 0 <= (( MemberFunc (X,A)) . x) by Def9;

      ( card (X /\ ( Class (the InternalRel of A,x)))) <= ( card ( Class (the InternalRel of A,x))) by NAT_1: 43, XBOOLE_1: 17;

      then (( card (X /\ ( Class (the InternalRel of A,x)))) / ( card ( Class (the InternalRel of A,x)))) <= 1 by XREAL_1: 185;

      hence thesis by Def9;

    end;

    theorem :: ROUGHS_1:39

    (( MemberFunc (X,A)) . x) in [. 0 , 1.]

    proof

       0 <= (( MemberFunc (X,A)) . x) & (( MemberFunc (X,A)) . x) <= 1 by Th38;

      hence thesis by XXREAL_1: 1;

    end;

    reserve A for finite Approximation_Space,

X,Y for Subset of A,

x for Element of A;

    theorem :: ROUGHS_1:40

    

     Th40: (( MemberFunc (X,A)) . x) = 1 iff x in ( LAp X)

    proof

      hereby

        assume

         A1: (( MemberFunc (X,A)) . x) = 1;

        (( MemberFunc (X,A)) . x) = (( card (X /\ ( Class (the InternalRel of A,x)))) / ( card ( Class (the InternalRel of A,x)))) by Def9;

        then ( card (X /\ ( Class (the InternalRel of A,x)))) = ( card ( Class (the InternalRel of A,x))) by A1, XCMPLX_1: 58;

        then (X /\ ( Class (the InternalRel of A,x))) = ( Class (the InternalRel of A,x)) by CARD_2: 102, XBOOLE_1: 17;

        then ( Class (the InternalRel of A,x)) c= X by XBOOLE_1: 18;

        hence x in ( LAp X);

      end;

      assume x in ( LAp X);

      then

       A2: ( card (X /\ ( Class (the InternalRel of A,x)))) = ( card ( Class (the InternalRel of A,x))) by Th8, XBOOLE_1: 28;

      (( MemberFunc (X,A)) . x) = (( card (X /\ ( Class (the InternalRel of A,x)))) / ( card ( Class (the InternalRel of A,x)))) by Def9;

      hence thesis by A2, XCMPLX_1: 60;

    end;

    theorem :: ROUGHS_1:41

    

     Th41: (( MemberFunc (X,A)) . x) = 0 iff x in (( UAp X) ` )

    proof

      hereby

        assume

         A1: (( MemberFunc (X,A)) . x) = 0 ;

        (( MemberFunc (X,A)) . x) = (( card (X /\ ( Class (the InternalRel of A,x)))) / ( card ( Class (the InternalRel of A,x)))) by Def9;

        then (X /\ ( Class (the InternalRel of A,x))) = {} by A1, XCMPLX_1: 50;

        then X misses ( Class (the InternalRel of A,x));

        then not x in ( UAp X) by Th10;

        hence x in (( UAp X) ` ) by XBOOLE_0:def 5;

      end;

      assume x in (( UAp X) ` );

      then not x in ( UAp X) by XBOOLE_0:def 5;

      then X misses ( Class (the InternalRel of A,x));

      then

       A2: ( card (X /\ ( Class (the InternalRel of A,x)))) = 0 ;

      (( MemberFunc (X,A)) . x) = (( card (X /\ ( Class (the InternalRel of A,x)))) / ( card ( Class (the InternalRel of A,x)))) by Def9;

      hence thesis by A2;

    end;

    theorem :: ROUGHS_1:42

    

     Th42: 0 < (( MemberFunc (X,A)) . x) & (( MemberFunc (X,A)) . x) < 1 iff x in ( BndAp X)

    proof

      hereby

        assume that

         A1: 0 < (( MemberFunc (X,A)) . x) and

         A2: (( MemberFunc (X,A)) . x) < 1;

         not x in (( UAp X) ` ) by A1, Th41;

        then

         A3: x in ( UAp X) by XBOOLE_0:def 5;

         not x in ( LAp X) by A2, Th40;

        hence x in ( BndAp X) by A3, XBOOLE_0:def 5;

      end;

      assume

       A4: x in ( BndAp X);

      then not x in ( LAp X) by XBOOLE_0:def 5;

      then

       A5: (( MemberFunc (X,A)) . x) <> 1 by Th40;

      x in ( UAp X) by A4, XBOOLE_0:def 5;

      then not x in (( UAp X) ` ) by XBOOLE_0:def 5;

      then

       A6: 0 <> (( MemberFunc (X,A)) . x) by Th41;

      (( MemberFunc (X,A)) . x) <= 1 by Th38;

      hence thesis by A6, A5, Th38, XXREAL_0: 1;

    end;

    theorem :: ROUGHS_1:43

    

     Th43: for A be discrete Approximation_Space, X be Subset of A holds X is exact

    proof

      let A be discrete Approximation_Space, X be Subset of A;

      

       A1: the InternalRel of A = ( id the carrier of A) by ORDERS_3:def 1;

      X = ( UAp X)

      proof

        thus X c= ( UAp X) by Th13;

        let x be object;

        assume

         A2: x in ( UAp X);

        then ( Class (the InternalRel of A,x)) meets X by Th10;

        then

         A3: ex y be object st y in ( Class (the InternalRel of A,x)) & y in X by XBOOLE_0: 3;

        ( Class (the InternalRel of A,x)) = {x} by A1, A2, EQREL_1: 25;

        hence thesis by A3, TARSKI:def 1;

      end;

      hence thesis;

    end;

    registration

      let A be discrete Approximation_Space;

      cluster -> exact for Subset of A;

      coherence by Th43;

    end

    theorem :: ROUGHS_1:44

    for A be discrete finite Approximation_Space, X be Subset of A holds ( MemberFunc (X,A)) = ( chi (X,the carrier of A))

    proof

      let A be discrete finite Approximation_Space, X be Subset of A;

      reconsider F = ( MemberFunc (X,A)) as Function of the carrier of A, REAL ;

      set G = ( chi (X,the carrier of A));

       {( In ( 0 , REAL )), ( In (1, REAL ))} c= REAL ;

      then

      reconsider G as Function of the carrier of A, REAL by FUNCT_2: 7;

      for x be object st x in the carrier of A holds (F . x) = (G . x)

      proof

        let x be object;

        assume

         A1: x in the carrier of A;

        per cases ;

          suppose

           A2: x in X;

          then x in ( LAp X) by Th15;

          then (F . x) = 1 by Th40;

          hence thesis by A2, FUNCT_3:def 3;

        end;

          suppose

           A3: not x in X;

          then not x in ( UAp X) by Th16;

          then x in (( UAp X) ` ) by A1, XBOOLE_0:def 5;

          then (F . x) = 0 by Th41;

          hence thesis by A1, A3, FUNCT_3:def 3;

        end;

      end;

      hence thesis by FUNCT_2: 12;

    end;

    theorem :: ROUGHS_1:45

    for A be finite Approximation_Space, X be Subset of A, x,y be set st [x, y] in the InternalRel of A holds (( MemberFunc (X,A)) . x) = (( MemberFunc (X,A)) . y)

    proof

      let A be finite Approximation_Space, X be Subset of A, x,y be set;

      assume

       A1: [x, y] in the InternalRel of A;

      then

       A2: y is Element of A by ZFMISC_1: 87;

      x is Element of A by A1, ZFMISC_1: 87;

      then

       A3: (( MemberFunc (X,A)) . x) = (( card (X /\ ( Class (the InternalRel of A,x)))) / ( card ( Class (the InternalRel of A,x)))) by Def9;

      x in ( Class (the InternalRel of A,y)) by A1, EQREL_1: 19;

      then ( Class (the InternalRel of A,x)) = ( Class (the InternalRel of A,y)) by A2, EQREL_1: 23;

      hence thesis by A2, A3, Def9;

    end;

    theorem :: ROUGHS_1:46

    (( MemberFunc ((X ` ),A)) . x) = (1 - (( MemberFunc (X,A)) . x))

    proof

      

       A1: (( [#] A) /\ ( Class (the InternalRel of A,x))) = ( Class (the InternalRel of A,x)) by XBOOLE_1: 28;

      (( MemberFunc ((X ` ),A)) . x) = (( card ((( [#] A) \ X) /\ ( Class (the InternalRel of A,x)))) / ( card ( Class (the InternalRel of A,x)))) by Def9

      .= (( card ((( [#] A) /\ ( Class (the InternalRel of A,x))) \ (X /\ ( Class (the InternalRel of A,x))))) / ( card ( Class (the InternalRel of A,x)))) by XBOOLE_1: 50

      .= ((( card (( [#] A) /\ ( Class (the InternalRel of A,x)))) - ( card (X /\ ( Class (the InternalRel of A,x))))) / ( card ( Class (the InternalRel of A,x)))) by A1, CARD_2: 44, XBOOLE_1: 17

      .= ((( card (( [#] A) /\ ( Class (the InternalRel of A,x)))) / ( card ( Class (the InternalRel of A,x)))) - (( card (X /\ ( Class (the InternalRel of A,x)))) / ( card ( Class (the InternalRel of A,x))))) by XCMPLX_1: 120

      .= ((( card ( Class (the InternalRel of A,x))) / ( card ( Class (the InternalRel of A,x)))) - (( card (X /\ ( Class (the InternalRel of A,x)))) / ( card ( Class (the InternalRel of A,x))))) by XBOOLE_1: 28

      .= (1 - (( card (X /\ ( Class (the InternalRel of A,x)))) / ( card ( Class (the InternalRel of A,x))))) by XCMPLX_1: 60

      .= (1 - (( MemberFunc (X,A)) . x)) by Def9;

      hence thesis;

    end;

    theorem :: ROUGHS_1:47

    

     Th47: X c= Y implies (( MemberFunc (X,A)) . x) <= (( MemberFunc (Y,A)) . x)

    proof

      set CI = ( Class (the InternalRel of A,x));

      assume X c= Y;

      then ( card (Y /\ CI)) >= ( card (X /\ CI)) by NAT_1: 43, XBOOLE_1: 26;

      then

       A1: (( card (Y /\ CI)) / ( card CI)) >= (( card (X /\ CI)) / ( card CI)) by XREAL_1: 72;

      (( MemberFunc (X,A)) . x) = (( card (X /\ CI)) / ( card CI)) by Def9;

      hence thesis by A1, Def9;

    end;

    theorem :: ROUGHS_1:48

    (( MemberFunc ((X \/ Y),A)) . x) >= (( MemberFunc (X,A)) . x) by Th47, XBOOLE_1: 7;

    theorem :: ROUGHS_1:49

    (( MemberFunc ((X /\ Y),A)) . x) <= (( MemberFunc (X,A)) . x) by Th47, XBOOLE_1: 17;

    theorem :: ROUGHS_1:50

    (( MemberFunc ((X \/ Y),A)) . x) >= ( max ((( MemberFunc (X,A)) . x),(( MemberFunc (Y,A)) . x)))

    proof

      (( MemberFunc ((X \/ Y),A)) . x) >= (( MemberFunc (X,A)) . x) & (( MemberFunc ((X \/ Y),A)) . x) >= (( MemberFunc (Y,A)) . x) by Th47, XBOOLE_1: 7;

      hence thesis by XXREAL_0: 28;

    end;

    theorem :: ROUGHS_1:51

    

     Th51: X misses Y implies (( MemberFunc ((X \/ Y),A)) . x) = ((( MemberFunc (X,A)) . x) + (( MemberFunc (Y,A)) . x))

    proof

      assume

       A1: X misses Y;

      ( card ((X \/ Y) /\ ( Class (the InternalRel of A,x)))) = ( card ((X /\ ( Class (the InternalRel of A,x))) \/ (Y /\ ( Class (the InternalRel of A,x))))) by XBOOLE_1: 23

      .= (( card (X /\ ( Class (the InternalRel of A,x)))) + ( card (Y /\ ( Class (the InternalRel of A,x))))) by A1, CARD_2: 40, XBOOLE_1: 76;

      

      then (( MemberFunc ((X \/ Y),A)) . x) = ((( card (X /\ ( Class (the InternalRel of A,x)))) + ( card (Y /\ ( Class (the InternalRel of A,x))))) / ( card ( Class (the InternalRel of A,x)))) by Def9

      .= ((( card (X /\ ( Class (the InternalRel of A,x)))) / ( card ( Class (the InternalRel of A,x)))) + (( card (Y /\ ( Class (the InternalRel of A,x)))) / ( card ( Class (the InternalRel of A,x))))) by XCMPLX_1: 62

      .= ((( MemberFunc (X,A)) . x) + (( card (Y /\ ( Class (the InternalRel of A,x)))) / ( card ( Class (the InternalRel of A,x))))) by Def9

      .= ((( MemberFunc (X,A)) . x) + (( MemberFunc (Y,A)) . x)) by Def9;

      hence thesis;

    end;

    theorem :: ROUGHS_1:52

    (( MemberFunc ((X /\ Y),A)) . x) <= ( min ((( MemberFunc (X,A)) . x),(( MemberFunc (Y,A)) . x)))

    proof

      (( MemberFunc ((X /\ Y),A)) . x) <= (( MemberFunc (X,A)) . x) & (( MemberFunc ((X /\ Y),A)) . x) <= (( MemberFunc (Y,A)) . x) by Th47, XBOOLE_1: 17;

      hence thesis by XXREAL_0: 20;

    end;

    definition

      let A be finite Tolerance_Space;

      let X be FinSequence of ( bool the carrier of A);

      let x be Element of A;

      :: ROUGHS_1:def10

      func FinSeqM (x,X) -> FinSequence of REAL means

      : Def10: ( dom it ) = ( dom X) & for n be Nat st n in ( dom X) holds (it . n) = (( MemberFunc ((X . n),A)) . x);

      existence

      proof

        deffunc F( Nat) = (( MemberFunc ((X . $1),A)) . x);

        ex z be FinSequence of REAL st ( len z) = ( len X) & for j be Nat st j in ( dom z) holds (z . j) = F(j) from FINSEQ_2:sch 1;

        then

        consider z be FinSequence of REAL such that

         A1: ( len z) = ( len X) and

         A2: for j be Nat st j in ( dom z) holds (z . j) = F(j);

        take z;

        

        thus ( dom z) = ( Seg ( len z)) by FINSEQ_1:def 3

        .= ( dom X) by A1, FINSEQ_1:def 3;

        let n be Nat;

        assume n in ( dom X);

        then

         A3: n in ( Seg ( len X)) by FINSEQ_1:def 3;

        ( dom z) = ( Seg ( len X)) by A1, FINSEQ_1:def 3;

        hence thesis by A2, A3;

      end;

      uniqueness

      proof

        let A1,A2 be FinSequence of REAL such that

         A4: ( dom A1) = ( dom X) and

         A5: for n be Nat st n in ( dom X) holds (A1 . n) = (( MemberFunc ((X . n),A)) . x) and

         A6: ( dom A2) = ( dom X) and

         A7: for n be Nat st n in ( dom X) holds (A2 . n) = (( MemberFunc ((X . n),A)) . x);

        for n be Nat st n in ( dom A1) holds (A1 . n) = (A2 . n)

        proof

          let n be Nat;

          assume

           A8: n in ( dom A1);

          reconsider n as Element of NAT by ORDINAL1:def 12;

          (A1 . n) = (( MemberFunc ((X . n),A)) . x) by A4, A5, A8

          .= (A2 . n) by A4, A7, A8;

          hence thesis;

        end;

        hence thesis by A4, A6, FINSEQ_1: 13;

      end;

    end

    theorem :: ROUGHS_1:53

    

     Th53: for X be FinSequence of ( bool the carrier of A), x be Element of A, y be Subset of A holds ( FinSeqM (x,(X ^ <*y*>))) = (( FinSeqM (x,X)) ^ <*(( MemberFunc (y,A)) . x)*>)

    proof

      let X be FinSequence of ( bool the carrier of A), x be Element of A, y be Subset of A;

      set p = ( FinSeqM (x,(X ^ <*y*>)));

      set q = (( FinSeqM (x,X)) ^ <*(( MemberFunc (y,A)) . x)*>);

      ( dom X) = ( dom ( FinSeqM (x,X))) by Def10;

      

      then ( Seg ( len X)) = ( dom ( FinSeqM (x,X))) by FINSEQ_1:def 3

      .= ( Seg ( len ( FinSeqM (x,X)))) by FINSEQ_1:def 3;

      then

       A1: ( len X) = ( len ( FinSeqM (x,X))) by FINSEQ_1: 6;

      

       A2: ( dom p) = ( dom (X ^ <*y*>)) by Def10

      .= ( Seg (( len X) + ( len <*y*>))) by FINSEQ_1:def 7

      .= ( Seg (( len X) + 1)) by FINSEQ_1: 39;

      

       A3: for k be Nat st k in ( dom p) holds (p . k) = (q . k)

      proof

        let k be Nat;

        assume

         A4: k in ( dom p);

        then

        reconsider k as Element of NAT ;

        

         A5: 1 <= k by A4, FINSEQ_3: 25;

        k in ( dom (X ^ <*y*>)) by A4, Def10;

        then

         A6: (p . k) = (( MemberFunc (((X ^ <*y*>) . k),A)) . x) by Def10;

        

         A7: k <= (( len X) + 1) by A2, A4, FINSEQ_1: 1;

        per cases by A7, NAT_1: 8;

          suppose

           A8: k <= ( len X);

          then

           A9: k in ( dom X) by A5, FINSEQ_3: 25;

          k in ( dom ( FinSeqM (x,X))) by A1, A5, A8, FINSEQ_3: 25;

          

          then (q . k) = (( FinSeqM (x,X)) . k) by FINSEQ_1:def 7

          .= (( MemberFunc ((X . k),A)) . x) by A9, Def10;

          hence thesis by A6, A9, FINSEQ_1:def 7;

        end;

          suppose

           A10: k = (( len X) + 1);

          then (q . k) = (( MemberFunc (y,A)) . x) by A1, FINSEQ_1: 42;

          hence thesis by A6, A10, FINSEQ_1: 42;

        end;

      end;

      ( dom q) = ( Seg (( len ( FinSeqM (x,X))) + ( len <*(( MemberFunc (y,A)) . x)*>))) by FINSEQ_1:def 7

      .= ( Seg (( len X) + 1)) by A1, FINSEQ_1: 39;

      hence thesis by A2, A3, FINSEQ_1: 13;

    end;

    theorem :: ROUGHS_1:54

    

     Th54: (( MemberFunc (( {} A),A)) . x) = 0

    proof

      ( UAp ( {} A)) = {} by Th19;

      then (( UAp ( {} A)) ` ) = ( [#] A);

      hence thesis by Th41;

    end;

    theorem :: ROUGHS_1:55

    for X be disjoint_valued FinSequence of ( bool the carrier of A) holds (( MemberFunc (( Union X),A)) . x) = ( Sum ( FinSeqM (x,X)))

    proof

      let X be disjoint_valued FinSequence of ( bool the carrier of A);

      defpred P[ FinSequence of ( bool the carrier of A)] means $1 is disjoint_valued implies (( MemberFunc (( Union $1),A)) . x) = ( Sum ( FinSeqM (x,$1)));

      

       A1: for p be FinSequence of ( bool the carrier of A) holds for y be Subset of A st P[p] holds P[(p ^ <*y*>)]

      proof

        let p be FinSequence of ( bool the carrier of A);

        let y be Subset of A;

        assume

         A2: P[p];

         P[(p ^ <*y*>)]

        proof

          assume

           A3: (p ^ <*y*>) is disjoint_valued;

          

           A4: ( Union p) misses y

          proof

            assume ( Union p) meets y;

            then

            consider x be object such that

             A5: x in ( Union p) and

             A6: x in y by XBOOLE_0: 3;

            consider X be set such that

             A7: x in X and

             A8: X in ( rng p) by A5, TARSKI:def 4;

            consider m be object such that

             A9: m in ( dom p) and

             A10: X = (p . m) by A8, FUNCT_1:def 3;

            reconsider m as Element of NAT by A9;

            

             A11: ((p ^ <*y*>) . m) = (p . m) & m <= ( len p) by A9, FINSEQ_1:def 7, FINSEQ_3: 25;

            

             A12: ((p ^ <*y*>) . (( len p) + 1)) = y & ( len p) < (( len p) + 1) by FINSEQ_1: 42, NAT_1: 13;

            (p . m) meets y by A6, A7, A10, XBOOLE_0: 3;

            hence thesis by A3, A12, A11;

          end;

          ( Union (p ^ <*y*>)) = (( Union p) \/ ( Union <*y*>)) by Th5

          .= (( Union p) \/ y) by FINSEQ_3: 135;

          

          then (( MemberFunc (( Union (p ^ <*y*>)),A)) . x) = ((( MemberFunc (( Union p),A)) . x) + (( MemberFunc (y,A)) . x)) by A4, Th51

          .= ( Sum (( FinSeqM (x,p)) ^ <*(( MemberFunc (y,A)) . x)*>)) by A2, A3, Th6, FINSEQ_6: 10, RVSUM_1: 74

          .= ( Sum ( FinSeqM (x,(p ^ <*y*>)))) by Th53;

          hence thesis;

        end;

        hence thesis;

      end;

      

       A13: P[( <*> ( bool the carrier of A))]

      proof

        set F = ( FinSeqM (x,( <*> ( bool the carrier of A))));

        assume ( <*> ( bool the carrier of A)) is disjoint_valued;

        ( dom F) = ( dom ( <*> ( bool the carrier of A))) by Def10;

        then

         A14: ( Sum F) = 0 by RELAT_1: 41, RVSUM_1: 72;

        ( Union ( <*> ( bool the carrier of A))) = ( {} A) by ZFMISC_1: 2;

        hence thesis by A14, Th54;

      end;

      for p be FinSequence of ( bool the carrier of A) holds P[p] from FINSEQ_2:sch 2( A13, A1);

      hence thesis;

    end;

    theorem :: ROUGHS_1:56

    ( LAp X) = { x where x be Element of A : (( MemberFunc (X,A)) . x) = 1 }

    proof

      thus ( LAp X) c= { x where x be Element of A : (( MemberFunc (X,A)) . x) = 1 }

      proof

        let y be object;

        assume

         A1: y in ( LAp X);

        then

        reconsider y9 = y as Element of A;

        (( MemberFunc (X,A)) . y9) = 1 by A1, Th40;

        hence thesis;

      end;

      let y be object;

      assume y in { x where x be Element of A : (( MemberFunc (X,A)) . x) = 1 };

      then ex y9 be Element of A st y9 = y & (( MemberFunc (X,A)) . y9) = 1;

      hence thesis by Th40;

    end;

    theorem :: ROUGHS_1:57

    ( UAp X) = { x where x be Element of A : (( MemberFunc (X,A)) . x) > 0 }

    proof

      thus ( UAp X) c= { x where x be Element of A : (( MemberFunc (X,A)) . x) > 0 }

      proof

        let y be object;

        assume

         A1: y in ( UAp X);

        then

        reconsider y9 = y as Element of A;

         not y in (( UAp X) ` ) by A1, XBOOLE_0:def 5;

        then (( MemberFunc (X,A)) . y9) <> 0 by Th41;

        then (( MemberFunc (X,A)) . y9) > 0 by Th38;

        hence thesis;

      end;

      let y be object;

      assume y in { x where x be Element of A : (( MemberFunc (X,A)) . x) > 0 };

      then

       A2: ex y9 be Element of A st y9 = y & (( MemberFunc (X,A)) . y9) > 0 ;

      then not y in (( UAp X) ` ) by Th41;

      hence thesis by A2, XBOOLE_0:def 5;

    end;

    theorem :: ROUGHS_1:58

    ( BndAp X) = { x where x be Element of A : 0 < (( MemberFunc (X,A)) . x) & (( MemberFunc (X,A)) . x) < 1 }

    proof

      thus ( BndAp X) c= { x where x be Element of A : 0 < (( MemberFunc (X,A)) . x) & (( MemberFunc (X,A)) . x) < 1 }

      proof

        let y be object;

        assume

         A1: y in ( BndAp X);

        then

        reconsider y9 = y as Element of A;

         0 < (( MemberFunc (X,A)) . y9) & (( MemberFunc (X,A)) . y9) < 1 by A1, Th42;

        hence thesis;

      end;

      let y be object;

      assume y in { x where x be Element of A : 0 < (( MemberFunc (X,A)) . x) & (( MemberFunc (X,A)) . x) < 1 };

      then ex y9 be Element of A st y9 = y & 0 < (( MemberFunc (X,A)) . y9) & (( MemberFunc (X,A)) . y9) < 1;

      hence thesis by Th42;

    end;

    begin

    reserve A for Tolerance_Space,

X,Y,Z for Subset of A;

    definition

      let A be Tolerance_Space, X,Y be Subset of A;

      :: ROUGHS_1:def11

      pred X _c= Y means ( LAp X) c= ( LAp Y);

      reflexivity ;

      :: ROUGHS_1:def12

      pred X c=^ Y means ( UAp X) c= ( UAp Y);

      reflexivity ;

    end

    definition

      let A be Tolerance_Space, X,Y be Subset of A;

      :: ROUGHS_1:def13

      pred X _c=^ Y means X _c= Y & X c=^ Y;

      reflexivity ;

    end

    theorem :: ROUGHS_1:59

    

     Th59: X _c= Y & Y _c= Z implies X _c= Z

    proof

      assume X _c= Y & Y _c= Z;

      then ( LAp X) c= ( LAp Y) & ( LAp Y) c= ( LAp Z);

      then ( LAp X) c= ( LAp Z);

      hence thesis;

    end;

    theorem :: ROUGHS_1:60

    

     Th60: X c=^ Y & Y c=^ Z implies X c=^ Z

    proof

      assume X c=^ Y & Y c=^ Z;

      then ( UAp X) c= ( UAp Y) & ( UAp Y) c= ( UAp Z);

      then ( UAp X) c= ( UAp Z);

      hence thesis;

    end;

    theorem :: ROUGHS_1:61

    X _c=^ Y & Y _c=^ Z implies X _c=^ Z by Th60, Th59;

    begin

    definition

      let A be Tolerance_Space, X,Y be Subset of A;

      :: ROUGHS_1:def14

      pred X _= Y means ( LAp X) = ( LAp Y);

      reflexivity ;

      symmetry ;

      :: ROUGHS_1:def15

      pred X =^ Y means ( UAp X) = ( UAp Y);

      reflexivity ;

      symmetry ;

      :: ROUGHS_1:def16

      pred X _=^ Y means ( LAp X) = ( LAp Y) & ( UAp X) = ( UAp Y);

      reflexivity ;

      symmetry ;

    end

    definition

      let A be Tolerance_Space, X,Y be Subset of A;

      :: original: _=

      redefine

      :: ROUGHS_1:def17

      pred X _= Y means X _c= Y & Y _c= X;

      compatibility

      proof

        thus X _= Y implies X _c= Y & Y _c= X;

        assume X _c= Y & Y _c= X;

        then ( LAp X) c= ( LAp Y) & ( LAp Y) c= ( LAp X);

        then ( LAp X) = ( LAp Y);

        hence thesis;

      end;

      :: original: =^

      redefine

      :: ROUGHS_1:def18

      pred X =^ Y means X c=^ Y & Y c=^ X;

      compatibility

      proof

        thus X =^ Y implies X c=^ Y & Y c=^ X;

        assume X c=^ Y & Y c=^ X;

        then ( UAp X) c= ( UAp Y) & ( UAp Y) c= ( UAp X);

        then ( UAp X) = ( UAp Y);

        hence thesis;

      end;

      :: original: _=^

      redefine

      :: ROUGHS_1:def19

      pred X _=^ Y means X _= Y & X =^ Y;

      compatibility ;

    end