roughs_5.miz

    begin

    definition

      let R be non empty set;

      let I be Function of R, ( bool R);

      :: ROUGHS_5:def1

      attr I is map-reflexive means for u be Element of R holds u in (I . u);

    end

    definition

      let R be non empty set;

      :: ROUGHS_5:def2

      func singleton R -> Function of R, ( bool R) means

      : SingleFunc: for x be Element of R holds (it . x) = {x};

      existence

      proof

        deffunc U( object) = {$1};

         A1:

        now

          let x be Element of R;

           {x} c= R;

          hence U(x) in ( bool R);

        end;

        thus ex f be Function of R, ( bool R) st for x be Element of R holds (f . x) = U(x) from FUNCT_2:sch 8( A1);

      end;

      uniqueness

      proof

        let IT,IT9 be Function of R, ( bool R) such that

         A3: for x be Element of R holds (IT . x) = {x} and

         A4: for x be Element of R holds (IT9 . x) = {x};

        now

          let x be Element of R;

          (IT . x) = {x} by A3;

          hence (IT . x) = (IT9 . x) by A4;

        end;

        hence thesis;

      end;

      correctness ;

    end

    registration

      let R be non empty set;

      cluster ( singleton R) -> map-reflexive;

      coherence

      proof

        for r be Element of R holds r in (( singleton R) . r)

        proof

          let r be Element of R;

          r in {r} by TARSKI:def 1;

          hence thesis by SingleFunc;

        end;

        hence thesis;

      end;

    end

    theorem :: ROUGHS_5:1

    for R be non empty RelStr, I be Function of the carrier of R, ( bool the carrier of R) st I is map-reflexive holds the carrier of R = ( union (I .: ( [#] R)))

    proof

      let R be non empty RelStr, I be Function of the carrier of R, ( bool the carrier of R);

      assume

       AA: I is map-reflexive;

      thus the carrier of R c= ( union (I .: ( [#] R)))

      proof

        let x be object;

        assume

         A0: x in the carrier of R;

        then

        reconsider y = x as Element of R;



         A2: y in (I . x) by AA;

        x in ( dom I) by A0, FUNCT_2:def 1;

        then (I . x) in (I .: ( [#] R)) by FUNCT_1:def 6;

        hence thesis by A2, TARSKI:def 4;

      end;

      let x be object;

      assume x in ( union (I .: ( [#] R)));

      then

      consider y be set such that

       T1: x in y & y in (I .: ( [#] R)) by TARSKI:def 4;

      thus thesis by T1;

    end;

    reserve f,g for Function;

    reserve R for non empty reflexive RelStr;

    theorem :: ROUGHS_5:2



     LApId: ( LAp R) cc= ( id ( bool the carrier of R))

    proof

      set f = ( LAp R);

      set g = ( id ( bool the carrier of R));



       A1: ( dom f) c= ( dom g);

      for i be set st i in ( dom f) holds (f . i) c= (g . i)

      proof

        let i be set;

        assume i in ( dom f);

        then

        reconsider ii = i as Subset of R;

        (f . ii) = ( LAp ii) by ROUGHS_2:def 10;

        hence thesis by ROUGHS_2: 35;

      end;

      hence thesis by A1, ALTCAT_2:def 1;

    end;

    theorem :: ROUGHS_5:3

    ( id ( bool the carrier of R)) cc= ( UAp R)

    proof

      set f = ( id ( bool the carrier of R));

      set g = ( UAp R);



       A1: ( dom f) c= ( dom g) by FUNCT_2:def 1;

      for i be set st i in ( dom f) holds (f . i) c= (g . i)

      proof

        let i be set;

        assume i in ( dom f);

        then

        reconsider ii = i as Subset of R;

        (g . ii) = ( UAp ii) by ROUGHS_2:def 11;

        hence (f . i) c= (g . i) by ROUGHS_2: 36;

      end;

      hence thesis by A1, ALTCAT_2:def 1;

    end;

    reserve R for non empty RelStr;

    theorem :: ROUGHS_5:4

    for f be map of R, x,y be Subset of R holds ( Flip ( Flip f)) = f by ROUGHS_2: 23;

    theorem :: ROUGHS_5:5



     FlipCompose: for f,g be map of R holds ( Flip (f * g)) = (( Flip f) * ( Flip g))

    proof

      let f,g be map of R;

      set fg = ( Flip (f * g));

      set ff = ( Flip f);

      set gg = ( Flip g);

      for x be Subset of R holds (fg . x) = ((ff * gg) . x)

      proof

        let x be Subset of R;

        (x ` ) in ( bool the carrier of R);

        then

         A1: (x ` ) in ( dom g) by FUNCT_2:def 1;



         a2: ( dom ( Flip g)) = ( bool the carrier of R) by FUNCT_2:def 1;

        (fg . x) = (((f * g) . (x ` )) ` ) by ROUGHS_2:def 14

        .= ((f . (((g . (x ` )) ` ) ` )) ` ) by FUNCT_1: 13, A1

        .= (ff . ((g . (x ` )) ` )) by ROUGHS_2:def 14

        .= (ff . (gg . x)) by ROUGHS_2:def 14

        .= ((ff * gg) . x) by a2, FUNCT_1: 13;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: ROUGHS_5:6

    for f be map of R holds (f . {} ) = {} iff (( Flip f) . the carrier of R) = the carrier of R

    proof

      let f be map of R;

      thus (f . {} ) = {} implies (( Flip f) . the carrier of R) = the carrier of R by ROUGHS_2: 18;

      set g = ( Flip f);



       A1: ( Flip ( Flip f)) = f by ROUGHS_2: 23;

      thus (( Flip f) . the carrier of R) = the carrier of R implies (f . {} ) = {} by A1, ROUGHS_2: 19;

    end;

    begin

    definition

      let R be non empty RelStr;

      :: ROUGHS_5:def3

      func UncertaintyMap R -> Function of the carrier of R, ( bool the carrier of R) means

      : DefUnc: for x be Element of R holds (it . x) = ( Coim (the InternalRel of R,x));

      existence

      proof

        deffunc F( Element of R) = ( In (( Coim (the InternalRel of R,$1)),( bool the carrier of R)));

        consider f be Function of the carrier of R, ( bool the carrier of R) such that

         A1: for x be Element of R holds (f . x) = F(x) from FUNCT_2:sch 4;

        take f;

        let x be Element of R;



         A2: (f . x) = ( In (( Coim (the InternalRel of R,x)),( bool the carrier of R))) by A1;

        (the InternalRel of R " {x}) c= the carrier of R;

        hence thesis by A2;

      end;

      uniqueness

      proof

        let f1,f2 be Function of the carrier of R, ( bool the carrier of R) such that

         A1: for x be Element of R holds (f1 . x) = ( Coim (the InternalRel of R,x)) and

         A2: for x be Element of R holds (f2 . x) = ( Coim (the InternalRel of R,x));

        for x be Element of R holds (f1 . x) = (f2 . x)

        proof

          let x be Element of R;

          (f1 . x) = ( Coim (the InternalRel of R,x)) by A1

          .= (f2 . x) by A2;

          hence thesis;

        end;

        hence thesis;

      end;

      correctness ;

    end

    theorem :: ROUGHS_5:7



     For3: for w,u be Element of R holds [w, u] in the InternalRel of R iff w in (( UncertaintyMap R) . u)

    proof

      let w,u be Element of R;

      thus [w, u] in the InternalRel of R implies w in (( UncertaintyMap R) . u)

      proof

        assume

         S1: [w, u] in the InternalRel of R;

        u in {u} by TARSKI:def 1;

        then w in ( Coim (the InternalRel of R,u)) by S1, RELAT_1:def 14;

        hence thesis by DefUnc;

      end;

      assume w in (( UncertaintyMap R) . u);

      then w in ( Coim (the InternalRel of R,u)) by DefUnc;

      then

      consider x be object such that

       S1: [w, x] in the InternalRel of R & x in {u} by RELAT_1:def 14;

      thus thesis by S1, TARSKI:def 1;

    end;

    definition

      let R be non empty RelStr;

      :: ROUGHS_5:def4

      func tau R -> Function of the carrier of R, ( bool the carrier of R) means

      : DefTau: for u be Element of R holds (it . u) = ( Im (the InternalRel of R,u));

      existence

      proof

        deffunc F( Element of R) = ( In (( Im (the InternalRel of R,$1)),( bool the carrier of R)));

        consider f be Function of the carrier of R, ( bool the carrier of R) such that

         A1: for x be Element of R holds (f . x) = F(x) from FUNCT_2:sch 4;

        take f;

        let x be Element of R;



         A2: (f . x) = ( In (( Im (the InternalRel of R,x)),( bool the carrier of R))) by A1;

        (the InternalRel of R .: {x}) c= the carrier of R;

        hence thesis by A2;

      end;

      uniqueness

      proof

        let f1,f2 be Function of the carrier of R, ( bool the carrier of R) such that

         A1: for x be Element of R holds (f1 . x) = ( Im (the InternalRel of R,x)) and

         A2: for x be Element of R holds (f2 . x) = ( Im (the InternalRel of R,x));

        for x be Element of R holds (f1 . x) = (f2 . x)

        proof

          let x be Element of R;

          (f1 . x) = ( Im (the InternalRel of R,x)) by A1

          .= (f2 . x) by A2;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: ROUGHS_5:8



     ImCoim: for u,w be Element of R holds u in ( Im (the InternalRel of R,w)) iff w in ( Coim (the InternalRel of R,u))

    proof

      let u,w be Element of R;

      thus u in ( Im (the InternalRel of R,w)) implies w in ( Coim (the InternalRel of R,u))

      proof

        assume u in ( Im (the InternalRel of R,w));

        then

         Z1: [w, u] in the InternalRel of R by RELAT_1: 169;

        u in {u} by TARSKI:def 1;

        hence thesis by Z1, RELAT_1:def 14;

      end;

      assume w in ( Coim (the InternalRel of R,u));

      then

      consider t be object such that

       W1: [w, t] in the InternalRel of R & t in {u} by RELAT_1:def 14;

      t = u by W1, TARSKI:def 1;

      hence thesis by RELAT_1: 169, W1;

    end;

    theorem :: ROUGHS_5:9



     For3A: for w,u be Element of R holds [w, u] in the InternalRel of R iff u in (( tau R) . w)

    proof

      let w,u be Element of R;

      thus [w, u] in the InternalRel of R implies u in (( tau R) . w)

      proof

        assume [w, u] in the InternalRel of R;

        then u in ( Im (the InternalRel of R,w)) by RELAT_1: 169;

        hence thesis by DefTau;

      end;

      assume u in (( tau R) . w);

      then u in ( Im (the InternalRel of R,w)) by DefTau;

      then w in ( Coim (the InternalRel of R,u)) by ImCoim;

      then

      consider x be object such that

       S1: [w, x] in the InternalRel of R & x in {u} by RELAT_1:def 14;

      thus thesis by S1, TARSKI:def 1;

    end;

    definition

      let R be non empty RelStr;

      let f be Function of the carrier of R, ( bool the carrier of R);

      :: ROUGHS_5:def5

      func ff_0 f -> map of R means

      : Defff: for x be Subset of R holds (it . x) = { u where u be Element of R : (f . u) meets x };

      existence

      proof

        deffunc F( Subset of R) = ( In ({ u where u be Element of R : (f . u) meets $1 },( bool the carrier of R)));

        consider g be map of R such that

         A1: for x be Element of ( bool the carrier of R) holds (g . x) = F(x) from FUNCT_2:sch 4;

        take g;

        let x be Subset of R;



         A2: (g . x) = ( In ({ u where u be Element of R : (f . u) meets x },( bool the carrier of R))) by A1;

        { u where u be Element of R : (f . u) meets x } c= the carrier of R

        proof

          let y be object;

          assume y in { u where u be Element of R : (f . u) meets x };

          then

          consider u be Element of R such that

           A3: y = u & (f . u) meets x;

          thus thesis by A3;

        end;

        hence thesis by A2, SUBSET_1:def 8;

      end;

      uniqueness

      proof

        let f1,f2 be map of R;

        assume that

         A1: for x be Subset of R holds (f1 . x) = { u where u be Element of R : (f . u) meets x } and

         A2: for x be Subset of R holds (f2 . x) = { u where u be Element of R : (f . u) meets x };

        for y be Element of ( bool the carrier of R) holds (f1 . y) = (f2 . y)

        proof

          let y be Element of ( bool the carrier of R);

          (f1 . y) = { u where u be Element of R : (f . u) meets y } by A1

          .= (f2 . y) by A2;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    definition

      let R be non empty RelStr;

      :: ROUGHS_5:def6

      func f_0 R -> map of R equals ( ff_0 ( tau R));

      coherence ;

      :: ROUGHS_5:def7

      func f_1 R -> map of R equals ( ff_0 ( UncertaintyMap R));

      coherence ;

    end

    theorem :: ROUGHS_5:10



     UncEqTau: the InternalRel of R is symmetric implies ( UncertaintyMap R) = ( tau R)

    proof

      assume

       AA: the InternalRel of R is symmetric;

      set f = ( UncertaintyMap R), g = ( tau R);

      for x be Element of R holds (f . x) = (g . x)

      proof

        let x be Element of R;



         Z2: (f . x) = ( Coim (the InternalRel of R,x)) by DefUnc;



         ZZ: ( Im (the InternalRel of R,x)) c= ( Coim (the InternalRel of R,x))

        proof

          let y be object;

          assume y in ( Im (the InternalRel of R,x));

          then [x, y] in the InternalRel of R by RELAT_1: 169;

          then

           B2: [y, x] in the InternalRel of R by AA, PREFER_1: 20;

          x in {x} by TARSKI:def 1;

          hence thesis by B2, RELAT_1:def 14;

        end;

        ( Coim (the InternalRel of R,x)) c= ( Im (the InternalRel of R,x))

        proof

          let y be object;

          assume y in ( Coim (the InternalRel of R,x));

          then

          consider yy be object such that

           B2: [y, yy] in the InternalRel of R & yy in {x} by RELAT_1:def 14;

          yy = x by TARSKI:def 1, B2;

          then [x, y] in the InternalRel of R by B2, PREFER_1: 20, AA;

          hence thesis by RELAT_1: 169;

        end;

        hence thesis by ZZ, DefTau, Z2;

      end;

      hence thesis;

    end;

    theorem :: ROUGHS_5:11

    the InternalRel of R is symmetric implies ( f_0 R) = ( f_1 R) by UncEqTau;



     Lemacik: for a,b be object, RR be Relation of the carrier of R st [a, b] in RR holds a is Element of R & b is Element of R by ZFMISC_1: 87;

    theorem :: ROUGHS_5:12

    the InternalRel of R is symmetric iff for u,v be Element of R holds u in (( tau R) . v) implies v in (( tau R) . u)

    proof

      hereby

        assume

         A1: the InternalRel of R is symmetric;

        let u,v be Element of R;

        assume u in (( tau R) . v);

        then u in (( UncertaintyMap R) . v) by A1, UncEqTau;

        then [u, v] in the InternalRel of R by For3;

        hence v in (( tau R) . u) by For3A;

      end;

      assume

       Z0: for u,v be Element of R holds u in (( tau R) . v) implies v in (( tau R) . u);

      for a,b be object st [a, b] in the InternalRel of R holds [b, a] in the InternalRel of R

      proof

        let a,b be object;

        assume

         Z1: [a, b] in the InternalRel of R;

        then

        reconsider aa = a, bb = b as Element of R by Lemacik;

        bb in (( tau R) . aa) by Z1, For3A;

        then aa in (( tau R) . bb) by Z0;

        hence thesis by For3A;

      end;

      hence thesis by PREFER_1: 20;

    end;

    theorem :: ROUGHS_5:13



     UApF0: ( f_0 R) = ( UAp R)

    proof

      set ff = ( f_0 R);

      set gg = ( UAp R);

      for x be Subset of R holds (ff . x) = (gg . x)

      proof

        let x be Subset of R;



         WW: { u where u be Element of R : (( tau R) . u) meets x } = { w where w be Element of R : ( Class (the InternalRel of R,w)) meets x }

        proof

          thus { u where u be Element of R : (( tau R) . u) meets x } c= { w where w be Element of R : ( Class (the InternalRel of R,w)) meets x }

          proof

            let t be object;

            assume t in { u where u be Element of R : (( tau R) . u) meets x };

            then

            consider u be Element of R such that

             W1: u = t & (( tau R) . u) meets x;

            consider tt be object such that

             W2: tt in (( tau R) . u) & tt in x by XBOOLE_0: 3, W1;



             W4: (( tau R) . u) = ( Im (the InternalRel of R,u)) by DefTau;

            reconsider ttt = tt as Element of R by W2;

            thus thesis by W1, W4;

          end;

          let t be object;

          assume t in { w where w be Element of R : ( Class (the InternalRel of R,w)) meets x };

          then

          consider tt be Element of R such that

           H1: tt = t & ( Class (the InternalRel of R,tt)) meets x;

          consider wx be object such that

           H2: wx in ( Class (the InternalRel of R,tt)) & wx in x by H1, XBOOLE_0: 3;

          reconsider wxx = wx as Element of R by H2;

          (( tau R) . tt) = ( Im (the InternalRel of R,tt)) by DefTau;

          hence thesis by H1;

        end;

        (ff . x) = ( UAp x) by WW, Defff

        .= (gg . x) by ROUGHS_2:def 11;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: ROUGHS_5:14



     FlipLAp: ( Flip ( f_0 R)) = ( LAp R)

    proof

      ( f_0 R) = ( UAp R) by UApF0;

      hence thesis by ROUGHS_2: 27;

    end;

    theorem :: ROUGHS_5:15

    for R be Approximation_Space holds for x be Subset of R holds (( f_0 R) . x) is exact

    proof

      let R be Approximation_Space;

      let x be Subset of R;

      (( f_0 R) . x) = (( UAp R) . x) by UApF0

      .= ( UAp x) by ROUGHS_2:def 11;

      hence thesis;

    end;

    theorem :: ROUGHS_5:16

    the InternalRel of R is total reflexive implies ( id ( bool the carrier of R)) cc= ( f_0 R)

    proof

      assume

       zz: the InternalRel of R is total reflexive;

      set f = ( id ( bool the carrier of R));

      set g = ( f_0 R);



       A1: ( dom f) c= ( dom g) by FUNCT_2:def 1;

      for i be set st i in ( dom f) holds (f . i) c= (g . i)

      proof

        let i be set;

        assume

         k2: i in ( dom f);

        then

        reconsider ii = i as Subset of R;

        i c= { u where u be Element of R : (( tau R) . u) meets ii }

        proof

          let y be object;

          assume

           D1: y in i;

          then

          reconsider wy = y as Element of R by k2;

           [wy, wy] in the InternalRel of R by zz, LATTAD_1: 1;

          then wy in (( tau R) . wy) by For3A;

          then (( tau R) . wy) meets ii by XBOOLE_0: 3, D1;

          hence thesis;

        end;

        hence (f . i) c= (g . i) by Defff;

      end;

      hence thesis by A1, ALTCAT_2:def 1;

    end;

    theorem :: ROUGHS_5:17

    R is reflexive implies ( Flip ( f_0 R)) cc= ( id ( bool the carrier of R))

    proof

      assume

       A0: R is reflexive;

      ( Flip ( f_0 R)) = ( LAp R) by FlipLAp;

      hence thesis by A0, LApId;

    end;

    theorem :: ROUGHS_5:18

    the InternalRel of R is total reflexive implies ( id ( bool the carrier of R)) cc= ( f_1 R)

    proof

      assume

       zz: the InternalRel of R is total reflexive;

      set f = ( id ( bool the carrier of R));

      set g = ( f_1 R);



       A1: ( dom f) c= ( dom g) by FUNCT_2:def 1;

      for i be set st i in ( dom f) holds (f . i) c= (g . i)

      proof

        let i be set;

        assume

         k2: i in ( dom f);

        then

        reconsider ii = i as Subset of R;

        i c= { u where u be Element of R : (( UncertaintyMap R) . u) meets ii }

        proof

          let y be object;

          assume

           D1: y in i;

          then

          reconsider wy = y as Element of R by k2;

           [wy, wy] in the InternalRel of R by zz, LATTAD_1: 1;

          then wy in (( UncertaintyMap R) . wy) by For3;

          then (( UncertaintyMap R) . wy) meets ii by XBOOLE_0: 3, D1;

          hence thesis;

        end;

        hence (f . i) c= (g . i) by Defff;

      end;

      hence thesis by A1, ALTCAT_2:def 1;

    end;

    reserve f for Function of the carrier of R, ( bool the carrier of R);

    theorem :: ROUGHS_5:19



     Proph: (( ff_0 f) . {} ) = {}

    proof

      { u where u be Element of R : (f . u) meets ( {} R) } c= {}

      proof

        let y be object;

        assume y in { u where u be Element of R : (f . u) meets ( {} R) };

        then

        consider u be Element of R such that

         A1: u = y & (f . u) meets ( {} R);

        thus thesis by A1;

      end;

      hence thesis by Defff;

    end;

    registration

      let R;

      let f;

      cluster ( ff_0 f) -> empty-preserving;

      coherence by Proph;

    end

    theorem :: ROUGHS_5:20

    (( f_0 R) . {} ) = {}

    proof

      { u where u be Element of R : (( tau R) . u) meets ( {} R) } c= {}

      proof

        let y be object;

        assume y in { u where u be Element of R : (( tau R) . u) meets ( {} R) };

        then

        consider u be Element of R such that

         A1: u = y & (( tau R) . u) meets ( {} R);

        thus thesis by A1;

      end;

      hence thesis by Defff;

    end;

    theorem :: ROUGHS_5:21

    (( f_1 R) . {} ) = {}

    proof

      { u where u be Element of R : (( UncertaintyMap R) . u) meets ( {} R) } c= {}

      proof

        let y be object;

        assume y in { u where u be Element of R : (( UncertaintyMap R) . u) meets ( {} R) };

        then

        consider u be Element of R such that

         A1: u = y & (( UncertaintyMap R) . u) meets ( {} R);

        thus thesis by A1;

      end;

      hence thesis by Defff;

    end;

    registration

      let R be non empty reflexive RelStr;

      cluster the InternalRel of R -> total reflexive;

      coherence ;

    end

    theorem :: ROUGHS_5:22

    f is map-reflexive implies (( ff_0 f) . the carrier of R) = the carrier of R

    proof

      assume

       RR: f is map-reflexive;



       A0: (( ff_0 f) . ( [#] R)) = { u where u be Element of R : (f . u) meets ( [#] R) } by Defff;

      the carrier of R c= { u where u be Element of R : (f . u) meets ( [#] R) }

      proof

        let y be object;

        assume y in the carrier of R;

        then

        reconsider u = y as Element of R;

        u in (f . u) by RR;

        then

        consider u be Element of R such that

         A1: u = y & (f . u) meets ( [#] R) by XBOOLE_0: 3;

        thus thesis by A1;

      end;

      hence thesis by A0;

    end;

    theorem :: ROUGHS_5:23

    the InternalRel of R is reflexive total implies (( f_0 R) . the carrier of R) = the carrier of R

    proof

      assume

       RR: the InternalRel of R is reflexive total;



       A0: (( f_0 R) . ( [#] R)) = { u where u be Element of R : (( tau R) . u) meets ( [#] R) } by Defff;

      the carrier of R c= { u where u be Element of R : (( tau R) . u) meets ( [#] R) }

      proof

        let y be object;

        assume y in the carrier of R;

        then

        reconsider u = y as Element of R;



         ZZ: (( tau R) . u) = ( Im (the InternalRel of R,u)) by DefTau;

         [u, u] in the InternalRel of R by LATTAD_1: 1, RR;

        then u in (( tau R) . u) by RELAT_1: 169, ZZ;

        then

        consider u be Element of R such that

         A1: u = y & (( tau R) . u) meets ( [#] R) by XBOOLE_0: 3;

        thus thesis by A1;

      end;

      hence thesis by A0;

    end;

    theorem :: ROUGHS_5:24

    the InternalRel of R is reflexive total implies (( f_1 R) . the carrier of R) = the carrier of R

    proof

      assume

       RR: the InternalRel of R is reflexive total;



       A0: (( f_1 R) . ( [#] R)) = { u where u be Element of R : (( UncertaintyMap R) . u) meets ( [#] R) } by Defff;

      the carrier of R c= { u where u be Element of R : (( UncertaintyMap R) . u) meets ( [#] R) }

      proof

        let y be object;

        assume y in the carrier of R;

        then

        reconsider u = y as Element of R;

         [u, u] in the InternalRel of R by LATTAD_1: 1, RR;

        then u in (( UncertaintyMap R) . u) by For3;

        then

        consider u be Element of R such that

         A1: u = y & (( UncertaintyMap R) . u) meets ( [#] R) by XBOOLE_0: 3;

        thus thesis by A1;

      end;

      hence thesis by A0;

    end;

    theorem :: ROUGHS_5:25

    for u,w be Element of R, x be Subset of R st (f . u) = (f . w) holds u in (( ff_0 f) . x) iff w in (( ff_0 f) . x)

    proof

      let u,w be Element of R, x be Subset of R;

      assume

       AA: (f . u) = (f . w);



       A3: (( ff_0 f) . x) = { w where w be Element of R : (f . w) meets x } by Defff;

      thus u in (( ff_0 f) . x) implies w in (( ff_0 f) . x)

      proof

        assume

         A1: u in (( ff_0 f) . x);

        consider v be Element of R such that

         A2: u = v & (f . v) meets x by A1, A3;

        thus w in (( ff_0 f) . x) by A3, AA, A2;

      end;

      assume w in (( ff_0 f) . x);

      then

      consider v be Element of R such that

       A2: w = v & (f . v) meets x by A3;

      thus thesis by A3, AA, A2;

    end;

    theorem :: ROUGHS_5:26

    for u,w be Element of R, x be Subset of R st (( UncertaintyMap R) . u) = (( UncertaintyMap R) . w) holds u in (( f_1 R) . x) iff w in (( f_1 R) . x)

    proof

      let u,w be Element of R, x be Subset of R;

      assume

       AA: (( UncertaintyMap R) . u) = (( UncertaintyMap R) . w);



       A3: (( f_1 R) . x) = { w where w be Element of R : (( UncertaintyMap R) . w) meets x } by Defff;

      thus u in (( f_1 R) . x) implies w in (( f_1 R) . x)

      proof

        assume

         A1: u in (( f_1 R) . x);

        consider v be Element of R such that

         A2: u = v & (( UncertaintyMap R) . v) meets x by A1, A3;

        thus w in (( f_1 R) . x) by A3, AA, A2;

      end;

      assume w in (( f_1 R) . x);

      then

      consider v be Element of R such that

       A2: w = v & (( UncertaintyMap R) . v) meets x by A3;

      thus thesis by A3, AA, A2;

    end;

    theorem :: ROUGHS_5:27

    for u,w be Element of R, x be Subset of R st (( tau R) . u) = (( tau R) . w) holds u in (( f_0 R) . x) iff w in (( f_0 R) . x)

    proof

      let u,w be Element of R, x be Subset of R;

      assume

       AA: (( tau R) . u) = (( tau R) . w);



       A3: (( f_0 R) . x) = { w where w be Element of R : (( tau R) . w) meets x } by Defff;

      thus u in (( f_0 R) . x) implies w in (( f_0 R) . x)

      proof

        assume u in (( f_0 R) . x);

        then

        consider v be Element of R such that

         A2: u = v & (( tau R) . v) meets x by A3;

        thus w in (( f_0 R) . x) by A3, AA, A2;

      end;

      assume w in (( f_0 R) . x);

      then

       A2: ex v be Element of R st w = v & (( tau R) . v) meets x by A3;

      thus thesis by A3, AA, A2;

    end;

    theorem :: ROUGHS_5:28



     FlipFF: for f be Function of the carrier of R, ( bool the carrier of R) holds for x be Subset of R holds (( Flip ( ff_0 f)) . x) = { w where w be Element of R : (f . w) c= x }

    proof

      let f be Function of the carrier of R, ( bool the carrier of R);

      let x be Subset of R;



       ZZ: (( ff_0 f) . (x ` )) = { w where w be Element of R : (f . w) meets (x ` ) } by Defff;

      thus (( Flip ( ff_0 f)) . x) c= { w where w be Element of R : (f . w) c= x }

      proof

        let y be object;

        assume

         S1: y in (( Flip ( ff_0 f)) . x);

        then y in ((( ff_0 f) . (x ` )) ` ) by ROUGHS_2:def 14;

        then

         Z1: not y in (( ff_0 f) . (x ` )) by XBOOLE_0:def 5;

        reconsider yy = y as Element of R by S1;

        (f . yy) misses (x ` ) by Z1, ZZ;

        then (f . yy) c= x by SUBSET_1: 24;

        hence thesis;

      end;

      let y be object;

      assume y in { w where w be Element of R : (f . w) c= x };

      then

      consider w be Element of R such that

       L1: y = w & (f . w) c= x;

      reconsider yy = y as Element of R by L1;

       not yy in (( ff_0 f) . (x ` ))

      proof

        assume yy in (( ff_0 f) . (x ` ));

        then

        consider v be Element of R such that

         L2: yy = v & (f . v) meets (x ` ) by ZZ;

        thus thesis by L1, L2, SUBSET_1: 24;

      end;

      then yy in ((( ff_0 f) . (x ` )) ` ) by XBOOLE_0:def 5;

      hence thesis by ROUGHS_2:def 14;

    end;

    theorem :: ROUGHS_5:29



     FlipF0: for x be Subset of R holds (( Flip ( f_0 R)) . x) = { w where w be Element of R : (( tau R) . w) c= x }

    proof

      let x be Subset of R;



       ZZ: (( f_0 R) . (x ` )) = { w where w be Element of R : (( tau R) . w) meets (x ` ) } by Defff;

      thus (( Flip ( f_0 R)) . x) c= { w where w be Element of R : (( tau R) . w) c= x }

      proof

        let y be object;

        assume

         S1: y in (( Flip ( f_0 R)) . x);

        then y in ((( f_0 R) . (x ` )) ` ) by ROUGHS_2:def 14;

        then

         Z1: not y in (( f_0 R) . (x ` )) by XBOOLE_0:def 5;

        reconsider yy = y as Element of R by S1;

        (( tau R) . yy) misses (x ` ) by Z1, ZZ;

        then (( tau R) . yy) c= x by SUBSET_1: 24;

        hence thesis;

      end;

      let y be object;

      assume y in { w where w be Element of R : (( tau R) . w) c= x };

      then

      consider w be Element of R such that

       L1: y = w & (( tau R) . w) c= x;

      reconsider yy = y as Element of R by L1;

       not yy in (( f_0 R) . (x ` ))

      proof

        assume yy in (( f_0 R) . (x ` ));

        then ex v be Element of R st yy = v & (( tau R) . v) meets (x ` ) by ZZ;

        hence thesis by L1, SUBSET_1: 24;

      end;

      then yy in ((( f_0 R) . (x ` )) ` ) by XBOOLE_0:def 5;

      hence thesis by ROUGHS_2:def 14;

    end;

    theorem :: ROUGHS_5:30



     FlipF1: for x be Subset of R holds (( Flip ( f_1 R)) . x) = { w where w be Element of R : (( UncertaintyMap R) . w) c= x }

    proof

      let x be Subset of R;



       ZZ: (( f_1 R) . (x ` )) = { w where w be Element of R : (( UncertaintyMap R) . w) meets (x ` ) } by Defff;

      thus (( Flip ( f_1 R)) . x) c= { w where w be Element of R : (( UncertaintyMap R) . w) c= x }

      proof

        let y be object;

        assume

         S1: y in (( Flip ( f_1 R)) . x);

        then y in ((( f_1 R) . (x ` )) ` ) by ROUGHS_2:def 14;

        then

         Z1: not y in (( f_1 R) . (x ` )) by XBOOLE_0:def 5;

        reconsider yy = y as Element of R by S1;

        (( UncertaintyMap R) . yy) misses (x ` ) by Z1, ZZ;

        then (( UncertaintyMap R) . yy) c= x by SUBSET_1: 24;

        hence thesis;

      end;

      let y be object;

      assume y in { w where w be Element of R : (( UncertaintyMap R) . w) c= x };

      then

      consider w be Element of R such that

       L1: y = w & (( UncertaintyMap R) . w) c= x;

      reconsider yy = y as Element of R by L1;

       not yy in (( f_1 R) . (x ` ))

      proof

        assume yy in (( f_1 R) . (x ` ));

        then ex v be Element of R st yy = v & (( UncertaintyMap R) . v) meets (x ` ) by ZZ;

        hence thesis by L1, SUBSET_1: 24;

      end;

      then yy in ((( f_1 R) . (x ` )) ` ) by XBOOLE_0:def 5;

      hence thesis by ROUGHS_2:def 14;

    end;

    theorem :: ROUGHS_5:31

    for u,w be Element of R, x be Subset of R st (f . u) = (f . w) holds u in (( Flip ( ff_0 f)) . x) iff w in (( Flip ( ff_0 f)) . x)

    proof

      let u,w be Element of R, x be Subset of R;

      assume

       AA: (f . u) = (f . w);



       A3: (( Flip ( ff_0 f)) . x) = { w where w be Element of R : (f . w) c= x } by FlipFF;

      thus u in (( Flip ( ff_0 f)) . x) implies w in (( Flip ( ff_0 f)) . x)

      proof

        assume u in (( Flip ( ff_0 f)) . x);

        then

        consider v be Element of R such that

         A2: u = v & (f . v) c= x by A3;

        thus w in (( Flip ( ff_0 f)) . x) by A3, AA, A2;

      end;

      assume w in (( Flip ( ff_0 f)) . x);

      then ex v be Element of R st w = v & (f . v) c= x by A3;

      hence thesis by A3, AA;

    end;

    theorem :: ROUGHS_5:32

    for u,w be Element of R, x be Subset of R st (( tau R) . u) = (( tau R) . w) holds u in (( Flip ( f_0 R)) . x) iff w in (( Flip ( f_0 R)) . x)

    proof

      let u,w be Element of R, x be Subset of R;

      assume

       AA: (( tau R) . u) = (( tau R) . w);



       A3: (( Flip ( f_0 R)) . x) = { w where w be Element of R : (( tau R) . w) c= x } by FlipF0;

      thus u in (( Flip ( f_0 R)) . x) implies w in (( Flip ( f_0 R)) . x)

      proof

        assume u in (( Flip ( f_0 R)) . x);

        then

        consider v be Element of R such that

         A2: u = v & (( tau R) . v) c= x by A3;

        thus w in (( Flip ( f_0 R)) . x) by A3, AA, A2;

      end;

      assume w in (( Flip ( f_0 R)) . x);

      then ex v be Element of R st w = v & (( tau R) . v) c= x by A3;

      hence thesis by A3, AA;

    end;

    theorem :: ROUGHS_5:33

    for u,w be Element of R, x be Subset of R st (( UncertaintyMap R) . u) = (( UncertaintyMap R) . w) holds u in (( Flip ( f_1 R)) . x) iff w in (( Flip ( f_1 R)) . x)

    proof

      let u,w be Element of R, x be Subset of R;

      assume

       AA: (( UncertaintyMap R) . u) = (( UncertaintyMap R) . w);



       A3: (( Flip ( f_1 R)) . x) = { w where w be Element of R : (( UncertaintyMap R) . w) c= x } by FlipF1;

      thus u in (( Flip ( f_1 R)) . x) implies w in (( Flip ( f_1 R)) . x)

      proof

        assume u in (( Flip ( f_1 R)) . x);

        then

        consider v be Element of R such that

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

        thus w in (( Flip ( f_1 R)) . x) by A3, AA, A2;

      end;

      assume w in (( Flip ( f_1 R)) . x);

      then ex v be Element of R st w = v & (( UncertaintyMap R) . v) c= x by A3;

      hence thesis by A3, AA;

    end;

    theorem :: ROUGHS_5:34



     ReflUnc: R is reflexive implies for w be Element of R holds w in (( UncertaintyMap R) . w)

    proof

      assume

       aa: R is reflexive;

      let w be Element of R;

       [w, w] in the InternalRel of R by aa, LATTAD_1: 1;

      hence thesis by For3;

    end;

    theorem :: ROUGHS_5:35



     ReflTau: R is reflexive implies for w be Element of R holds w in (( tau R) . w)

    proof

      assume

       aa: R is reflexive;

      let w be Element of R;

       [w, w] in the InternalRel of R by aa, LATTAD_1: 1;

      hence thesis by For3A;

    end;

    registration

      let R be reflexive non empty RelStr;

      cluster ( UncertaintyMap R) -> map-reflexive;

      coherence by ReflUnc;

      cluster ( tau R) -> map-reflexive;

      coherence by ReflTau;

    end

    theorem :: ROUGHS_5:36

    R is reflexive implies ( Flip ( f_1 R)) cc= ( id ( bool the carrier of R))

    proof

      assume

       TT: R is reflexive;

      set f = ( Flip ( f_1 R));

      set g = ( id ( bool the carrier of R));



       A1: ( dom f) c= ( dom g);

      for i be set st i in ( dom f) holds (f . i) c= (g . i)

      proof

        let i be set;

        assume i in ( dom f);

        then

        reconsider ii = i as Subset of R;

        { w where w be Element of R : (( UncertaintyMap R) . w) c= ii } c= ii

        proof

          let r be object;

          assume r in { w where w be Element of R : (( UncertaintyMap R) . w) c= ii };

          then

          consider w be Element of R such that

           C4: r = w & (( UncertaintyMap R) . w) c= ii;

          thus thesis by C4, TT, ReflUnc;

        end;

        hence thesis by FlipF1;

      end;

      hence thesis by A1, ALTCAT_2:def 1;

    end;

    theorem :: ROUGHS_5:37

    (( f_0 R) * ( f_0 R)) = ( f_0 R) iff (( Flip ( f_0 R)) * ( Flip ( f_0 R))) = ( Flip ( f_0 R))

    proof

      thus (( f_0 R) * ( f_0 R)) = ( f_0 R) implies (( Flip ( f_0 R)) * ( Flip ( f_0 R))) = ( Flip ( f_0 R)) by FlipCompose;

      assume (( Flip ( f_0 R)) * ( Flip ( f_0 R))) = ( Flip ( f_0 R));

      then ( Flip (( Flip ( f_0 R)) * ( Flip ( f_0 R)))) = ( f_0 R) by ROUGHS_2: 23;



      then ( f_0 R) = (( Flip ( Flip ( f_0 R))) * ( Flip ( Flip ( f_0 R)))) by FlipCompose

      .= (( f_0 R) * ( Flip ( Flip ( f_0 R)))) by ROUGHS_2: 23

      .= (( f_0 R) * ( f_0 R)) by ROUGHS_2: 23;

      hence thesis;

    end;

    theorem :: ROUGHS_5:38

    R is reflexive implies ( union (( UncertaintyMap R) .: ( [#] R))) = the carrier of R

    proof

      assume

       AA: R is reflexive;



       B1: the carrier of R c= ( union (( UncertaintyMap R) .: ( [#] R)))

      proof

        let t be object;

        assume t in the carrier of R;

        then

        reconsider tt = t as Element of R;

        ( dom ( UncertaintyMap R)) = the carrier of R by FUNCT_2:def 1;

        then

         A2: tt in ( dom ( UncertaintyMap R)) & tt in ( [#] R);



         A3: tt in (( UncertaintyMap R) . t) by AA, ReflUnc;

        (( UncertaintyMap R) . t) in (( UncertaintyMap R) .: ( [#] R)) by A2, FUNCT_1:def 6;

        hence thesis by TARSKI:def 4, A3;

      end;

      ( union (( UncertaintyMap R) .: ( [#] R))) c= the carrier of R

      proof

        let f be object;

        assume f in ( union (( UncertaintyMap R) .: ( [#] R)));

        then ex tt be set st f in tt & tt in (( UncertaintyMap R) .: ( [#] R)) by TARSKI:def 4;

        hence thesis;

      end;

      hence thesis by B1;

    end;



     F0Mono: ( f_0 R) is c=-monotone

    proof

      set f = ( f_0 R);

      for a,b be Subset of R st a c= b holds (f . a) c= (f . b)

      proof

        let a,b be Subset of R;

        assume

         A0: a c= b;



         A1: (f . a) = (( UAp R) . a) by UApF0

        .= ( UAp a) by ROUGHS_2:def 11;

        (f . b) = (( UAp R) . b) by UApF0

        .= ( UAp b) by ROUGHS_2:def 11;

        hence thesis by A1, A0, ROUGHS_2: 15;

      end;

      hence thesis;

    end;



     F1Mono: ( f_1 R) is c=-monotone

    proof

      set f = ( f_1 R);

      for a,b be Subset of R st a c= b holds (f . a) c= (f . b)

      proof

        let a,b be Subset of R;

        assume

         A0: a c= b;



         A2: { u where u be Element of R : (( UncertaintyMap R) . u) meets a } c= { u where u be Element of R : (( UncertaintyMap R) . u) meets b }

        proof

          let t be object;

          assume t in { u where u be Element of R : (( UncertaintyMap R) . u) meets a };

          then

          consider u be Element of R such that

           B1: u = t & (( UncertaintyMap R) . u) meets a;

          (( UncertaintyMap R) . u) meets b by A0, B1, XBOOLE_1: 63;

          hence thesis by B1;

        end;

        (f . a) = { u where u be Element of R : (( UncertaintyMap R) . u) meets a } by Defff;

        hence thesis by A2, Defff;

      end;

      hence thesis;

    end;

    registration

      let R be non empty RelStr;

      cluster ( f_0 R) -> c=-monotone;

      coherence by F0Mono;

      cluster ( f_1 R) -> c=-monotone;

      coherence by F1Mono;

    end

    theorem :: ROUGHS_5:39



     FlipMono: for f be map of R st f is c=-monotone holds ( Flip f) is c=-monotone

    proof

      let f be map of R;

      set g = ( Flip f);

      assume

       A1: f is c=-monotone;

      for A,B be Subset of R st A c= B holds (g . A) c= (g . B)

      proof

        let A,B be Subset of R;

        assume A c= B;

        then (B ` ) c= (A ` ) by SUBSET_1: 12;

        then (f . (B ` )) c= (f . (A ` )) by A1;

        then ((f . (A ` )) ` ) c= ((f . (B ` )) ` ) by SUBSET_1: 12;

        then (g . A) c= ((f . (B ` )) ` ) by ROUGHS_2:def 14;

        hence thesis by ROUGHS_2:def 14;

      end;

      hence thesis;

    end;

    theorem :: ROUGHS_5:40

    ( Flip ( f_0 R)) is c=-monotone by FlipMono;

    theorem :: ROUGHS_5:41

    ( Flip ( f_1 R)) is c=-monotone by FlipMono;

    theorem :: ROUGHS_5:42



     Propj: for f be Function of the carrier of R, ( bool the carrier of R) holds for x,y be Subset of R holds (( ff_0 f) . (x \/ y)) = ((( ff_0 f) . x) \/ (( ff_0 f) . y))

    proof

      let f be Function of the carrier of R, ( bool the carrier of R);

      let x,y be Subset of R;



       AA: (( ff_0 f) . (x \/ y)) = { u where u be Element of R : (f . u) meets (x \/ y) } by Defff;



       AB: (( ff_0 f) . x) = { u where u be Element of R : (f . u) meets x } by Defff;



       AC: (( ff_0 f) . y) = { u where u be Element of R : (f . u) meets y } by Defff;

      thus (( ff_0 f) . (x \/ y)) c= ((( ff_0 f) . x) \/ (( ff_0 f) . y))

      proof

        let t be object;

        assume t in (( ff_0 f) . (x \/ y));

        then

        consider u be Element of R such that

         A1: t = u & (f . u) meets (x \/ y) by AA;

        (f . u) meets x or (f . u) meets y by A1, XBOOLE_1: 70;

        then t in (( ff_0 f) . x) or t in (( ff_0 f) . y) by A1, AB, AC;

        hence thesis by XBOOLE_0:def 3;

      end;

      let t be object;

      assume t in ((( ff_0 f) . x) \/ (( ff_0 f) . y));

      per cases by XBOOLE_0:def 3;

        suppose t in (( ff_0 f) . x);

        then

        consider u be Element of R such that

         A1: t = u & (f . u) meets x by AB;

        (f . u) meets (x \/ y) by XBOOLE_1: 70, A1;

        hence thesis by A1, AA;

      end;

        suppose t in (( ff_0 f) . y);

        then

        consider u be Element of R such that

         A1: t = u & (f . u) meets y by AC;

        (f . u) meets (x \/ y) by XBOOLE_1: 70, A1;

        hence thesis by A1, AA;

      end;

    end;

    theorem :: ROUGHS_5:43

    for x,y be Subset of R holds (( f_0 R) . (x \/ y)) = ((( f_0 R) . x) \/ (( f_0 R) . y)) by Propj;

    theorem :: ROUGHS_5:44

    for x,y be Subset of R holds (( f_1 R) . (x \/ y)) = ((( f_1 R) . x) \/ (( f_1 R) . y)) by Propj;

    theorem :: ROUGHS_5:45



     Propk: for f be Function of the carrier of R, ( bool the carrier of R) holds for x,y be Subset of R holds ((( Flip ( ff_0 f)) . x) \/ (( Flip ( ff_0 f)) . y)) c= (( Flip ( ff_0 f)) . (x \/ y))

    proof

      let f be Function of the carrier of R, ( bool the carrier of R);

      let x,y be Subset of R;



       AA: (( Flip ( ff_0 f)) . (x \/ y)) = { u where u be Element of R : (f . u) c= (x \/ y) } by FlipFF;



       AB: (( Flip ( ff_0 f)) . x) = { u where u be Element of R : (f . u) c= x } by FlipFF;



       AC: (( Flip ( ff_0 f)) . y) = { u where u be Element of R : (f . u) c= y } by FlipFF;



       XX: x c= (x \/ y) & y c= (x \/ y) by XBOOLE_1: 7;

      let t be object;

      assume t in ((( Flip ( ff_0 f)) . x) \/ (( Flip ( ff_0 f)) . y));

      per cases by XBOOLE_0:def 3;

        suppose t in (( Flip ( ff_0 f)) . x);

        then

        consider u be Element of R such that

         A1: t = u & (f . u) c= x by AB;

        (f . u) c= (x \/ y) by A1, XX;

        hence thesis by A1, AA;

      end;

        suppose t in (( Flip ( ff_0 f)) . y);

        then

        consider u be Element of R such that

         A1: t = u & (f . u) c= y by AC;

        (f . u) c= (x \/ y) by A1, XX;

        hence thesis by A1, AA;

      end;

    end;

    theorem :: ROUGHS_5:46

    for x,y be Subset of R holds ((( Flip ( f_0 R)) . x) \/ (( Flip ( f_0 R)) . y)) c= (( Flip ( f_0 R)) . (x \/ y)) by Propk;

    theorem :: ROUGHS_5:47

    for x,y be Subset of R holds ((( Flip ( f_1 R)) . x) \/ (( Flip ( f_1 R)) . y)) c= (( Flip ( f_1 R)) . (x \/ y)) by Propk;

    theorem :: ROUGHS_5:48



     Propl: for f be Function of the carrier of R, ( bool the carrier of R) holds for x,y be Subset of R holds (( ff_0 f) . (x /\ y)) c= ((( ff_0 f) . x) /\ (( ff_0 f) . y))

    proof

      let f be Function of the carrier of R, ( bool the carrier of R);

      let x,y be Subset of R;



       AB: (( ff_0 f) . x) = { u where u be Element of R : (f . u) meets x } by Defff;



       AC: (( ff_0 f) . y) = { u where u be Element of R : (f . u) meets y } by Defff;

      let t be object;

      assume t in (( ff_0 f) . (x /\ y));

      then t in { u where u be Element of R : (f . u) meets (x /\ y) } by Defff;

      then

      consider u be Element of R such that

       A1: t = u & (f . u) meets (x /\ y);

      (f . u) meets x & (f . u) meets y by A1, XBOOLE_1: 74;

      then t in (( ff_0 f) . x) & t in (( ff_0 f) . y) by A1, AB, AC;

      hence thesis by XBOOLE_0:def 4;

    end;

    theorem :: ROUGHS_5:49

    for x,y be Subset of R holds (( f_0 R) . (x /\ y)) c= ((( f_0 R) . x) /\ (( f_0 R) . y)) by Propl;

    theorem :: ROUGHS_5:50

    for x,y be Subset of R holds (( f_1 R) . (x /\ y)) c= ((( f_1 R) . x) /\ (( f_1 R) . y)) by Propl;

    theorem :: ROUGHS_5:51



     Propm: for f be Function of the carrier of R, ( bool the carrier of R) holds for x,y be Subset of R holds ((( Flip ( ff_0 f)) . x) /\ (( Flip ( ff_0 f)) . y)) = (( Flip ( ff_0 f)) . (x /\ y))

    proof

      let f be Function of the carrier of R, ( bool the carrier of R);

      let x,y be Subset of R;



       AA: (( ff_0 f) . ((x /\ y) ` )) = { u where u be Element of R : (f . u) meets ((x /\ y) ` ) } by Defff;



       AB: (( ff_0 f) . (x ` )) = { u where u be Element of R : (f . u) meets (x ` ) } by Defff;



       AC: (( ff_0 f) . (y ` )) = { u where u be Element of R : (f . u) meets (y ` ) } by Defff;

      thus ((( Flip ( ff_0 f)) . x) /\ (( Flip ( ff_0 f)) . y)) c= (( Flip ( ff_0 f)) . (x /\ y))

      proof

        let t be object;

        assume

         zz: t in ((( Flip ( ff_0 f)) . x) /\ (( Flip ( ff_0 f)) . y));

        then

         ZZ: t in (( Flip ( ff_0 f)) . x) & t in (( Flip ( ff_0 f)) . y) by XBOOLE_0:def 4;

        then t in ((( ff_0 f) . (x ` )) ` ) by ROUGHS_2:def 14;

        then

         Z1: not t in (( ff_0 f) . (x ` )) by XBOOLE_0:def 5;

        t in ((( ff_0 f) . (y ` )) ` ) by ZZ, ROUGHS_2:def 14;

        then

         V1: not t in (( ff_0 f) . (y ` )) by XBOOLE_0:def 5;

         not t in (( ff_0 f) . ((x /\ y) ` ))

        proof

          assume t in (( ff_0 f) . ((x /\ y) ` ));

          then

          consider w be Element of R such that

           A1: t = w & (f . w) meets ((x /\ y) ` ) by AA;

          (f . w) meets ((x ` ) \/ (y ` )) by XBOOLE_1: 54, A1;

          per cases by XBOOLE_1: 70;

            suppose (f . w) meets (x ` );

            hence thesis by Z1, A1, AB;

          end;

            suppose (f . w) meets (y ` );

            hence thesis by V1, AC, A1;

          end;

        end;

        then t in ((( ff_0 f) . ((x /\ y) ` )) ` ) by zz, XBOOLE_0:def 5;

        hence thesis by ROUGHS_2:def 14;

      end;

      let t be object;

      assume

       v0: t in (( Flip ( ff_0 f)) . (x /\ y));

      then t in ((( ff_0 f) . ((x /\ y) ` )) ` ) by ROUGHS_2:def 14;

      then

       ww: not t in { u where u be Element of R : (f . u) meets ((x /\ y) ` ) } by AA, XBOOLE_0:def 5;



       vc: ((x /\ y) ` ) = ((x ` ) \/ (y ` )) by XBOOLE_1: 54;



       w1: not t in (( ff_0 f) . (x ` ))

      proof

        assume t in (( ff_0 f) . (x ` ));

        then

        consider w be Element of R such that

         A1: t = w & (f . w) meets (x ` ) by AB;

        (f . w) meets ((x /\ y) ` ) by vc, A1, XBOOLE_1: 63, XBOOLE_1: 7;

        hence thesis by ww, A1;

      end;



       z1: not t in (( ff_0 f) . (y ` ))

      proof

        assume t in (( ff_0 f) . (y ` ));

        then

        consider w be Element of R such that

         A1: t = w & (f . w) meets (y ` ) by AC;

        (f . w) meets ((x /\ y) ` ) by vc, A1, XBOOLE_1: 63, XBOOLE_1: 7;

        hence thesis by ww, A1;

      end;

      t in ((( ff_0 f) . (x ` )) ` ) by w1, v0, XBOOLE_0:def 5;

      then

       W1: t in (( Flip ( ff_0 f)) . x) by ROUGHS_2:def 14;

      t in ((( ff_0 f) . (y ` )) ` ) by z1, v0, XBOOLE_0:def 5;

      then t in (( Flip ( ff_0 f)) . y) by ROUGHS_2:def 14;

      hence thesis by W1, XBOOLE_0:def 4;

    end;

    theorem :: ROUGHS_5:52

    for x,y be Subset of R holds ((( Flip ( f_0 R)) . x) /\ (( Flip ( f_0 R)) . y)) = (( Flip ( f_0 R)) . (x /\ y)) by Propm;

    theorem :: ROUGHS_5:53

    for x,y be Subset of R holds ((( Flip ( f_1 R)) . x) /\ (( Flip ( f_1 R)) . y)) = (( Flip ( f_1 R)) . (x /\ y)) by Propm;