roughs_2.miz

    begin

    registration

      cluster non empty void for RelStr;

      existence

      proof

        reconsider E = {} as Relation of 1 by RELSET_1: 12;

        set X = RelStr (# 1, E #);

        reconsider X as non empty RelStr;

        X is void;

        hence thesis;

      end;

    end

    theorem :: ROUGHS_2:1



     Th1: for R be total non empty RelStr, x be Element of R holds x in ( field the InternalRel of R)

    proof

      let R be total non empty RelStr;

      let x be Element of R;

      ( dom the InternalRel of R) = the carrier of R by PARTFUN1:def 2;

      hence thesis by XBOOLE_0:def 3;

    end;

    theorem :: ROUGHS_2:2



     Th2: for R be non empty 1-sorted, X be Subset of R holds { x where x be Element of R : {} c= X } = ( [#] R)

    proof

      let R be non empty 1-sorted;

      let X be Subset of R;

      thus { x where x be Element of R : {} c= X } c= ( [#] R)

      proof

        let y be object;

        assume y in { x where x be Element of R : {} c= X };

        then ex z be Element of R st z = y & {} c= X;

        hence thesis;

      end;

      let y be object;

      assume

       A1: y in ( [#] R);

      y in { x where x be Element of R : {} c= X }

      proof

        assume not y in { x where x be Element of R : {} c= X };

        then not y is Element of R or not {} c= X;

        hence contradiction by A1;

      end;

      hence thesis;

    end;

    theorem :: ROUGHS_2:3



     Th3: for R be 1-sorted, X be Subset of R holds { x where x be Element of R : {} meets X } = ( {} R)

    proof

      let R be 1-sorted;

      let X be Subset of R;

      thus { x where x be Element of R : {} meets X } c= ( {} R)

      proof

        let y be object;

        assume y in { x where x be Element of R : {} meets X };

        then ex z be Element of R st z = y & {} meets X;

        then ( {} /\ X) <> {} ;

        hence thesis;

      end;

      thus thesis;

    end;

    begin

    definition

      let R be Relation, X be set;

      :: ROUGHS_2:def1

      pred R is_serial_in X means

      : Def1: for x be object st x in X holds ex y be object st y in X & [x, y] in R;

    end

    definition

      let R be Relation;

      :: ROUGHS_2:def2

      attr R is serial means R is_serial_in ( field R);

    end

    definition

      let R be RelStr;

      :: ROUGHS_2:def3

      attr R is serial means

      : Def3: the InternalRel of R is_serial_in the carrier of R;

    end



     Lm1: for R be RelStr st the InternalRel of R is_reflexive_in the carrier of R holds R is serial

    proof

      let R be RelStr;

      assume

       A1: the InternalRel of R is_reflexive_in the carrier of R;

      set IR = the InternalRel of R, X = the carrier of R;

      for x be object st x in X holds ex y be object st y in X & [x, y] in IR

      proof

        let x be object;

        assume

         A2: x in X;

        then [x, x] in IR by A1, RELAT_2:def 1;

        hence thesis by A2;

      end;

      hence thesis by Def1;

    end;

    registration

      cluster reflexive -> serial for RelStr;

      coherence by Lm1, ORDERS_2:def 2;

    end

    definition

      let R be non empty RelStr;

      :: original: serial

      redefine

      :: ROUGHS_2:def4

      attr R is serial means for x be Element of R holds ex y be Element of R st x <= y;

      compatibility

      proof

        thus R is serial implies for x be Element of R holds ex y be Element of R st x <= y

        proof

          assume

           A1: R is serial;

          set IR = the InternalRel of R, X = the carrier of R;

          let x be Element of R;

          consider y be object such that

           A2: y in X & [x, y] in IR by Def1, A1;

          thus thesis by A2, ORDERS_2:def 5;

        end;

        assume

         A3: for x be Element of R holds ex y be Element of R st x <= y;

        the InternalRel of R is_serial_in the carrier of R

        proof

          let x be object;

          assume x in the carrier of R;

          then

          reconsider xx = x as Element of R;

          consider y be Element of R such that

           A4: xx <= y by A3;

          take y;

          thus thesis by A4, ORDERS_2:def 5;

        end;

        hence thesis;

      end;

    end

    registration

      cluster total -> serial for RelStr;

      coherence

      proof

        let R be RelStr;

        set RR = the InternalRel of R, X = the carrier of R;

        assume R is total;

        then

         A1: ( dom RR) = X by PARTFUN1:def 2;

        RR is_serial_in X

        proof

          let x be object;

          assume x in X;

          then

          consider y be object such that

           A2: [x, y] in RR by A1, RELSET_1: 9;

          take y;

          consider xx,yy be object such that

           A3: [x, y] = [xx, yy] & xx in X & yy in X by A2, RELSET_1: 2;

          thus thesis by A2, A3, XTUPLE_0: 1;

        end;

        hence thesis;

      end;

      cluster serial -> total for RelStr;

      coherence

      proof

        let R be RelStr;

        set RR = the InternalRel of R, X = the carrier of R;

        assume

         A4: R is serial;

        for x be object st x in X holds ex y be object st [x, y] in RR

        proof

          let x be object;

          assume x in X;

          then ex y be object st y in X & [x, y] in RR by Def1, A4;

          hence thesis;

        end;

        then ( dom RR) = X by RELSET_1: 9;

        then RR is total by PARTFUN1:def 2;

        hence thesis by ORDERS_2:def 1;

      end;

    end



     Lm2: for R be non empty serial RelStr, x be Element of R holds ( Class (the InternalRel of R,x)) <> {}

    proof

      let R be non empty serial RelStr;

      let x be Element of R;



       A1: x in {x} by TARSKI:def 1;

      consider y be object such that

       A2: y in the carrier of R & [x, y] in the InternalRel of R by Def1, Def3;

      thus thesis by RELAT_1:def 13, A2, A1;

    end;

    registration

      let R be non empty serial RelStr, x be Element of R;

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

      coherence by Lm2;

    end

    theorem :: ROUGHS_2:4



     Th4: for R be non empty reflexive RelStr, x be Element of R holds x in ( Class (the InternalRel of R,x))

    proof

      let R be non empty reflexive RelStr;

      let x be Element of R;



       A1: x in ( field the InternalRel of R) by Th1;



       A2: x in {x} by TARSKI:def 1;

       [x, x] in the InternalRel of R by A1, RELAT_2:def 1, RELAT_2:def 9;

      hence thesis by RELAT_1:def 13, A2;

    end;

    registration

      let R be non empty reflexive RelStr, x be Element of R;

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

      coherence ;

    end

    definition

      let R be Relation, X be set;

      :: ROUGHS_2:def5

      pred R is_mediate_in X means

      : Def5: for x,y be object st x in X & y in X holds [x, y] in R implies ex z be object st z in X & [x, z] in R & [z, y] in R;

    end

    definition

      let R be Relation;

      :: ROUGHS_2:def6

      attr R is mediate means R is_mediate_in ( field R);

    end

    definition

      let R be RelStr;

      :: ROUGHS_2:def7

      attr R is mediate means

      : Def7: the InternalRel of R is_mediate_in the carrier of R;

    end

    registration

      cluster reflexive -> mediate for RelStr;

      coherence

      proof

        let R be RelStr;

        assume

         A1: R is reflexive;

        set IR = the InternalRel of R, X = the carrier of R;

        for x,y be object st x in X & y in X holds [x, y] in the InternalRel of R implies ex z be object st z in X & [x, z] in IR & [z, y] in IR

        proof

          let x,y be object;

          assume

           A2: x in X & y in X;

          assume

           A3: [x, y] in IR;

           [x, x] in IR by A2, RELAT_2:def 1, A1, ORDERS_2:def 2;

          hence thesis by A2, A3;

        end;

        hence thesis by Def5;

      end;

    end

    begin

    theorem :: ROUGHS_2:5



     Th5: for R be non empty RelStr, a,b be Element of R st a in ( UAp {b}) holds [a, b] in the InternalRel of R

    proof

      let R be non empty RelStr;

      let a,b be Element of R;

      assume a in ( UAp {b});

      then

      consider x be Element of R such that

       A1: x = a & ( Class (the InternalRel of R,x)) meets {b};

      consider y be object such that

       A2: y in (( Class (the InternalRel of R,x)) /\ {b}) by A1, XBOOLE_0:def 1;

      y in ( Class (the InternalRel of R,x)) & y in {b} by XBOOLE_0:def 4, A2;

      then y = b & y in ( Class (the InternalRel of R,x)) by TARSKI:def 1;

      hence thesis by A1, RELAT_1: 169;

    end;

    definition

      let R be non empty RelStr;

      let X be Subset of R;

      :: ROUGHS_2:def8

      func Uap X -> Subset of R equals (( LAp (X ` )) ` );

      coherence ;

    end

    definition

      let R be non empty RelStr;

      let X be Subset of R;

      :: ROUGHS_2:def9

      func Lap X -> Subset of R equals (( UAp (X ` )) ` );

      coherence ;

    end

    theorem :: ROUGHS_2:6



     Th6: for R be non empty RelStr, X be Subset of R holds for x be object st x in ( LAp X) holds ( Class (the InternalRel of R,x)) c= X

    proof

      let R be non empty RelStr, X be Subset of R;

      let x be object;

      assume x in ( LAp X);

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

      hence thesis;

    end;

    theorem :: ROUGHS_2:7



     Th7: for R be non empty RelStr, X be Subset of R holds for x be set st x in ( UAp X) holds ( Class (the InternalRel of R,x)) meets X

    proof

      let R be non empty RelStr, X be Subset of R;

      let x be set;

      assume x in ( UAp X);

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

      hence thesis;

    end;

    theorem :: ROUGHS_2:8



     Th8: for R be non empty RelStr, X be Subset of R holds ( Uap X) = ( UAp X)

    proof

      let R be non empty RelStr, X be Subset of R;



       A1: ( LAp (X ` )) misses ( UAp X)

      proof

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

        then

        consider x be object such that

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

        ( Class (the InternalRel of R,x)) meets X & ( Class (the InternalRel of R,x)) c= (X ` ) by A2, Th6, Th7;

        hence thesis by XBOOLE_1: 63, XBOOLE_1: 79;

      end;

      (( UAp X) ` ) c= ( LAp (X ` ))

      proof

        let x be object;

        assume

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

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

        then ( Class (the InternalRel of R,x)) misses X by A3;

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

        hence x in ( LAp (X ` )) by A3;

      end;

      hence thesis by A1, SUBSET_1: 17, SUBSET_1: 23;

    end;

    theorem :: ROUGHS_2:9



     Th9: for R be non empty RelStr, X be Subset of R holds ( Lap X) = ( LAp X)

    proof

      let R be non empty RelStr, X be Subset of R;

      ( Uap (X ` )) = ( UAp (X ` )) by Th8;

      hence thesis;

    end;

    theorem :: ROUGHS_2:10

    for R be non empty void RelStr, X be Subset of R holds ( LAp X) = ( [#] R)

    proof

      let R be non empty void RelStr, X be Subset of R;



       A1: the InternalRel of R = {} by YELLOW_3:def 3;

      { x where x be Element of R : ( Class ( {} ,x)) c= X } = { x where x be Element of R : {} c= X }

      proof

        thus { x where x be Element of R : ( Class ( {} ,x)) c= X } c= { x where x be Element of R : {} c= X }

        proof

          let y be object;

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

          then

          consider z be Element of R such that

           A2: z = y & ( Class ( {} ,z)) c= X;

          thus thesis by A2;

        end;

        let y be object;

        assume y in { x where x be Element of R : {} c= X };

        then

        consider z be Element of R such that

         A3: z = y & {} c= X;

        ( Class ( {} ,z)) c= X;

        hence thesis by A3;

      end;

      hence thesis by Th2, A1;

    end;

    theorem :: ROUGHS_2:11

    for R be non empty void RelStr, X be Subset of R holds ( UAp X) = ( {} R)

    proof

      let R be non empty void RelStr, X be Subset of R;



       A1: the InternalRel of R = {} by YELLOW_3:def 3;

      { x where x be Element of R : ( Class ( {} ,x)) meets X } = { x where x be Element of R : {} meets X }

      proof

        thus { x where x be Element of R : ( Class ( {} ,x)) meets X } c= { x where x be Element of R : {} meets X }

        proof

          let y be object;

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

          then

          consider z be Element of R such that

           A2: z = y & ( Class ( {} ,z)) meets X;

          thus thesis by A2;

        end;

        let y be object;

        assume y in { x where x be Element of R : {} meets X };

        then

        consider z be Element of R such that

         A3: z = y & {} meets X;

        thus thesis by A3;

      end;

      hence thesis by Th3, A1;

    end;

    begin

    registration

      let R be non empty RelStr;

      reduce ( LAp ( [#] R)) to ( [#] R);

      reducibility

      proof

        { x where x be Element of R : ( Class (the InternalRel of R,x)) c= ( [#] R) } = ( [#] R)

        proof

          thus { x where x be Element of R : ( Class (the InternalRel of R,x)) c= ( [#] R) } c= ( [#] R)

          proof

            let y be object;

            assume y in { x where x be Element of R : ( Class (the InternalRel of R,x)) c= ( [#] R) };

            then ex z be Element of R st z = y & ( Class (the InternalRel of R,z)) c= ( [#] R);

            hence thesis;

          end;

          let y be object;

          assume

           A1: y in ( [#] R);

          assume not y in { x where x be Element of R : ( Class (the InternalRel of R,x)) c= ( [#] R) };

          then not y is Element of R or not ( Class (the InternalRel of R,y)) c= ( [#] R);

          hence contradiction by A1;

        end;

        hence thesis;

      end;

    end

    registration

      let R be non empty serial RelStr;

      reduce ( UAp ( [#] R)) to ( [#] R);

      reducibility

      proof

        ( [#] R) c= ( UAp ( [#] R))

        proof

          let y be object;

          assume

           A1: y in ( [#] R);

          then ( Class (the InternalRel of R,y)) meets ( [#] R) by XBOOLE_1: 28;

          hence thesis by A1;

        end;

        hence thesis;

      end;

    end

    registration

      let R be non empty serial RelStr;

      reduce ( LAp ( {} R)) to ( {} R);

      reducibility

      proof

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

        proof

          let y be object;

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

          then

          consider z be Element of R such that

           A1: z = y & ( Class (the InternalRel of R,z)) c= ( {} R);

          thus thesis by A1;

        end;

        hence thesis;

      end;

    end

    registration

      let R be non empty RelStr;

      reduce ( UAp ( {} R)) to ( {} R);

      reducibility

      proof

        thus ( UAp ( {} R)) c= ( {} R)

        proof

          let y be object;

          assume y in ( UAp ( {} R));

          then

          consider z be Element of R such that

           A1: y = z & ( Class (the InternalRel of R,z)) meets ( {} R);

          thus thesis by A1;

        end;

        thus thesis;

      end;

    end

    theorem :: ROUGHS_2:12

    for R be non empty RelStr, X,Y be Subset of R holds ( LAp (X /\ Y)) = (( LAp X) /\ ( LAp Y))

    proof

      let R be non empty RelStr;

      let X,Y be Subset of R;

      { x where x be Element of R : ( Class (the InternalRel of R,x)) c= (X /\ Y) } = ({ x where x be Element of R : ( Class (the InternalRel of R,x)) c= X } /\ { x where x be Element of R : ( Class (the InternalRel of R,x)) c= Y })

      proof

        thus { x where x be Element of R : ( Class (the InternalRel of R,x)) c= (X /\ Y) } c= ({ x where x be Element of R : ( Class (the InternalRel of R,x)) c= X } /\ { x where x be Element of R : ( Class (the InternalRel of R,x)) c= Y })

        proof

          let y be object;

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

          then

          consider z be Element of R such that

           A1: z = y & ( Class (the InternalRel of R,z)) c= (X /\ Y);

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

          then ( Class (the InternalRel of R,z)) c= X & ( Class (the InternalRel of R,z)) c= Y by A1;

          then z in { x where x be Element of R : ( Class (the InternalRel of R,x)) c= X } & z in { x where x be Element of R : ( Class (the InternalRel of R,x)) c= Y };

          hence thesis by A1, XBOOLE_0:def 4;

        end;

        let y be object;

        assume

         A2: y in ({ x where x be Element of R : ( Class (the InternalRel of R,x)) c= X } /\ { x where x be Element of R : ( Class (the InternalRel of R,x)) c= Y });

        then

         A3: y in { x where x be Element of R : ( Class (the InternalRel of R,x)) c= X } by XBOOLE_0:def 4;



         A4: y in { x where x be Element of R : ( Class (the InternalRel of R,x)) c= Y } by XBOOLE_0:def 4, A2;

        consider z be Element of R such that

         A5: z = y & ( Class (the InternalRel of R,z)) c= X by A3;

        consider w be Element of R such that

         A6: w = y & ( Class (the InternalRel of R,w)) c= Y by A4;

        (( Class (the InternalRel of R,z)) /\ ( Class (the InternalRel of R,z))) c= (X /\ Y) by A5, XBOOLE_1: 27, A6;

        hence thesis by A5;

      end;

      hence thesis;

    end;

    theorem :: ROUGHS_2:13



     Th13: for R be non empty RelStr, X,Y be Subset of R holds ( UAp (X \/ Y)) = (( UAp X) \/ ( UAp Y))

    proof

      let R be non empty RelStr;

      let X,Y be Subset of R;

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

      proof

        let y be object;

        assume y in ( UAp (X \/ Y));

        then

        consider z be Element of R such that

         A1: z = y & ( Class (the InternalRel of R,z)) meets (X \/ Y);

        ( Class (the InternalRel of R,z)) meets X or ( Class (the InternalRel of R,z)) meets Y by A1, XBOOLE_1: 70;

        then z in { x where x be Element of R : ( Class (the InternalRel of R,x)) meets X } or z in { x where x be Element of R : ( Class (the InternalRel of R,x)) meets Y };

        hence thesis by A1, XBOOLE_0:def 3;

      end;

      let y be object;

      assume y in (( UAp X) \/ ( UAp Y));

      per cases by XBOOLE_0:def 3;

        suppose y in ( UAp X);

        then

        consider z be Element of R such that

         A2: z = y & ( Class (the InternalRel of R,z)) meets X;

        ( Class (the InternalRel of R,z)) meets (X \/ Y) by A2, XBOOLE_1: 70;

        hence thesis by A2;

      end;

        suppose y in ( UAp Y);

        then

        consider z be Element of R such that

         A3: z = y & ( Class (the InternalRel of R,z)) meets Y;

        ( Class (the InternalRel of R,z)) meets (X \/ Y) by A3, XBOOLE_1: 70;

        hence thesis by A3;

      end;

    end;

    theorem :: ROUGHS_2:14

    for R be non empty RelStr, X,Y be Subset of R st X c= Y holds ( LAp X) c= ( LAp Y)

    proof

      let R be non empty RelStr;

      let X,Y be Subset of R;

      assume

       A1: X c= Y;

      let y be object;

      assume y in ( LAp X);

      then

      consider z be Element of R such that

       A2: z = y & ( Class (the InternalRel of R,z)) c= X;

      ( Class (the InternalRel of R,z)) c= Y by A1, A2;

      hence thesis by A2;

    end;

    theorem :: ROUGHS_2:15



     Th15: for R be non empty RelStr, X,Y be Subset of R st X c= Y holds ( UAp X) c= ( UAp Y)

    proof

      let R be non empty RelStr;

      let X,Y be Subset of R;

      assume

       A1: X c= Y;

      let y be object;

      assume y in ( UAp X);

      then

      consider z be Element of R such that

       A2: z = y & ( Class (the InternalRel of R,z)) meets X;

      ( Class (the InternalRel of R,z)) meets Y by A1, A2, XBOOLE_1: 63;

      hence thesis by A2;

    end;

    theorem :: ROUGHS_2:16



     Th16: for R be non empty RelStr, X be Subset of R holds ( LAp (X ` )) = (( UAp X) ` )

    proof

      let R be non empty RelStr;

      let X be Subset of R;

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

      proof

        let y be object;

        assume y in ( LAp (X ` ));

        then

        consider z be Element of R such that

         A1: z = y & ( Class (the InternalRel of R,z)) c= (X ` );

         not z in { x where x be Element of R : ( Class (the InternalRel of R,x)) meets X }

        proof

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

          then

          consider t be Element of R such that

           A2: t = z & ( Class (the InternalRel of R,t)) meets X;

          thus contradiction by A1, SUBSET_1: 23, A2;

        end;

        hence thesis by A1, XBOOLE_0:def 5;

      end;

      let y be object;

      assume

       A3: y in (( UAp X) ` );

      y in ( [#] R) & not y in ( UAp X) by XBOOLE_0:def 5, A3;

      then not (( Class (the InternalRel of R,y)) meets X);

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

      hence thesis by A3;

    end;

    theorem :: ROUGHS_2:17



     Th17: for R be non empty serial RelStr, X be Subset of R holds ( LAp X) c= ( UAp X)

    proof

      let R be non empty serial RelStr;

      let X be Subset of R;

      let y be object;

      assume y in ( LAp X);

      then

      consider z be Element of R such that

       A1: z = y & ( Class (the InternalRel of R,z)) c= X;

      ( Class (the InternalRel of R,z)) meets X by XBOOLE_1: 69, A1;

      hence thesis by A1;

    end;

    begin

    definition

      let R be non empty RelStr;

      :: ROUGHS_2:def10

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

      : Def10: for X be Subset of R holds (it . X) = ( LAp X);

      existence

      proof

        deffunc F( Element of ( bool the carrier of R)) = ( LAp $1);

        ex f be Function of ( bool the carrier of R), ( bool the carrier of R) st for X be Element of ( bool the carrier of R) holds (f . X) = F(X) from FUNCT_2:sch 4;

        then

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

         A1: for X be Subset of R holds (f . X) = F(X);

        take f;

        let r be Subset of R;

        thus thesis by A1;

      end;

      uniqueness

      proof

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

         A2: for X be Subset of R holds (f . X) = ( LAp X) and

         A3: for X be Subset of R holds (g . X) = ( LAp X);

        let Y be Subset of R;



        thus (f . Y) = ( LAp Y) by A2

        .= (g . Y) by A3;

      end;

      :: ROUGHS_2:def11

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

      : Def11: for X be Subset of R holds (it . X) = ( UAp X);

      existence

      proof

        deffunc F( Element of ( bool the carrier of R)) = ( UAp $1);

        ex f be Function of ( bool the carrier of R), ( bool the carrier of R) st for X be Element of ( bool the carrier of R) holds (f . X) = F(X) from FUNCT_2:sch 4;

        then

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

         A4: for X be Subset of R holds (f . X) = F(X);

        take f;

        let r be Subset of R;

        thus thesis by A4;

      end;

      uniqueness

      proof

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

         A5: for X be Subset of R holds (f . X) = ( UAp X) and

         A6: for X be Subset of R holds (g . X) = ( UAp X);

        let Y be Subset of R;



        thus (f . Y) = ( UAp Y) by A5

        .= (g . Y) by A6;

      end;

    end

    definition

      let f be Function;

      :: ROUGHS_2:def12

      attr f is empty-preserving means

      : Def12: (f . {} ) = {} ;

    end

    definition

      let A be set;

      let f be Function of ( bool A), ( bool A);

      :: ROUGHS_2:def13

      attr f is universe-preserving means

      : Def13: (f . A) = A;

    end

    registration

      let A be non empty set;

      cluster ( id ( bool A)) -> empty-preserving universe-preserving;

      coherence

      proof

        reconsider f = ( id ( bool A)) as Function of ( bool A), ( bool A);

         {} c= A;

        then

         A1: (f . {} ) = {} by FUNCT_1: 18;

        A in ( bool A) by ZFMISC_1:def 1;

        then (f . A) = A by FUNCT_1: 18;

        hence thesis by A1;

      end;

    end

    registration

      let A be non empty set;

      cluster empty-preserving universe-preserving for Function of ( bool A), ( bool A);

      existence

      proof

        reconsider f = ( id ( bool A)) as Function of ( bool A), ( bool A);

        f is empty-preserving universe-preserving;

        hence thesis;

      end;

    end

    definition

      let X be set;

      let f be Function of ( bool X), ( bool X);

      :: ROUGHS_2:def14

      func Flip f -> Function of ( bool X), ( bool X) means

      : Def14: for x be Subset of X holds (it . x) = ((f . (x ` )) ` );

      existence

      proof

        deffunc F( Element of ( bool X)) = ((f . ($1 ` )) ` );

        ex g be Function of ( bool X), ( bool X) st for x be Element of ( bool X) holds (g . x) = F(x) from FUNCT_2:sch 4;

        then

        consider g be Function of ( bool X), ( bool X) such that

         A1: for x be Element of ( bool X) holds (g . x) = F(x);

        take g;

        let x be Subset of X;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let f1,f2 be Function of ( bool X), ( bool X) such that

         A2: for x be Subset of X holds (f1 . x) = ((f . (x ` )) ` ) and

         A3: for x be Subset of X holds (f2 . x) = ((f . (x ` )) ` );

        let x be Subset of X;



        thus (f1 . x) = ((f . (x ` )) ` ) by A2

        .= (f2 . x) by A3;

      end;

    end

    theorem :: ROUGHS_2:18



     Th18: for X be set, f be Function of ( bool X), ( bool X) st (f . {} ) = {} holds (( Flip f) . X) = X

    proof

      let X be set, f be Function of ( bool X), ( bool X);

      assume

       A1: (f . {} ) = {} ;

      X c= X;

      then

      reconsider y = X as Subset of X;

      (( Flip f) . y) = ((f . (y ` )) ` ) by Def14

      .= (( {} X) ` ) by A1

      .= y;

      hence thesis;

    end;

    theorem :: ROUGHS_2:19



     Th19: for X be set, f be Function of ( bool X), ( bool X) st (f . X) = X holds (( Flip f) . {} ) = {}

    proof

      let X be set, f be Function of ( bool X), ( bool X);

      assume

       A1: (f . X) = X;

      set y = ( {} X);

      (( Flip f) . y) = ((f . (y ` )) ` ) by Def14

      .= ( {} X) by A1;

      hence thesis;

    end;

    theorem :: ROUGHS_2:20

    for X be set, f be Function of ( bool X), ( bool X) st f = ( id ( bool X)) holds ( Flip f) = f

    proof

      let X be set, f be Function of ( bool X), ( bool X);

      assume

       A1: f = ( id ( bool X));

      for x be Subset of X holds (( Flip f) . x) = (f . x)

      proof

        let x be Subset of X;



        thus (( Flip f) . x) = ((f . (x ` )) ` ) by Def14

        .= ((x ` ) ` ) by A1

        .= (f . x) by A1;

      end;

      hence thesis;

    end;

    theorem :: ROUGHS_2:21

    for X be set, f be Function of ( bool X), ( bool X) st for A,B be Subset of X holds (f . (A \/ B)) = ((f . A) \/ (f . B)) holds for A,B be Subset of X holds (( Flip f) . (A /\ B)) = ((( Flip f) . A) /\ (( Flip f) . B))

    proof

      let X be set, f be Function of ( bool X), ( bool X);

      assume

       A1: for A,B be Subset of X holds (f . (A \/ B)) = ((f . A) \/ (f . B));

      let A,B be Subset of X;

      set g = ( Flip f);

      (g . (A /\ B)) = ((f . ((A /\ B) ` )) ` ) by Def14

      .= ((f . ((A ` ) \/ (B ` ))) ` ) by XBOOLE_1: 54

      .= (((f . (A ` )) \/ (f . (B ` ))) ` ) by A1

      .= (((f . (A ` )) ` ) /\ ((f . (B ` )) ` )) by XBOOLE_1: 53

      .= ((g . A) /\ ((f . (B ` )) ` )) by Def14

      .= ((g . A) /\ (g . B)) by Def14;

      hence thesis;

    end;

    theorem :: ROUGHS_2:22



     Th22: for X be set, f be Function of ( bool X), ( bool X) st for A,B be Subset of X holds (f . (A /\ B)) = ((f . A) /\ (f . B)) holds for A,B be Subset of X holds (( Flip f) . (A \/ B)) = ((( Flip f) . A) \/ (( Flip f) . B))

    proof

      let X be set, f be Function of ( bool X), ( bool X);

      assume

       A1: for A,B be Subset of X holds (f . (A /\ B)) = ((f . A) /\ (f . B));

      let A,B be Subset of X;

      set g = ( Flip f);

      (g . (A \/ B)) = ((f . ((A \/ B) ` )) ` ) by Def14

      .= ((f . ((A ` ) /\ (B ` ))) ` ) by XBOOLE_1: 53

      .= (((f . (A ` )) /\ (f . (B ` ))) ` ) by A1

      .= (((f . (A ` )) ` ) \/ ((f . (B ` )) ` )) by XBOOLE_1: 54

      .= ((g . A) \/ ((f . (B ` )) ` )) by Def14

      .= ((g . A) \/ (g . B)) by Def14;

      hence thesis;

    end;

    theorem :: ROUGHS_2:23



     Th23: for X be set, f be Function of ( bool X), ( bool X) holds ( Flip ( Flip f)) = f

    proof

      let X be set, f be Function of ( bool X), ( bool X);

      set g = ( Flip ( Flip f));

      for x be Subset of X holds (g . x) = (f . x)

      proof

        let x be Subset of X;

        (g . x) = ((( Flip f) . (x ` )) ` ) by Def14

        .= (((f . ((x ` ) ` )) ` ) ` ) by Def14

        .= (f . x);

        hence thesis;

      end;

      hence thesis;

    end;

    registration

      let A be non empty set;

      let f be universe-preserving Function of ( bool A), ( bool A);

      cluster ( Flip f) -> empty-preserving;

      coherence

      proof

        (f . A) = A by Def13;

        hence thesis by Th19;

      end;

    end

    registration

      let A be non empty set;

      let f be empty-preserving Function of ( bool A), ( bool A);

      cluster ( Flip f) -> universe-preserving;

      coherence

      proof

        (f . {} ) = {} by Def12;

        hence thesis by Th18;

      end;

    end

    theorem :: ROUGHS_2:24



     Th24: for A be non empty set, L,U be Function of ( bool A), ( bool A) st U = ( Flip L) & for X be Subset of A holds (L . (L . X)) c= (L . X) holds for X be Subset of A holds (U . X) c= (U . (U . X))

    proof

      let A be non empty set;

      let L,U be Function of ( bool A), ( bool A);

      assume that

       A1: U = ( Flip L) and

       A2: for X be Subset of A holds (L . (L . X)) c= (L . X);

      let X be Subset of A;



       A3: (U . X) = ((L . (X ` )) ` ) by Def14, A1;

      (U . (U . X)) = (U . ((L . (X ` )) ` )) by Def14, A1

      .= ((L . (((L . (X ` )) ` ) ` )) ` ) by Def14, A1

      .= ((L . (L . (X ` ))) ` );

      hence thesis by A3, A2, SUBSET_1: 12;

    end;

    begin

    definition

      let T be TopSpace;

      :: ROUGHS_2:def15

      func ClMap T -> Function of ( bool the carrier of T), ( bool the carrier of T) means

      : Def15: for X be Subset of T holds (it . X) = ( Cl X);

      existence

      proof

        deffunc F( Subset of T) = ( Cl $1);

        set X = the carrier of T;

        ex g be Function of ( bool X), ( bool X) st for x be Element of ( bool X) holds (g . x) = F(x) from FUNCT_2:sch 4;

        then

        consider g be Function of ( bool X), ( bool X) such that

         A1: for x be Element of ( bool X) holds (g . x) = F(x);

        take g;

        let x be Subset of X;

        thus thesis by A1;

      end;

      uniqueness

      proof

        set X = the carrier of T;

        let f1,f2 be Function of ( bool X), ( bool X) such that

         A2: for x be Subset of X holds (f1 . x) = ( Cl x) and

         A3: for x be Subset of X holds (f2 . x) = ( Cl x);

        let x be Subset of X;



        thus (f1 . x) = ( Cl x) by A2

        .= (f2 . x) by A3;

      end;

      :: ROUGHS_2:def16

      func IntMap T -> Function of ( bool the carrier of T), ( bool the carrier of T) means

      : Def16: for X be Subset of T holds (it . X) = ( Int X);

      existence

      proof

        deffunc F( Subset of T) = ( Int $1);

        set X = the carrier of T;

        ex g be Function of ( bool X), ( bool X) st for x be Element of ( bool X) holds (g . x) = F(x) from FUNCT_2:sch 4;

        then

        consider g be Function of ( bool X), ( bool X) such that

         A4: for x be Element of ( bool X) holds (g . x) = F(x);

        take g;

        let x be Subset of X;

        thus thesis by A4;

      end;

      uniqueness

      proof

        set X = the carrier of T;

        let f1,f2 be Function of ( bool X), ( bool X) such that

         A5: for x be Subset of X holds (f1 . x) = ( Int x) and

         A6: for x be Subset of X holds (f2 . x) = ( Int x);

        let x be Subset of X;



        thus (f1 . x) = ( Int x) by A5

        .= (f2 . x) by A6;

      end;

    end

    definition

      let T be TopSpace;

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

      :: ROUGHS_2:def17

      attr f is closed-valued means for X be Subset of T holds (f . X) is closed;

      :: ROUGHS_2:def18

      attr f is open-valued means for X be Subset of T holds (f . X) is open;

    end

    registration

      let T be TopSpace;

      cluster ( ClMap T) -> closed-valued;

      coherence

      proof

        let X be Subset of T;

        (( ClMap T) . X) = ( Cl X) by Def15;

        hence thesis;

      end;

      cluster ( IntMap T) -> open-valued;

      coherence

      proof

        let X be Subset of T;

        (( IntMap T) . X) = ( Int X) by Def16;

        hence thesis;

      end;

    end

    registration

      let T be TopSpace;

      cluster closed-valued for Function of ( bool the carrier of T), ( bool the carrier of T);

      existence

      proof

        take ( ClMap T);

        thus thesis;

      end;

      cluster open-valued for Function of ( bool the carrier of T), ( bool the carrier of T);

      existence

      proof

        take ( IntMap T);

        thus thesis;

      end;

    end

    theorem :: ROUGHS_2:25



     Th25: for T be TopSpace holds ( Flip ( ClMap T)) = ( IntMap T)

    proof

      let T be TopSpace;

      set f = ( Flip ( ClMap T)), g = ( IntMap T);

      for x be Subset of T holds (f . x) = (g . x)

      proof

        let x be Subset of T;



         A1: (( Int x) ` ) = ( Cl (x ` )) by TDLAT_3: 2;

        (f . x) = ((( ClMap T) . (x ` )) ` ) by Def14

        .= (( Cl (x ` )) ` ) by Def15

        .= (g . x) by Def16, A1;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: ROUGHS_2:26

    for T be TopSpace holds ( Flip ( IntMap T)) = ( ClMap T)

    proof

      let T be TopSpace;

      ( Flip ( Flip ( ClMap T))) = ( Flip ( IntMap T)) by Th25;

      hence thesis by Th23;

    end;

    registration

      let T be non empty TopSpace;

      cluster ( ClMap T) -> empty-preserving universe-preserving;

      coherence

      proof

        set f = ( ClMap T);



         A1: (f . ( {} T)) = ( Cl ( {} T)) by Def15

        .= ( {} T) by PRE_TOPC: 22;

        (f . ( [#] T)) = ( Cl ( [#] T)) by Def15

        .= ( [#] T) by PRE_TOPC: 22;

        hence thesis by A1;

      end;

      cluster ( IntMap T) -> empty-preserving universe-preserving;

      coherence

      proof

        set f = ( IntMap T);



         A2: (f . ( {} T)) = ( Int ( {} T)) by Def16

        .= ( {} T);

        (f . ( [#] T)) = ( Int ( [#] T)) by Def16

        .= ( [#] T) by TOPS_1: 15;

        hence thesis by A2;

      end;

    end

    begin

    theorem :: ROUGHS_2:27



     Th27: for R be non empty RelStr holds ( Flip ( UAp R)) = ( LAp R)

    proof

      let R be non empty RelStr;

      set f = ( Flip ( UAp R)), g = ( LAp R);

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

      proof

        let x be Subset of R;

        (f . x) = ((( UAp R) . (x ` )) ` ) by Def14

        .= ( Lap x) by Def11

        .= ( LAp x) by Th9

        .= (g . x) by Def10;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: ROUGHS_2:28



     Th28: for R be non empty RelStr holds ( Flip ( LAp R)) = ( UAp R)

    proof

      let R be non empty RelStr;

      ( Flip ( UAp R)) = ( LAp R) by Th27;

      hence thesis by Th23;

    end;

    theorem :: ROUGHS_2:29



     Th29: for A be non empty finite set, U be Function of ( bool A), ( bool A) st (U . {} ) = {} & (for X,Y be Subset of A holds (U . (X \/ Y)) = ((U . X) \/ (U . Y))) holds ex R be non empty finite RelStr st the carrier of R = A & U = ( UAp R)

    proof

      let A be non empty finite set;

      let L be Function of ( bool A), ( bool A);

      assume that

       A1: (L . {} ) = {} and

       A2: for X,Y be Subset of A holds (L . (X \/ Y)) = ((L . X) \/ (L . Y));

      defpred P[ set, set] means $1 in (L . {$2});

      consider R be Relation of A such that

       A3: for x,y be Element of A holds [x, y] in R iff P[x, y] from RELSET_1:sch 2;

      reconsider RR = RelStr (# A, R #) as non empty finite RelStr;

      take RR;



       A4: for y be Element of RR, Y be Subset of RR st Y = {y} holds ( UAp Y) = (L . Y)

      proof

        let y be Element of RR, Y be Subset of RR;

        assume

         A5: Y = {y};

        thus ( UAp Y) c= (L . Y)

        proof

          let x be object;

          assume x in ( UAp Y);

          then

          consider a be Element of RR such that

           A6: a = x & ( Class (the InternalRel of RR,a)) meets Y;

          consider z be object such that

           A7: z in ( Class (the InternalRel of RR,a)) & z in Y by A6, XBOOLE_0: 3;

          z = y by A7, TARSKI:def 1, A5;

          then [x, y] in R by A6, A7, EQREL_1: 18;

          hence thesis by A5, A3, A6;

        end;

        let x be object;

        assume

         A8: x in (L . Y);



         A9: y in Y by TARSKI:def 1, A5;



         A10: (L . Y) in ( bool A) by FUNCT_2: 5;

        then [x, y] in R by A3, A8, A5;

        then y in ( Class (R,x)) by EQREL_1: 18;

        then ( Class (the InternalRel of RR,x)) meets Y by A9, XBOOLE_0: 3;

        hence thesis by A10, A8;

      end;

      ( dom L) = ( bool A) by FUNCT_2:def 1;

      then

       A11: ( dom ( UAp RR)) = ( dom L) by FUNCT_2:def 1;

      for x be object st x in ( dom ( UAp RR)) holds (( UAp RR) . x) = (L . x)

      proof

        let x be object;

        assume

         A12: x in ( dom ( UAp RR));

        per cases ;

          suppose x <> {} ;

          then

          reconsider X = x as finite non empty Subset of RR by A12;

          defpred P[ finite non empty Subset of RR] means (( UAp RR) . $1) = (L . $1);



           A13: for x be Element of RR st x in X holds P[ {x}]

          proof

            let x be Element of RR;

            assume x in X;

            set I = {x};

            (( UAp RR) . I) = ( UAp I) by Def11

            .= (L . I) by A4;

            hence thesis;

          end;



           A14: for x be Element of RR, B be non empty finite Subset of RR st x in X & B c= X & not x in B & P[B] holds P[(B \/ {x})]

          proof

            let x be Element of RR, B be non empty finite Subset of RR;

            assume x in X & B c= X & not x in B & P[B];

            then

             A15: ( UAp B) = (L . B) by Def11;

            set I = {x};

            (( UAp RR) . (B \/ {x})) = ( UAp (B \/ I)) by Def11

            .= (( UAp B) \/ ( UAp I)) by Th13

            .= ((L . B) \/ (L . I)) by A4, A15

            .= (L . (B \/ I)) by A2;

            hence thesis;

          end;

           P[X] from CHAIN_1:sch 2( A13, A14);

          hence thesis;

        end;

          suppose

           A16: x = {} ;

          ( UAp ( {} RR)) = (L . {} ) by A1;

          hence thesis by Def11, A16;

        end;

      end;

      hence thesis by A11, FUNCT_1: 2;

    end;

    theorem :: ROUGHS_2:30



     Th30: for A be non empty finite set, L be Function of ( bool A), ( bool A) st (L . A) = A & (for X,Y be Subset of A holds (L . (X /\ Y)) = ((L . X) /\ (L . Y))) holds ex R be non empty finite RelStr st the carrier of R = A & L = ( LAp R)

    proof

      let A be non empty finite set, L be Function of ( bool A), ( bool A);

      assume that

       A1: (L . A) = A and

       A2: for X,Y be Subset of A holds (L . (X /\ Y)) = ((L . X) /\ (L . Y));

      set U = ( Flip L);



       A3: (U . {} ) = {} by Th19, A1;



       A4: for X,Y be Subset of A holds (U . (X \/ Y)) = ((U . X) \/ (U . Y)) by Th22, A2;

      consider R be non empty finite RelStr such that

       A5: the carrier of R = A & U = ( UAp R) by Th29, A3, A4;

      take R;

      L = ( Flip ( UAp R)) by Th23, A5;

      hence thesis by A5, Th27;

    end;

    theorem :: ROUGHS_2:31



     Th31: for A be non empty finite set, L be Function of ( bool A), ( bool A) st (L . A) = A & (L . {} ) = {} & (for X,Y be Subset of A holds (L . (X /\ Y)) = ((L . X) /\ (L . Y))) holds ex R be non empty serial RelStr st the carrier of R = A & L = ( LAp R)

    proof

      let A be non empty finite set;

      let L be Function of ( bool A), ( bool A);

      assume that

       A1: (L . A) = A and

       A2: (L . {} ) = {} and

       A3: for X,Y be Subset of A holds (L . (X /\ Y)) = ((L . X) /\ (L . Y));

      consider R be non empty finite RelStr such that

       A4: the carrier of R = A & L = ( LAp R) by Th30, A3, A1;

      for x be object st x in the carrier of R holds ex y be object st y in the carrier of R & [x, y] in the InternalRel of R

      proof

        let x be object;

        assume

         A5: x in the carrier of R;



         A6: (( LAp R) . {} ) = ( LAp ( {} R)) by Def10

        .= { y where y be Element of R : ( Class (the InternalRel of R,y)) c= {} };

        for y be Element of R holds ( Class (the InternalRel of R,y)) <> {}

        proof

          let y be Element of R;

          assume ( Class (the InternalRel of R,y)) = {} ;

          then y in { y where y be Element of R : ( Class (the InternalRel of R,y)) c= {} };

          hence contradiction by A6, A4, A2;

        end;

        then ( Class (the InternalRel of R,x)) <> {} by A5;

        then

        consider t be object such that

         A7: t in ( Im (the InternalRel of R,x)) by XBOOLE_0:def 1;



         A8: [x, t] in the InternalRel of R by A7, RELAT_1: 169;

        then t in ( rng the InternalRel of R) by A5, RELSET_1: 25;

        hence thesis by A8;

      end;

      then R is serial by Def1;

      hence thesis by A4;

    end;

    theorem :: ROUGHS_2:32



     Th32: for A be non empty finite set, U be Function of ( bool A), ( bool A) st (U . A) = A & (U . {} ) = {} & (for X,Y be Subset of A holds (U . (X \/ Y)) = ((U . X) \/ (U . Y))) holds ex R be non empty finite serial RelStr st the carrier of R = A & U = ( UAp R)

    proof

      let A be non empty finite set;

      let U be Function of ( bool A), ( bool A);

      assume that

       A1: (U . A) = A and

       A2: (U . {} ) = {} and

       A3: for X,Y be Subset of A holds (U . (X \/ Y)) = ((U . X) \/ (U . Y));

      consider R be non empty finite RelStr such that

       A4: the carrier of R = A & U = ( UAp R) by Th29, A2, A3;

      for x be object st x in the carrier of R holds ex y be object st y in the carrier of R & [x, y] in the InternalRel of R

      proof

        let x be object;

        assume

         A5: x in the carrier of R;

        reconsider Z = ( [#] A) as Subset of R by A4;

        ( UAp Z) = Z by A4, A1, Def11;

        then

        consider t be Element of R such that

         A6: t = x & ( Class (the InternalRel of R,t)) meets ( [#] A) by A5, A4;

        ( Class (the InternalRel of R,t)) <> {} by A6;

        then

        consider s be object such that

         A7: s in ( Class (the InternalRel of R,t)) by XBOOLE_0:def 1;

         [t, s] in the InternalRel of R by A7, RELAT_1: 169;

        then [x, s] in the InternalRel of R & s in ( rng the InternalRel of R) by XTUPLE_0:def 13, A6;

        hence thesis;

      end;

      then R is serial by Def1;

      hence thesis by A4;

    end;

    theorem :: ROUGHS_2:33



     Th33: for A be non empty finite set, L be Function of ( bool A), ( bool A) st (L . A) = A & (for X be Subset of A holds (L . X) c= ((L . (X ` )) ` )) & (for X,Y be Subset of A holds (L . (X /\ Y)) = ((L . X) /\ (L . Y))) holds ex R be non empty finite serial RelStr st the carrier of R = A & L = ( LAp R)

    proof

      let A be non empty finite set;

      let L be Function of ( bool A), ( bool A);

      assume that

       A1: (L . A) = A and

       A2: for X be Subset of A holds (L . X) c= ((L . (X ` )) ` ) and

       A3: for X,Y be Subset of A holds (L . (X /\ Y)) = ((L . X) /\ (L . Y));

      consider R be non empty finite RelStr such that

       A4: the carrier of R = A & L = ( LAp R) by Th30, A1, A3;

      set XX = ( {} A);



       A5: (L . (XX ` )) = A by A1;

      then

       A6: (L . {} ) c= (( [#] A) ` ) by A2;

      for x be object st x in the carrier of R holds ex y be object st y in the carrier of R & [x, y] in the InternalRel of R

      proof

        let x be object;

        assume

         A7: x in the carrier of R;

        reconsider Z = ( [#] A) as Subset of R by A4;



         A8: (( LAp R) . {} ) = ( LAp ( {} R)) by Def10

        .= { y where y be Element of R : ( Class (the InternalRel of R,y)) c= {} };

        for y be Element of R holds ( Class (the InternalRel of R,y)) <> {}

        proof

          let y be Element of R;

          assume ( Class (the InternalRel of R,y)) = {} ;

          then y in { z where z be Element of R : ( Class (the InternalRel of R,z)) c= {} };

          hence contradiction by A8, A4, A6, A5;

        end;

        then ( Class (the InternalRel of R,x)) <> {} by A7;

        then

        consider t be object such that

         A9: t in ( Im (the InternalRel of R,x)) by XBOOLE_0:def 1;



         A10: [x, t] in the InternalRel of R by A9, RELAT_1: 169;

        then t in ( rng the InternalRel of R) by RELSET_1: 25, A7;

        hence thesis by A10;

      end;

      then R is serial by Def1;

      hence thesis by A4;

    end;

    theorem :: ROUGHS_2:34



     Th34: for A be non empty finite set, U be Function of ( bool A), ( bool A) st (U . {} ) = {} & (for X be Subset of A holds ((U . (X ` )) ` ) c= (U . X)) & (for X,Y be Subset of A holds (U . (X \/ Y)) = ((U . X) \/ (U . Y))) holds ex R be non empty serial RelStr st the carrier of R = A & U = ( UAp R)

    proof

      let A be non empty finite set;

      let U be Function of ( bool A), ( bool A);

      assume that

       A1: (U . {} ) = {} and

       A2: for X be Subset of A holds ((U . (X ` )) ` ) c= (U . X) and

       A3: for X,Y be Subset of A holds (U . (X \/ Y)) = ((U . X) \/ (U . Y));

      consider R be non empty finite RelStr such that

       A4: the carrier of R = A & U = ( UAp R) by Th29, A1, A3;

      for x be object st x in the carrier of R holds ex y be object st y in the carrier of R & [x, y] in the InternalRel of R

      proof

        let x be object;

        assume

         A5: x in the carrier of R;

        reconsider Z = ( [#] A) as Subset of R by A4;

        set XX = ( [#] A);

        ((U . (XX ` )) ` ) c= (U . XX) by A2;

        then (( {} A) ` ) c= (U . XX) by A1;

        then

         A6: (( Flip ( UAp R)) . {} ) = {} by Th19, A4, XBOOLE_0:def 10;



         A7: (( LAp R) . {} ) = ( LAp ( {} R)) by Def10

        .= { y where y be Element of R : ( Class (the InternalRel of R,y)) c= {} };

        for y be Element of R holds ( Class (the InternalRel of R,y)) <> {}

        proof

          let y be Element of R;

          assume ( Class (the InternalRel of R,y)) = {} ;

          then y in { z where z be Element of R : ( Class (the InternalRel of R,z)) c= {} };

          hence contradiction by A7, A6, Th27;

        end;

        then ( Class (the InternalRel of R,x)) <> {} by A5;

        then

        consider t be object such that

         A8: t in ( Im (the InternalRel of R,x)) by XBOOLE_0:def 1;



         A9: [x, t] in the InternalRel of R by A8, RELAT_1: 169;

        then t in ( rng the InternalRel of R) by RELSET_1: 25, A5;

        hence thesis by A9;

      end;

      then R is serial by Def1;

      hence thesis by A4;

    end;

    theorem :: ROUGHS_2:35

    for R be non empty reflexive RelStr, X be Subset of R holds ( LAp X) c= X

    proof

      let R be non empty reflexive RelStr;

      let X be Subset of R;

      let y be object;

      assume y in ( LAp X);

      then

      consider z be Element of R such that

       A1: z = y & ( Class (the InternalRel of R,z)) c= X;



       A2: z in ( field the InternalRel of R) by Th1;



       A3: z in {z} by TARSKI:def 1;

       [z, z] in the InternalRel of R by A2, RELAT_2:def 1, RELAT_2:def 9;

      then z in (the InternalRel of R .: {z}) by RELAT_1:def 13, A3;

      hence thesis by A1;

    end;

    theorem :: ROUGHS_2:36

    for R be non empty reflexive RelStr, X be Subset of R holds X c= ( UAp X)

    proof

      let R be non empty reflexive RelStr, X be Subset of R;

      let y be object;

      assume

       A1: y in X;

      then y in ( Class (the InternalRel of R,y)) by Th4;

      then ( Class (the InternalRel of R,y)) meets X by A1, XBOOLE_0:def 4;

      hence thesis by A1;

    end;

    theorem :: ROUGHS_2:37



     Th37: for A be non empty finite set, U be Function of ( bool A), ( bool A) st (U . {} ) = {} & (for X be Subset of A holds X c= (U . X)) & (for X,Y be Subset of A holds (U . (X \/ Y)) = ((U . X) \/ (U . Y))) holds ex R be non empty finite reflexive RelStr st the carrier of R = A & U = ( UAp R)

    proof

      let A be non empty finite set;

      let U be Function of ( bool A), ( bool A);

      assume that

       A1: (U . {} ) = {} and

       A2: for X be Subset of A holds X c= (U . X) and

       A3: for X,Y be Subset of A holds (U . (X \/ Y)) = ((U . X) \/ (U . Y));

      (U . ( [#] A)) c= ( [#] A) & ( [#] A) c= (U . ( [#] A)) by A2;

      then (U . A) = A;

      then

      consider R be non empty finite serial RelStr such that

       A4: the carrier of R = A & U = ( UAp R) by Th32, A1, A3;

      for x be object st x in the carrier of R holds [x, x] in the InternalRel of R

      proof

        let x be object;

        assume

         A5: x in the carrier of R;

        then

         A6: {x} is Subset of R by ZFMISC_1: 31;

        reconsider Z = {x} as Subset of R by A5, ZFMISC_1: 31;



         A7: {x} c= (U . {x}) by A4, A6, A2;

        x in {x} by TARSKI:def 1;

        then

         A8: x in (U . {x}) by A7;

        (U . {x}) = ( UAp Z) by Def11, A4

        .= { y where y be Element of R : ( Class (the InternalRel of R,y)) meets Z };

        then

        consider t be Element of R such that

         A9: t = x & ( Class (the InternalRel of R,t)) meets Z by A8;

        x in ( Class (the InternalRel of R,t))

        proof

          assume

           A10: not x in ( Class (the InternalRel of R,t));

          consider y be object such that

           A11: y in (( Class (the InternalRel of R,t)) /\ {x}) by A9, XBOOLE_0:def 1;

          y in ( Class (the InternalRel of R,t)) & y in {x} by XBOOLE_0:def 4, A11;

          hence contradiction by A10, TARSKI:def 1;

        end;

        hence thesis by A9, RELAT_1: 169;

      end;

      then R is reflexive by ORDERS_2:def 2, RELAT_2:def 1;

      hence thesis by A4;

    end;

    theorem :: ROUGHS_2:38

    for A be non empty finite set, L be Function of ( bool A), ( bool A) st (L . A) = A & (for X be Subset of A holds (L . X) c= X) & (for X,Y be Subset of A holds (L . (X /\ Y)) = ((L . X) /\ (L . Y))) holds ex R be non empty finite reflexive RelStr st the carrier of R = A & L = ( LAp R)

    proof

      let A be non empty finite set;

      let L be Function of ( bool A), ( bool A);

      assume that

       A1: (L . A) = A and

       A2: for X be Subset of A holds (L . X) c= X and

       A3: for X,Y be Subset of A holds (L . (X /\ Y)) = ((L . X) /\ (L . Y));

      set U = ( Flip L);



       A4: (U . {} ) = {} by A1, Th19;



       A5: for X be Subset of A holds X c= (U . X)

      proof

        let X be Subset of A;

        ((X ` ) ` ) c= ((L . (X ` )) ` ) by A2, SUBSET_1: 12;

        hence thesis by Def14;

      end;

      for X,Y be Subset of A holds (U . (X \/ Y)) = ((U . X) \/ (U . Y)) by A3, Th22;

      then

      consider R be non empty finite reflexive RelStr such that

       A6: the carrier of R = A & U = ( UAp R) by Th37, A4, A5;

      L = ( Flip ( UAp R)) by Th23, A6;

      then L = ( LAp R) by Th27;

      hence thesis by A6;

    end;

    theorem :: ROUGHS_2:39



     Th39: for R be non empty mediate RelStr, X be Subset of R holds ( UAp X) c= ( UAp ( UAp X))

    proof

      let R be non empty mediate RelStr;

      let X be Subset of R;

      let y be object;

      assume y in ( UAp X);

      then

      consider t be Element of R such that

       A1: t = y & ( Class (the InternalRel of R,t)) meets X;

      ex w be object st w in (( Class (the InternalRel of R,t)) /\ X) by A1, XBOOLE_0:def 1;

      then

      consider w be Element of the carrier of R such that

       A2: w in (( Class (the InternalRel of R,t)) /\ X);



       A3: w in ( Class (the InternalRel of R,t)) & w in X by XBOOLE_0:def 4, A2;

      then [t, w] in the InternalRel of R by RELAT_1: 169;

      then

      consider z be object such that

       A4: z in the carrier of R & [t, z] in the InternalRel of R & [z, w] in the InternalRel of R by Def5, Def7;

      reconsider z as Element of R by A4;



       A5: z in ( Class (the InternalRel of R,t)) & w in ( Class (the InternalRel of R,z)) by A4, RELAT_1: 169;

      then ( Class (the InternalRel of R,z)) meets X by A3, XBOOLE_0:def 4;

      then

       A6: z in { x where x be Element of R : ( Class (the InternalRel of R,x)) meets X };



       A7: ( UAp {z}) c= ( UAp ( UAp X)) by Th15, A6, ZFMISC_1: 31;

      z in {z} by TARSKI:def 1;

      then ( Class (the InternalRel of R,t)) meets {z} by A5, XBOOLE_0:def 4;

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

      hence thesis by A1, A7;

    end;

    theorem :: ROUGHS_2:40

    for R be non empty mediate RelStr, X be Subset of R holds ( LAp ( LAp X)) c= ( LAp X)

    proof

      let R be non empty mediate RelStr;

      let X be Subset of R;



       A1: ( LAp ( LAp X)) = ( LAp ((( LAp X) ` ) ` ))

      .= (( UAp (( LAp ((X ` ) ` )) ` )) ` ) by Th16

      .= (( UAp ((( UAp (X ` )) ` ) ` )) ` ) by Th16

      .= (( UAp ( UAp (X ` ))) ` );

      (( UAp (X ` )) ` ) = ( LAp ((X ` ) ` )) by Th16

      .= ( LAp X);

      hence thesis by A1, SUBSET_1: 12, Th39;

    end;

    theorem :: ROUGHS_2:41



     Th41: for A be non empty finite set, U be Function of ( bool A), ( bool A) st (U . {} ) = {} & (for X be Subset of A holds (U . X) c= (U . (U . X))) & (for X,Y be Subset of A holds (U . (X \/ Y)) = ((U . X) \/ (U . Y))) holds ex R be non empty mediate finite RelStr st the carrier of R = A & U = ( UAp R)

    proof

      let A be non empty finite set;

      let U be Function of ( bool A), ( bool A);

      assume that

       A1: (U . {} ) = {} and

       A2: for X be Subset of A holds (U . X) c= (U . (U . X)) and

       A3: for X,Y be Subset of A holds (U . (X \/ Y)) = ((U . X) \/ (U . Y));

      consider R be non empty finite RelStr such that

       A4: the carrier of R = A & U = ( UAp R) by Th29, A1, A3;

      for x,y be object st x in the carrier of R & y in the carrier of R holds [x, y] in the InternalRel of R implies ex z be object st z in the carrier of R & [x, z] in the InternalRel of R & [z, y] in the InternalRel of R

      proof

        let x,y be object;

        assume

         A5: x in the carrier of R & y in the carrier of R;

        then

        reconsider Y = {y} as Subset of R by ZFMISC_1: 31;

        assume

         A6: [x, y] in the InternalRel of R;

        reconsider x as Element of R by A5;

        y in ( Class (the InternalRel of R,x)) & y in {y} by A6, TARSKI:def 1, RELAT_1: 169;

        then ( Class (the InternalRel of R,x)) meets {y} by XBOOLE_0:def 4;

        then

         A7: x in ( UAp Y);

        x in ( UAp ( UAp Y))

        proof



           A8: x in (U . Y) by A4, Def11, A7;

          x in (U . (U . Y)) by A2, TARSKI:def 3, A4, A8;

          then x in (U . ( UAp Y)) by Def11, A4;

          hence thesis by Def11, A4;

        end;

        then

        consider t be Element of R such that

         A9: t = x & ( Class (the InternalRel of R,t)) meets ( UAp Y);

        consider z be object such that

         A10: z in (( Class (the InternalRel of R,t)) /\ ( UAp Y)) by A9, XBOOLE_0:def 1;

        reconsider Z = {z} as Subset of R by ZFMISC_1: 31, A10;



         A11: z in {z} & z in ( Class (the InternalRel of R,t)) & z in ( UAp Y) by A10, XBOOLE_0:def 4, TARSKI:def 1;

        then ( Class (the InternalRel of R,t)) meets {z} by XBOOLE_0:def 4;

        then t in ( UAp Z);

        then [t, z] in the InternalRel of R & [z, y] in the InternalRel of R by A11, A5, Th5;

        hence thesis by A9, A10;

      end;

      then R is mediate by Def5;

      hence thesis by A4;

    end;

    theorem :: ROUGHS_2:42

    for A be non empty finite set, L be Function of ( bool A), ( bool A) st (L . A) = A & (for X be Subset of A holds (L . (L . X)) c= (L . X)) & (for X,Y be Subset of A holds (L . (X /\ Y)) = ((L . X) /\ (L . Y))) holds ex R be non empty mediate finite RelStr st the carrier of R = A & L = ( LAp R)

    proof

      let A be non empty finite set;

      let L be Function of ( bool A), ( bool A);

      assume that

       A1: (L . A) = A and

       A2: for X be Subset of A holds (L . (L . X)) c= (L . X) and

       A3: for X,Y be Subset of A holds (L . (X /\ Y)) = ((L . X) /\ (L . Y));

      set U = ( Flip L);



       A4: (U . {} ) = {} by A1, Th19;



       A5: for X be Subset of A holds (U . X) c= (U . (U . X)) by Th24, A2;

      for X,Y be Subset of A holds (U . (X \/ Y)) = ((U . X) \/ (U . Y)) by Th22, A3;

      then

      consider R be non empty mediate finite RelStr such that

       A6: the carrier of R = A & U = ( UAp R) by Th41, A4, A5;

      take R;

      L = ( Flip ( UAp R)) by Th23, A6;

      hence thesis by A6, Th27;

    end;

    theorem :: ROUGHS_2:43

    for A be non empty finite set, L be Function of ( bool A), ( bool A) st (L . A) = A & (for X,Y be Subset of A holds (L . (X /\ Y)) = ((L . X) /\ (L . Y))) holds (for X be Subset of A holds (L . X) c= ((L . (X ` )) ` )) iff (L . {} ) = {}

    proof

      let A be non empty finite set;

      let L be Function of ( bool A), ( bool A);

      assume that

       A1: (L . A) = A and

       A2: for X,Y be Subset of A holds (L . (X /\ Y)) = ((L . X) /\ (L . Y));

      thus (for X be Subset of A holds (L . X) c= ((L . (X ` )) ` )) implies (L . {} ) = {}

      proof

        assume for X be Subset of A holds (L . X) c= ((L . (X ` )) ` );

        then

        consider R be non empty serial finite RelStr such that

         A3: the carrier of R = A & L = ( LAp R) by A1, Th33, A2;

        (L . {} ) = ( LAp ( {} R)) by Def10, A3;

        hence thesis;

      end;

      assume (L . {} ) = {} ;

      then

      consider R be non empty serial RelStr such that

       A4: the carrier of R = A & L = ( LAp R) by A1, Th31, A2;

      let X be Subset of A;

      reconsider Xa = X as Subset of R by A4;

      set U = ( Flip L);



       A5: U = ( UAp R) by A4, Th28;

      ( LAp Xa) c= ( UAp Xa) by Th17;

      then ( LAp Xa) c= (( UAp R) . X) by Def11;

      then (( LAp R) . X) c= (( UAp R) . X) by Def10;

      hence thesis by Def14, A4, A5;

    end;

    theorem :: ROUGHS_2:44

    for A be non empty finite set, U be Function of ( bool A), ( bool A) st (U . {} ) = {} & (for X,Y be Subset of A holds (U . (X \/ Y)) = ((U . X) \/ (U . Y))) holds (for X be Subset of A holds ((U . (X ` )) ` ) c= (U . X)) iff (U . A) = A

    proof

      let A be non empty finite set;

      let U be Function of ( bool A), ( bool A);

      assume that

       A1: (U . {} ) = {} and

       A2: for X,Y be Subset of A holds (U . (X \/ Y)) = ((U . X) \/ (U . Y));

      thus (for X be Subset of A holds ((U . (X ` )) ` ) c= (U . X)) implies (U . A) = A

      proof

        assume for X be Subset of A holds ((U . (X ` )) ` ) c= (U . X);

        then

        consider R be non empty serial RelStr such that

         A3: the carrier of R = A & U = ( UAp R) by Th34, A1, A2;

        (( UAp R) . ( [#] R)) = ( UAp ( [#] R)) by Def11;

        hence thesis by A3;

      end;

      assume (U . A) = A;

      then

      consider R be non empty finite serial RelStr such that

       A4: the carrier of R = A & U = ( UAp R) by A1, Th32, A2;

      let X be Subset of A;

      reconsider Xa = X as Subset of R by A4;

      set L = ( Flip U);



       A5: L = ( LAp R) by A4, Th27;

      ( LAp Xa) c= ( UAp Xa) by Th17;

      then ( LAp Xa) c= (( UAp R) . X) by Def11;

      then (( LAp R) . X) c= (( UAp R) . X) by Def10;

      hence thesis by Def14, A4, A5;

    end;