roughs_3.miz



    begin

    reserve X,a,b,c,x,y,z,t for set;

    reserve R for Relation;

    registration

      let X be non empty set;

      cluster ( bool X) -> d.union-closed;

      coherence ;

    end

    scheme :: ROUGHS_3:sch1

    FinSubIndA1 { X() -> non empty finite set , P[ Subset of X()] } :

for B be Subset of X() holds P[B]

      provided

       A1: P[( {} X())]

       and

       A2: for B9 be Subset of X(), b be Element of X() holds P[B9] & not b in B9 implies P[(B9 \/ {b})];

      defpred X[ set] means ex B9 be Subset of X() st B9 = $1 & P[B9];

      let B be Subset of X();

      

       A3: for x,A be set st x in B & A c= B & X[A] holds X[(A \/ {x})]

      proof

        let x,A be set such that

         A4: x in B and

         A5: A c= B and

         A6: ex B9 be Subset of X() st B9 = A & P[B9];

        reconsider x9 = x as Element of X() by A4;

        reconsider A9 = A as Subset of X() by A5, XBOOLE_1: 1;

        reconsider A99 = (A9 \/ {x9}) as Subset of X();

        take A99;

        thus A99 = (A \/ {x});

        thus P[A99] by A2, A6, ZFMISC_1: 40;

      end;

      

       A7: B is finite;

      

       A8: X[ {} ] by A1;

       X[B] from FINSET_1:sch 2( A7, A8, A3);

      hence thesis;

    end;

    scheme :: ROUGHS_3:sch2

    FinSubIndA2 { X() -> non empty finite set , P[ Subset of X()] } :

for B be non empty Subset of X() holds P[B]

      provided

       A1: for x be Element of X() holds P[ {x}]

       and

       A2: for B1,B2 be non empty Subset of X() st P[B1] & P[B2] holds P[(B1 \/ B2)];

      let B be non empty Subset of X();

      reconsider BB = B as non empty Element of ( Fin X()) by FINSUB_1:def 5;

      defpred PP[ Element of ( Fin X())] means ex C be Subset of X() st C = $1 & P[C];

      

       B1: for x be Element of X() holds PP[ {.x.}]

      proof

        let x be Element of X();

        P[ {x}] by A1;

        hence thesis;

      end;

      

       B2: for B1,B2 be non empty Element of ( Fin X()) st PP[B1] & PP[B2] holds PP[(B1 \/ B2)]

      proof

        let B1,B2 be non empty Element of ( Fin X());

        assume

         K1: PP[B1] & PP[B2];

        then

        reconsider A1 = B1, A2 = B2 as Subset of X();

        P[(A1 \/ A2)] by A2, K1;

        hence thesis;

      end;

      for B be non empty Element of ( Fin X()) holds PP[B] from SETWISEO:sch 3( B1, B2);

      then PP[BB];

      hence thesis;

    end;

    theorem :: ROUGHS_3:1

    

     Th21: for f be Function st ( dom f) is subset-closed & ( dom f) is d.union-closed & f is d.union-distributive holds for a,y be set st a in ( dom f) & y in (f . a) holds ex b be set st b is finite & b c= a & y in (f . b)

    proof

      let f be Function such that

       A1: ( dom f) is subset-closed;

      assume that

       A2: ( dom f) is d.union-closed and

       AA: f is d.union-distributive;

      reconsider C = ( dom f) as d.union-closed subset-closed set by A1, A2;

      let a,y be set;

      assume that

       A3: a in ( dom f) and

       A4: y in (f . a);

      reconsider A = { b where b be Subset of a : b is finite } as set;

      

       A5: A is c=directed

      proof

        let Y be finite Subset of A;

        take ( union Y);

        now

          let x be set;

          assume x in Y;

          then x in A;

          then ex c be Subset of a st x = c & c is finite;

          hence x c= a;

        end;

        then

         A6: ( union Y) c= a by ZFMISC_1: 76;

        now

          let b be set;

          assume b in Y;

          then b in A;

          then ex c be Subset of a st b = c & c is finite;

          hence b is finite;

        end;

        then ( union Y) is finite by FINSET_1: 7;

        hence thesis by A6;

      end;

      

       A7: ( union A) = a

      proof

        thus ( union A) c= a

        proof

          let x be object;

          assume x in ( union A);

          then

          consider b be set such that

           A8: x in b and

           A9: b in A by TARSKI:def 4;

          ex c be Subset of a st b = c & c is finite by A9;

          hence thesis by A8;

        end;

        let x be object;

        assume x in a;

        then {x} c= a by ZFMISC_1: 31;

        then x in {x} & {x} in A by TARSKI:def 1;

        hence thesis by TARSKI:def 4;

      end;

      

       A10: A c= C

      proof

        let x be object;

        assume x in A;

        then ex b be Subset of a st x = b & b is finite;

        hence thesis by A3, CLASSES1:def 1;

      end;

      (f . ( union A)) = ( union (f .: A)) by A3, A7, A5, A10, AA, COHSP_1:def 10;

      then

      consider B be set such that

       A11: y in B and

       A12: B in (f .: A) by A4, A7, TARSKI:def 4;

      consider b be object such that b in ( dom f) and

       A13: b in A and

       A14: B = (f . b) by A12, FUNCT_1:def 6;

      reconsider bb = b as set by TARSKI: 1;

      take bb;

      ex c be Subset of a st b = c & c is finite by A13;

      hence bb is finite & bb c= a & y in (f . bb) by A11, A14;

    end;

    theorem :: ROUGHS_3:2

    

     KeyLemma: for f be Function st ( dom f) is subset-closed & f is union-distributive & ( dom f) is d.union-closed holds for a,y be set st a in ( dom f) & y in (f . a) holds ex x be set st x in a & y in (f . {x})

    proof

      let f be Function;

      assume

       A1: ( dom f) is subset-closed;

      then

      reconsider C = ( dom f) as subset-closed set;

      

       A2: {} is Subset of ( dom f) by XBOOLE_1: 2;

      assume that

       A3: f is union-distributive and

       AB: ( dom f) is d.union-closed;

      let a,y be set;

      assume that

       A4: a in ( dom f) and

       A5: y in (f . a);

      consider b be set such that b is finite and

       A6: b c= a and

       A7: y in (f . b) by A1, A4, A5, Th21, AB, A3;

      

       A9: ( dom f) = C;

      then {} in ( dom f) by A4, CLASSES1:def 1, XBOOLE_1: 2;

      

      then (f . {} ) = ( union (f .: {} )) by A3, A2, ZFMISC_1: 2, COHSP_1:def 9

      .= {} by ZFMISC_1: 2;

      then

      reconsider b as non empty set by A7;

      reconsider A = the set of all {x} where x be Element of b as set;

      

       A10: b in ( dom f) by A4, A6, A9, CLASSES1:def 1;

      

       A11: A c= ( dom f)

      proof

        let X be object;

        reconsider xx = X as set by TARSKI: 1;

        assume X in A;

        then ex x be Element of b st X = {x};

        hence thesis by A9, A10, CLASSES1:def 1;

      end;

      now

        let X be set;

        assume X in A;

        then ex x be Element of b st X = {x};

        hence X c= b;

      end;

      then

       A12: ( union A) in ( dom f) by A9, A10, CLASSES1:def 1, ZFMISC_1: 76;

      reconsider A as Subset of ( dom f) by A11;

      b c= ( union A)

      proof

        let x be object;

        assume x in b;

        then {x} in A;

        then {x} c= ( union A) by ZFMISC_1: 74;

        hence thesis by ZFMISC_1: 31;

      end;

      then

       A13: (f . b) c= (f . ( union A)) by A3, A10, A12, COHSP_1:def 11;

      (f . ( union A)) = ( union (f .: A)) by A3, A12, COHSP_1:def 9;

      then

      consider Y be set such that

       A14: y in Y and

       A15: Y in (f .: A) by A7, A13, TARSKI:def 4;

      consider X be object such that X in ( dom f) and

       A16: X in A and

       A17: Y = (f . X) by A15, FUNCT_1:def 6;

      reconsider X as set by A16;

      consider x be Element of b such that

       A18: X = {x} by A16;

      reconsider x as set;

      take x;

      x in b;

      hence x in a by A6;

      thus y in (f . {x}) by A14, A17, A18;

    end;

    begin

    definition

      let R1,R2 be RelStr;

      :: ROUGHS_3:def1

      func Union (R1,R2) -> strict RelStr means

      : DefUnion: the carrier of it = (the carrier of R1 \/ the carrier of R2) & the InternalRel of it = (the InternalRel of R1 \/ the InternalRel of R2);

      existence

      proof

        set X = (the carrier of R1 \/ the carrier of R2);

        set I = (the InternalRel of R1 \/ the InternalRel of R2);

        

         A2: I c= ( [:the carrier of R1, the carrier of R1:] \/ [:the carrier of R2, the carrier of R2:]) by XBOOLE_1: 13;

        set X1 = the carrier of R1;

        set X2 = the carrier of R2;

        X1 c= X & X2 c= X by XBOOLE_1: 7;

        then [:X1, X1:] c= [:X, X:] & [:X2, X2:] c= [:X, X:] by ZFMISC_1: 96;

        then ( [:X1, X1:] \/ [:X2, X2:]) c= [:X, X:] by XBOOLE_1: 8;

        then

        reconsider I as Relation of X by A2, XBOOLE_1: 1;

        set RR = RelStr (# X, I #);

        the carrier of RR = X & the InternalRel of RR = I;

        hence thesis;

      end;

      uniqueness ;

      commutativity ;

      :: ROUGHS_3:def2

      func Meet (R1,R2) -> strict RelStr means

      : DefMeet: the carrier of it = (the carrier of R1 /\ the carrier of R2) & the InternalRel of it = (the InternalRel of R1 /\ the InternalRel of R2);

      existence

      proof

        set X = (the carrier of R1 /\ the carrier of R2);

        set I = (the InternalRel of R1 /\ the InternalRel of R2);

        

         A2: I c= ( [:the carrier of R1, the carrier of R1:] /\ [:the carrier of R2, the carrier of R2:]) by XBOOLE_1: 27;

        reconsider I as Relation of X by A2, ZFMISC_1: 100;

        set RR = RelStr (# X, I #);

        the carrier of RR = X & the InternalRel of RR = I;

        hence thesis;

      end;

      uniqueness ;

      commutativity ;

    end

    registration

      let R1 be RelStr, R2 be non empty RelStr;

      cluster ( Union (R1,R2)) -> non empty;

      coherence

      proof

        the carrier of ( Union (R1,R2)) = (the carrier of R1 \/ the carrier of R2) by DefUnion;

        hence thesis;

      end;

    end

    begin

    registration

      let A be set;

      cluster /\-preserving \/-preserving for Function of ( bool A), ( bool A);

      existence

      proof

        ( id ( bool A)) in ( Funcs (( bool A),( bool A))) by FUNCT_2: 126;

        then

        reconsider f = ( id ( bool A)) as Function of ( bool A), ( bool A) by FUNCT_2: 66;

        take f;

        thus thesis by ROUGHS_4:def 14, ROUGHS_4:def 12;

      end;

    end

    registration

      let A be set;

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

      cluster ( Flip f) -> \/-preserving;

      coherence

      proof

        for a,b be Subset of A holds (f . (a /\ b)) = ((f . a) /\ (f . b)) by ROUGHS_4:def 10;

        then for a,b be Subset of A holds (( Flip f) . (a \/ b)) = ((( Flip f) . a) \/ (( Flip f) . b)) by ROUGHS_2: 22;

        hence thesis by ROUGHS_4:def 9;

      end;

    end

    registration

      let A be set;

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

      cluster ( Flip f) -> /\-preserving;

      coherence

      proof

        for a,b be Subset of A holds (f . (a \/ b)) = ((f . a) \/ (f . b)) by ROUGHS_4:def 9;

        then for a,b be Subset of A holds (( Flip f) . (a /\ b)) = ((( Flip f) . a) /\ (( Flip f) . b)) by ROUGHS_2: 21;

        hence thesis by ROUGHS_4:def 10;

      end;

    end

    theorem :: ROUGHS_3:3

    

     FlipCC: for A be non empty set holds for f,g be Function of ( bool A), ( bool A) st f cc= g holds ( Flip g) cc= ( Flip f)

    proof

      let A be non empty set;

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

      assume

       A1: f cc= g;

      set ff = ( Flip f), gg = ( Flip g);

      

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

      for x be set st x in ( dom gg) holds (gg . x) c= (ff . x)

      proof

        let x be set;

        assume x in ( dom gg);

        then

        reconsider xx = x as Subset of A;

        

         B1: (( Flip g) . xx) = ((g . (xx ` )) ` ) by ROUGHS_2:def 14;

        

         B2: (( Flip f) . xx) = ((f . (xx ` )) ` ) by ROUGHS_2:def 14;

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

        then (f . (xx ` )) c= (g . (xx ` )) by A1, ALTCAT_2:def 1;

        hence thesis by B1, B2, SUBSET_1: 12;

      end;

      hence thesis by a2, ALTCAT_2:def 1;

    end;

    registration

      cluster non empty mediate transitive for RelStr;

      existence

      proof

        set R = the non empty reflexive transitive RelStr;

        take R;

        thus thesis;

      end;

    end

    registration

      let R be total mediate RelStr;

      cluster the InternalRel of R -> mediate;

      coherence

      proof

        ( field the InternalRel of R) = the carrier of R by ORDERS_1: 12;

        hence thesis by ROUGHS_2:def 6, ROUGHS_2:def 7;

      end;

    end

    theorem :: ROUGHS_3:4

    

     Th13: for L1,L2 be RelStr st the RelStr of L1 = the RelStr of L2 & L1 is mediate holds L2 is mediate

    proof

      let L1,L2 be RelStr;

      assume

       A1: the RelStr of L1 = the RelStr of L2;

      assume L1 is mediate;

      then the InternalRel of L1 is_mediate_in the carrier of L1 by ROUGHS_2:def 7;

      hence thesis by A1, ROUGHS_2:def 7;

    end;

    theorem :: ROUGHS_3:5

    

     NatDay: for L1,L2 be RelStr st the RelStr of L1 = the RelStr of L2 & L1 is serial holds L2 is serial

    proof

      let L1,L2 be RelStr;

      assume

       A1: the RelStr of L1 = the RelStr of L2;

      assume L1 is serial;

      then the InternalRel of L1 is_serial_in the carrier of L1 by ROUGHS_2:def 3;

      hence thesis by A1, ROUGHS_2:def 3;

    end;

    theorem :: ROUGHS_3:6

    

     R224: 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 . X) c= (L . (L . X)) holds for X be Subset of A holds (U . (U . X)) c= (U . X)

    proof

      let A be non empty set, 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 . X) c= (L . (L . X));

      let X be Subset of A;

      

       A3: (U . X) = ((L . (X ` )) ` ) by ROUGHS_2:def 14, A1;

      (U . (U . X)) = (U . ((L . (X ` )) ` )) by ROUGHS_2:def 14, A1

      .= ((L . (((L . (X ` )) ` ) ` )) ` ) by ROUGHS_2:def 14, A1

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

      hence thesis by A3, A2, SUBSET_1: 12;

    end;

    theorem :: ROUGHS_3:7

    

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

    proof

      let R be non empty RelStr;

      let a,b be Element of R;

      

       B1: b in {b} by TARSKI:def 1;

      assume [a, b] in the InternalRel of R;

      then

       B3: b in ( Class (the InternalRel of R,a)) by RELAT_1: 169;

      reconsider B = {b} as Subset of R;

      

       B2: ( Class (the InternalRel of R,a)) meets B by B3, B1, XBOOLE_0: 3;

      ( UAp B) = { x where x be Element of R : ( Class (the InternalRel of R,x)) meets B } by ROUGHS_1:def 5;

      hence thesis by B2;

    end;

    

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

    proof

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

      let x be object;

      assume

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

      then

      reconsider xx = x as Element of R;

      ( Class (the InternalRel of R,x)) meets Y by A1, ROUGHS_2: 7, XBOOLE_1: 74;

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

      then

       A2: x in ( UAp Y) by ROUGHS_1:def 5;

      ( Class (the InternalRel of R,x)) meets X by A1, ROUGHS_2: 7, XBOOLE_1: 74;

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

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

      hence thesis by A2, XBOOLE_0:def 4;

    end;

    theorem :: ROUGHS_3:8

    

     UApAdditive: for R be non empty RelStr, A,B be Subset of R holds (( UAp R) . (A \/ B)) = ((( UAp R) . A) \/ (( UAp R) . B))

    proof

      let R be non empty RelStr;

      let X,Y be Subset of R;

      set H = ( UAp R);

      (H . (X \/ Y)) = ( UAp (X \/ Y)) by ROUGHS_2:def 11

      .= (( UAp X) \/ ( UAp Y)) by ROUGHS_2: 13

      .= ((H . X) \/ ( UAp Y)) by ROUGHS_2:def 11

      .= ((H . X) \/ (H . Y)) by ROUGHS_2:def 11;

      hence thesis;

    end;

    theorem :: ROUGHS_3:9

    for R be non empty RelStr, A,B be Subset of R holds (( LAp R) . (A /\ B)) = ((( LAp R) . A) /\ (( LAp R) . B))

    proof

      let R be non empty RelStr;

      let X,Y be Subset of R;

      set L = ( LAp R);

      (L . (X /\ Y)) = ( LAp (X /\ Y)) by ROUGHS_2:def 10

      .= (( LAp X) /\ ( LAp Y)) by ROUGHS_2: 12

      .= ((L . X) /\ ( LAp Y)) by ROUGHS_2:def 10

      .= ((L . X) /\ (L . Y)) by ROUGHS_2:def 10;

      hence thesis;

    end;

    theorem :: ROUGHS_3:10

    

     UApEmpty: for R be non empty RelStr holds (( UAp R) . {} ) = {}

    proof

      let R be non empty RelStr;

      (( UAp R) . {} ) = ( UAp ( {} R)) by ROUGHS_2:def 11

      .= {} ;

      hence thesis;

    end;

    theorem :: ROUGHS_3:11

    

     Pom1: for R1,R2 be non empty RelStr, X be Subset of R1, Y be Subset of R2 st the RelStr of R1 = the RelStr of R2 & X = Y holds ( UAp X) = ( UAp Y)

    proof

      let R1,R2 be non empty RelStr, X be Subset of R1, Y be Subset of R2;

      assume that

       A1: the RelStr of R1 = the RelStr of R2 and

       A2: X = Y;

      ( UAp X) = { x where x be Element of R1 : ( Class (the InternalRel of R1,x)) meets X } by ROUGHS_1:def 5

      .= ( UAp Y) by A1, A2, ROUGHS_1:def 5;

      hence thesis;

    end;

    theorem :: ROUGHS_3:12

    

     Pom2: for R1,R2 be non empty RelStr, X be Subset of R1, Y be Subset of R2 st the RelStr of R1 = the RelStr of R2 & X = Y holds ( LAp X) = ( LAp Y)

    proof

      let R1,R2 be non empty RelStr, X be Subset of R1, Y be Subset of R2;

      assume that

       A1: the RelStr of R1 = the RelStr of R2 and

       A2: X = Y;

      ( LAp X) = { x where x be Element of R1 : ( Class (the InternalRel of R1,x)) c= X } by ROUGHS_1:def 4

      .= ( LAp Y) by A1, A2, ROUGHS_1:def 4;

      hence thesis;

    end;

    begin

    definition

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

      :: ROUGHS_3:def3

      func GeneratedRelation (R,H) -> Relation of the carrier of R means

      : GRDef: for x,y be Element of R holds [x, y] in it iff x in (H . {y});

      existence

      proof

        defpred P[ Element of R, Element of R] means $1 in (H . {$2});

        consider RR be Relation of the carrier of R such that

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

        take RR;

        thus thesis by A0;

      end;

      uniqueness

      proof

        let R1,R2 be Relation of the carrier of R such that

         A1: for x,y be Element of R holds [x, y] in R1 iff x in (H . {y}) and

         A2: for x,y be Element of R holds [x, y] in R2 iff x in (H . {y});

        for x,y be Element of R holds [x, y] in R1 iff [x, y] in R2

        proof

          let x,y be Element of R;

          hereby

            assume [x, y] in R1;

            then x in (H . {y}) by A1;

            hence [x, y] in R2 by A2;

          end;

          assume [x, y] in R2;

          then x in (H . {y}) by A2;

          hence thesis by A1;

        end;

        hence thesis by RELSET_1:def 2;

      end;

    end

    definition

      let R be non empty RelStr;

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

      :: ROUGHS_3:def4

      func GeneratedRelStr (H) -> RelStr equals RelStr (# the carrier of R, ( GeneratedRelation (R,H)) #);

      coherence ;

    end

    registration

      let R be non empty RelStr;

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

      cluster ( GeneratedRelStr H) -> non empty;

      coherence ;

    end

    theorem :: ROUGHS_3:13

    

     KeyTheorem: for R be finite non empty RelStr, H be Function of ( bool the carrier of R), ( bool the carrier of R) st (H . {} ) = {} & H is \/-preserving holds ( UAp ( GeneratedRelStr H)) = H

    proof

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

      assume

       AA: (H . {} ) = {} & H is \/-preserving;

      

       K1: ( dom H) = ( bool the carrier of R) by FUNCT_2:def 1;

      

       g2: for A be Subset of ( dom H) st ( union A) in ( dom H) holds (H . ( union A)) = ( union (H .: A))

      proof

        let A be Subset of ( dom H);

        per cases ;

          suppose A = {} ;

          hence thesis by AA, ZFMISC_1: 2;

        end;

          suppose

           KJ: A <> {} ;

          assume ( union A) in ( dom H);

          reconsider AA = A as Element of ( Fin ( bool the carrier of R)) by K1, FINSUB_1:def 5;

          reconsider HH = H as Function of ( bool the carrier of R), ( Fin the carrier of R) by FINSUB_1: 14;

          defpred P[ Subset of ( bool the carrier of R)] means (H . ( union $1)) = ( union (H .: $1));

          

           V1: for x be Element of ( bool the carrier of R) holds P[ {x}]

          proof

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

            (H . ( union {x})) = (H . x) by ZFMISC_1: 25

            .= ( union {(H . x)}) by ZFMISC_1: 25

            .= ( union ( Im (H,x))) by K1, FUNCT_1: 59

            .= ( union (H .: {x}));

            hence thesis;

          end;

          

           V2: for B1,B2 be non empty Subset of ( bool the carrier of R) st P[B1] & P[B2] holds P[(B1 \/ B2)]

          proof

            let B1,B2 be non empty Subset of ( bool the carrier of R);

            assume

             BB: P[B1] & P[B2];

            set B12 = (B1 \/ B2);

            

             zx: for g be set st g in B1 holds g c= the carrier of R;

            for g be set st g in B2 holds g c= the carrier of R;

            then

            reconsider U1 = ( union B1), U2 = ( union B2) as Subset of R by zx, ZFMISC_1: 76;

            (H . ( union B12)) = (H . (( union B1) \/ ( union B2))) by ZFMISC_1: 78

            .= ((H . U1) \/ (H . U2)) by ROUGHS_4:def 9, AA

            .= ( union ((H .: B1) \/ (H .: B2))) by ZFMISC_1: 78, BB

            .= ( union (H .: (B1 \/ B2))) by RELAT_1: 120;

            hence thesis;

          end;

          

           SS: for B be non empty Subset of ( bool the carrier of R) holds P[B] from FinSubIndA2( V1, V2);

          reconsider AA = A as non empty Subset of ( bool the carrier of R) by KJ, FUNCT_2:def 1;

          (H . ( union AA)) = ( union (H .: AA)) by SS;

          hence thesis;

        end;

      end;

      set HH = ( UAp ( GeneratedRelStr H));

      for X be Subset of R holds (HH . X) = (H . X)

      proof

        let X be Subset of R;

        

         PS: (HH . X) c= (H . X)

        proof

          let x be object;

          assume

           a1: x in (HH . X);

          reconsider XX = X as Subset of ( GeneratedRelStr H);

          

           a2: x in ( UAp XX) by ROUGHS_2:def 11, a1;

          reconsider xx = x as Element of R by a2;

          consider y be object such that

           a4: y in ( Class (( GeneratedRelation (R,H)),x)) & y in X by a2, XBOOLE_0: 3, ROUGHS_2: 7;

          reconsider y as Element of R by a4;

          reconsider Y = {y} as Subset of R;

           [xx, y] in ( GeneratedRelation (R,H)) by RELSET_2: 9, a4;

          then

           a5: xx in (H . {y}) by GRDef;

          (H . Y) c= (H . X) by AA, ROUGHS_4:def 8, a4, ZFMISC_1: 31;

          hence thesis by a5;

        end;

        (H . X) c= (HH . X)

        proof

          let x be object;

          assume

           a1: x in (H . X);

          reconsider XX = X as Subset of ( GeneratedRelStr H);

          consider y be set such that

           b1: y in X & x in (H . {y}) by a1, KeyLemma, g2, K1, COHSP_1:def 9;

          reconsider xx = x as Element of R by a1;

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

          reconsider xx = x, yy = y as Element of R by a1, b1;

           [xx, yy] in ( GeneratedRelation (R,H)) by GRDef, b1;

          then yy in ( Class (( GeneratedRelation (R,H)),xx)) & y in XX by b1, RELSET_2: 9;

          then ( Class (the InternalRel of ( GeneratedRelStr H),xx)) meets XX by XBOOLE_0: 3;

          then xx in { x where x be Element of ( GeneratedRelStr H) : ( Class (the InternalRel of ( GeneratedRelStr H),x)) meets XX };

          then xx in ( UAp XX) by ROUGHS_1:def 5;

          hence thesis by ROUGHS_2:def 11;

        end;

        hence thesis by XBOOLE_0:def 10, PS;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    begin

    theorem :: ROUGHS_3:14

    

     YaoTh3: for A be finite non empty set, L,H be Function of ( bool A), ( bool A) st L = ( Flip H) holds ((H . {} ) = {} & (for X,Y be Subset of A holds (H . (X \/ Y)) = ((H . X) \/ (H . Y)))) iff ex R be non empty finite RelStr st the carrier of R = A & ( LAp R) = L & ( UAp R) = H & for x,y be Element of R holds [x, y] in the InternalRel of R iff x in (H . {y})

    proof

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

      assume

       ZA: L = ( Flip H);

      thus (H . {} ) = {} & (for X,Y be Subset of A holds (H . (X \/ Y)) = ((H . X) \/ (H . Y))) implies ex R be non empty finite RelStr st the carrier of R = A & ( LAp R) = L & ( UAp R) = H & for x,y be Element of R holds [x, y] in the InternalRel of R iff x in (H . {y})

      proof

        assume

         A0: (H . {} ) = {} & (for X,Y be Subset of A holds (H . (X \/ Y)) = ((H . X) \/ (H . Y)));

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

        consider R be Relation of A such that

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

        set RR = RelStr (# A, R #);

        reconsider RR as finite non empty RelStr;

        

         W1: for X be Subset of RR holds (( UAp RR) . X) = (H . X)

        proof

          let X be Subset of RR;

          deffunc A() = the carrier of RR;

          defpred P[ set] means for X be Subset of RR st X c= $1 holds (( UAp RR) . X) = (H . X);

          

           U1: the carrier of RR is finite;

          for X be Subset of RR st X c= {} holds (( UAp RR) . X) = (H . X)

          proof

            let X be Subset of RR;

            

             F2: ( UAp ( {} RR)) = {} ;

            assume X c= {} ;

            then X = {} ;

            hence thesis by ROUGHS_2:def 11, F2, A0;

          end;

          then

           U2: P[ {} ];

          

           U3: for x,B be set st x in A() & B c= A() & P[B] holds P[(B \/ {x})]

          proof

            let x,B be set;

            assume

             I1: x in A() & B c= A() & P[B];

            

             BE: (H . {x}) = { y where y be Element of RR : x in ( Class (the InternalRel of RR,y)) }

            proof

              thus (H . {x}) c= { y where y be Element of RR : x in ( Class (the InternalRel of RR,y)) }

              proof

                let w be object;

                assume

                 P1: w in (H . {x});

                 {x} c= A by I1, ZFMISC_1: 31;

                then

                 t1: (H . {x}) in ( bool A) by FUNCT_2: 5;

                reconsider xxx = x as Element of A by I1;

                reconsider www = w as Element of RR by t1, P1;

                

                 P2: [www, xxx] in the InternalRel of RR by WW1, P1;

                www in {www} by TARSKI:def 1;

                then x in ( Class (the InternalRel of RR,www)) by P2, RELAT_1:def 13;

                hence thesis;

              end;

              let w be object;

              assume w in { y where y be Element of RR : x in ( Class (the InternalRel of RR,y)) };

              then

              consider ww be Element of RR such that

               P3: ww = w & x in ( Class (the InternalRel of RR,ww));

              consider xx be object such that

               P4: [xx, x] in the InternalRel of RR & xx in {ww} by P3, RELAT_1:def 13;

              xx = ww by P4, TARSKI:def 1;

              hence thesis by WW1, P3, P4;

            end;

            reconsider xx = {x} as Subset of RR by I1, ZFMISC_1: 31;

            

             WX: { y where y be Element of RR : ( Class (the InternalRel of RR,y)) meets xx } = { y where y be Element of RR : x in ( Class (the InternalRel of RR,y)) }

            proof

              thus { y where y be Element of RR : ( Class (the InternalRel of RR,y)) meets xx } c= { y where y be Element of RR : x in ( Class (the InternalRel of RR,y)) }

              proof

                let w be object;

                assume w in { y where y be Element of RR : ( Class (the InternalRel of RR,y)) meets xx };

                then

                consider ww be Element of RR such that

                 H1: ww = w & ( Class (the InternalRel of RR,ww)) meets xx;

                x in ( Class (the InternalRel of RR,ww)) by H1, ZFMISC_1: 50;

                hence thesis by H1;

              end;

              let w be object;

              assume w in { y where y be Element of RR : x in ( Class (the InternalRel of RR,y)) };

              then

              consider ww be Element of RR such that

               H1: ww = w & x in ( Class (the InternalRel of RR,ww));

              ( Class (the InternalRel of RR,ww)) meets xx by H1, ZFMISC_1: 48;

              hence thesis by H1;

            end;

            for X be Subset of RR st X c= (B \/ {x}) holds (( UAp RR) . X) = (H . X)

            proof

              let X be Subset of RR;

              assume

               WW: X c= (B \/ {x});

              (X \ {x}) c= ((B \/ {x}) \ {x}) by WW, XBOOLE_1: 33;

              then

               W8: (X \ {x}) c= (B \ {x}) by XBOOLE_1: 40;

              per cases ;

                suppose

                 XX1: x in X;

                reconsider XX = (X \ {x}) as Subset of RR;

                

                 Ji: (XX \/ xx) = X by XX1, ZFMISC_1: 116;

                

                 OP: ( UAp xx) = (H . xx) by BE, WX, ROUGHS_1:def 5;

                

                 OR: (H . XX) = (( UAp RR) . XX) by W8, XBOOLE_1: 1, I1

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

                (( UAp RR) . X) = ( UAp X) by ROUGHS_2:def 11

                .= (( UAp XX) \/ ( UAp xx)) by ROUGHS_2: 13, Ji

                .= (H . X) by A0, Ji, OP, OR;

                hence thesis;

              end;

                suppose not x in X;

                hence thesis by I1, ZFMISC_1: 135, WW;

              end;

            end;

            hence thesis;

          end;

           P[the carrier of RR] from FINSET_1:sch 2( U1, U2, U3);

          hence thesis;

        end;

        

         T3: ( UAp RR) = H by W1, FUNCT_2: 63;

        then ( LAp RR) = L by ROUGHS_2: 27, ZA;

        hence thesis by T3, WW1;

      end;

      given R be non empty finite RelStr such that

       U0: the carrier of R = A & ( LAp R) = L & ( UAp R) = H & for x,y be Element of R holds [x, y] in the InternalRel of R iff x in (H . {y});

      thus thesis by UApAdditive, U0, UApEmpty;

    end;

    begin

    theorem :: ROUGHS_3:15

    

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

    proof

      let R be non empty transitive RelStr;

      let X be Subset of R;

      let x be object;

      assume x in ( LAp X);

      then x in { u where u be Element of R : ( Class (the InternalRel of R,u)) c= X } by ROUGHS_1:def 4;

      then

      consider y be Element of R such that

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

      ( Class (the InternalRel of R,y)) c= ( LAp X)

      proof

        let t be object;

        assume t in ( Class (the InternalRel of R,y));

        then

         B0: [y, t] in the InternalRel of R by RELAT_1: 169;

        then

         b1: t in ( rng the InternalRel of R) by XTUPLE_0:def 13;

        ( Class (the InternalRel of R,t)) c= X

        proof

          let s be object;

          assume s in ( Class (the InternalRel of R,t));

          then

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

          then s in ( rng the InternalRel of R) by XTUPLE_0:def 13;

          then [y, s] in the InternalRel of R by B0, B2, b1, RELAT_2:def 8, ORDERS_2:def 3;

          then s in ( Im (the InternalRel of R,y)) by RELAT_1: 169;

          hence thesis by A1;

        end;

        then t in { u where u be Element of R : ( Class (the InternalRel of R,u)) c= X } by b1;

        hence thesis by ROUGHS_1:def 4;

      end;

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

      hence thesis by ROUGHS_1:def 4, A1;

    end;

    theorem :: ROUGHS_3:16

    

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

    proof

      let R be non empty transitive RelStr;

      let X be Subset of R;

      let x be object;

      assume x in ( UAp ( UAp X));

      then x in { y where y be Element of R : ( Class (the InternalRel of R,y)) meets ( UAp X) } by ROUGHS_1:def 5;

      then

      consider y be Element of R such that

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

      consider b be object such that

       A2: b in (( Class (the InternalRel of R,y)) /\ ( UAp X)) by XBOOLE_0: 7, XBOOLE_0:def 7, A1;

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

      then

       A3: [y, b] in the InternalRel of R by RELAT_1: 169;

      b in ( UAp X) by A2, XBOOLE_0:def 4;

      then b in { t where t be Element of R : ( Class (the InternalRel of R,t)) meets X } by ROUGHS_1:def 5;

      then

      consider c be Element of R such that

       A4: c = b & ( Class (the InternalRel of R,c)) meets X;

      consider d be object such that

       A5: d in (( Class (the InternalRel of R,c)) /\ X) by XBOOLE_0: 7, A4, XBOOLE_0:def 7;

      

       AA: d in ( Class (the InternalRel of R,c)) & d in X by XBOOLE_0:def 4, A5;

      

       A6: [c, d] in the InternalRel of R & d in X by RELAT_1: 169, AA;

       [y, d] in the InternalRel of R & d in X by ORDERS_2:def 3, RELAT_2:def 8, A6, A3, A4;

      then d in ( Im (the InternalRel of R,y)) & d in X by RELAT_1: 169;

      then d in (( Class (the InternalRel of R,y)) /\ X) by XBOOLE_0:def 4;

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

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

      hence thesis by A1, ROUGHS_1:def 5;

    end;

    theorem :: ROUGHS_3:17

    

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

    proof

      let A be finite non empty set;

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

      assume

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

      set H = ( Flip L);

      

       LL: L = ( Flip H) by ROUGHS_2: 23;

      

       C1: (H . {} ) = {} by A0, ROUGHS_2: 19;

      (for X,Y be Subset of A holds (H . (X \/ Y)) = ((H . X) \/ (H . Y))) by A0, ROUGHS_2: 22;

      then

      consider R be non empty finite RelStr such that

       A1: the carrier of R = A & ( LAp R) = L & ( UAp R) = H & for x,y be Element of R holds [x, y] in the InternalRel of R iff x in (H . {y}) by YaoTh3, LL, C1;

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

      proof

        let x,y,z be object;

        assume

         B1: x in the carrier of R & y in the carrier of R & z in the carrier of R & [x, y] in the InternalRel of R & [y, z] in the InternalRel of R;

        reconsider z as Element of R by B1;

        reconsider xx = x as Element of R by B1;

        reconsider w = x, yw = y as Element of R by B1;

        reconsider XX = {xx} as Subset of R;

        

         zz: L is /\-preserving by A0, ROUGHS_4:def 10;

        reconsider xx = {x}, yy = {y} as Subset of A by ZFMISC_1: 31, A1, B1;

        yy in ( bool A);

        then

        reconsider Hy = (H . {y}) as Subset of A by FUNCT_2: 5;

        

         ZX: {y} c= (H . {z}) by A1, ZFMISC_1: 31, B1;

        reconsider Hz = (H . {z}) as Subset of A by A1, FUNCT_2: 5;

        reconsider az = {z} as Subset of A by A1;

        

         G1: (H . yy) c= (H . Hz) by ROUGHS_4:def 8, zz, ZX;

        (H . (H . az)) c= (H . az) by R224, A0;

        then

         BL: (H . {y}) c= (H . {z}) by G1, XBOOLE_1: 1;

        w in (H . {yw}) by B1, A1;

        hence thesis by A1, BL;

      end;

      then R is transitive by ORDERS_2:def 3, RELAT_2:def 8;

      hence thesis by A1;

    end;

    theorem :: ROUGHS_3:18

    

     ThProposition9U: 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 . (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 finite transitive 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

       A0: (U . {} ) = {} & (for X be Subset of A holds (U . (U . X)) c= (U . X)) & (for X,Y be Subset of A holds (U . (X \/ Y)) = ((U . X) \/ (U . Y)));

      set L = ( Flip U);

      

       a1: (L . A) = A by ROUGHS_2: 18, A0;

      

       a2: for X be Subset of A holds (L . X) c= (L . (L . X)) by ROUGHS_2: 24, A0;

      for X,Y be Subset of A holds (L . (X /\ Y)) = ((L . X) /\ (L . Y)) by A0, ROUGHS_2: 21;

      then

      consider R be non empty finite transitive RelStr such that

       W1: the carrier of R = A & L = ( LAp R) by a1, a2, ThProposition9;

      U = ( Flip L) by ROUGHS_2: 23;

      then U = ( UAp R) by W1, ROUGHS_2: 28;

      hence thesis by W1;

    end;

    begin

    theorem :: ROUGHS_3:19

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

    proof

      let R be non empty mediate transitive RelStr;

      let X be Subset of R;

      

       A0: ( LAp X) c= ( LAp ( LAp X)) by Th95L;

      ( LAp ( LAp X)) c= ( LAp X) by ROUGHS_2: 40;

      hence thesis by A0, XBOOLE_0:def 10;

    end;

    theorem :: ROUGHS_3:20

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

    proof

      let R be non empty mediate transitive RelStr;

      let X be Subset of R;

      

       A0: ( UAp X) c= ( UAp ( UAp X)) by ROUGHS_2: 39;

      ( UAp ( UAp X)) c= ( UAp X) by Th95H;

      hence thesis by A0, XBOOLE_0:def 10;

    end;

    

     Prop17A: for R1,R2 be non empty RelStr st the carrier of R1 = the carrier of R2 & ( UAp R1) cc= ( UAp R2) holds the InternalRel of R1 c= the InternalRel of R2

    proof

      let R1,R2 be non empty RelStr;

      assume

       T0: the carrier of R1 = the carrier of R2;

      assume

       XX: ( UAp R1) cc= ( UAp R2);

      set U1 = ( UAp R1);

      set U2 = ( UAp R2);

      set A = the carrier of R1;

      for x,y be object st [x, y] in the InternalRel of R1 holds [x, y] in the InternalRel of R2

      proof

        let x,y be object;

        assume

         B0: [x, y] in the InternalRel of R1;

        then

         b0: x in the carrier of R1 & y in the carrier of R1 by ZFMISC_1: 87;

        reconsider xx = x, yy = y as Element of R1 by B0, ZFMISC_1: 87;

        

         b1: ( dom ( UAp R1)) = ( bool the carrier of R1) by FUNCT_2:def 1;

         {y} c= the carrier of R1 by ZFMISC_1: 31, b0;

        then

         B1: (( UAp R1) . {y}) c= (( UAp R2) . {y}) by XX, ALTCAT_2:def 1, b1;

        reconsider yyy = {yy} as Subset of R2 by T0;

        reconsider yy1 = {yy} as Subset of R1;

        xx in ( UAp yy1) by Th5A, B0;

        then xx in (( UAp R1) . {yy}) by ROUGHS_2:def 11;

        then x in (( UAp R2) . {y}) by B1;

        then xx in ( UAp yyy) by ROUGHS_2:def 11;

        hence thesis by ROUGHS_2: 5, T0;

      end;

      hence thesis by RELAT_1:def 3;

    end;

    

     Corr3A: for R1,R2 be non empty RelStr st the carrier of R1 = the carrier of R2 & ( UAp R1) = ( UAp R2) holds the InternalRel of R1 = the InternalRel of R2

    proof

      let R1,R2 be non empty RelStr;

      assume

       A1: the carrier of R1 = the carrier of R2 & ( UAp R1) = ( UAp R2);

      

       A2: the InternalRel of R1 c= the InternalRel of R2 by A1, Prop17A;

      the InternalRel of R2 c= the InternalRel of R1 by A1, Prop17A;

      hence thesis by A2, XBOOLE_0:def 10;

    end;

    theorem :: ROUGHS_3:21

    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) = (L . (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 transitive 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

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

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

      then

      consider R be non empty finite transitive RelStr such that

       A1: the carrier of R = A & L = ( LAp R) by ThProposition9, A0;

      for X be Subset of A holds (L . (L . X)) c= (L . X) by A0;

      then

      consider R2 be non empty mediate finite RelStr such that

       A2: the carrier of R2 = A & L = ( LAp R2) by ROUGHS_2: 42, A0;

      reconsider LL = L as Function of ( bool the carrier of R2), ( bool the carrier of R2) by A2;

      set H = ( Flip LL);

      

       F1: (H . {} ) = {} by ROUGHS_2: 19, A0, A2;

      

       f2: for S,T be Subset of the carrier of R2 holds (H . (S \/ T)) = ((H . S) \/ (H . T)) by ROUGHS_2: 22, A2, A0;

      set Rx = ( GeneratedRelStr H);

      

       S2: ( UAp R2) = H by ROUGHS_2: 28, A2;

      

       S3: ( UAp Rx) = H by KeyTheorem, F1, f2, ROUGHS_4:def 9;

      then

       S5: the InternalRel of Rx = the InternalRel of R2 by S2, Corr3A;

      H = ( UAp R) by A1, ROUGHS_2: 28, A2;

      then the InternalRel of Rx = the InternalRel of R by Corr3A, S3, A1, A2;

      then

      reconsider RRR = the RelStr of Rx as non empty finite mediate transitive RelStr by S5, Th13, A2, A1;

      take RRR;

      ( Flip ( UAp RRR)) = ( LAp RRR) by ROUGHS_2: 27;

      hence thesis by ROUGHS_2: 27, A2, S3, S2;

    end;

    theorem :: ROUGHS_3:22

    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 . (U . X)) = (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 transitive 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

       a0: (U . {} ) = {} & (for X be Subset of A holds (U . (U . X)) = (U . X)) & (for X,Y be Subset of A holds (U . (X \/ Y)) = ((U . X) \/ (U . Y)));

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

      then

      consider R be non empty finite transitive RelStr such that

       a1: the carrier of R = A & U = ( UAp R) by ThProposition9U, a0;

      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

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

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

        reconsider x as Element of R by A0;

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

        then (( Class (the InternalRel of R,x)) /\ {y}) <> {} by XBOOLE_0:def 4;

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

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

        then

         B1: x in ( UAp Y) by ROUGHS_1:def 5;

        x in ( UAp ( UAp Y))

        proof

          x in (U . Y) by a1, ROUGHS_2:def 11, B1;

          then x in (U . (U . Y)) by a1, a0;

          then x in (U . ( UAp Y)) by ROUGHS_2:def 11, a1;

          hence thesis by ROUGHS_2:def 11, a1;

        end;

        then x in { t where t be Element of R : ( Class (the InternalRel of R,t)) meets ( UAp Y) } by ROUGHS_1:def 5;

        then

        consider t be Element of R such that

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

        consider z be object such that

         B5: z in (( Class (the InternalRel of R,t)) /\ ( UAp Y)) by XBOOLE_0: 7, B4, XBOOLE_0:def 7;

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

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

        then z in ( {z} /\ ( Class (the InternalRel of R,t))) & z in ( UAp Y) by XBOOLE_0:def 4;

        then ( Class (the InternalRel of R,t)) meets {z} & [z, y] in the InternalRel of R by XBOOLE_0:def 7, ROUGHS_2: 5, A0;

        then t in { w where w be Element of R : ( Class (the InternalRel of R,w)) meets {z} } & [z, y] in the InternalRel of R;

        then t in ( UAp Z) & [z, y] in the InternalRel of R by ROUGHS_1:def 5;

        then [t, z] in the InternalRel of R & [z, y] in the InternalRel of R by ROUGHS_2: 5, B5;

        hence thesis by B4, B5;

      end;

      then R is mediate by ROUGHS_2:def 7, ROUGHS_2:def 5;

      hence thesis by a1;

    end;

    begin

    definition

      let X be set, R be Relation of X;

      :: ROUGHS_3:def5

      pred R is_positive_alliance_in X means for x,y be object st x in X & y in X & not [x, y] in R holds ex z be object st z in X & [x, z] in R & not [z, y] in R;

      :: ROUGHS_3:def6

      pred R is_negative_alliance_in X means for x,y be object st x in X & y in X holds (ex z be object st z in X & [x, z] in R & not [z, y] in R) implies not [x, y] in R;

    end

    definition

      let X be set, R be Relation of X;

      :: ROUGHS_3:def7

      pred R is_alliance_in X means R is_negative_alliance_in X & R is_positive_alliance_in X;

    end

    definition

      let R be non empty RelStr;

      :: ROUGHS_3:def8

      attr R is positive_alliance means

      : DefPA: the InternalRel of R is_positive_alliance_in the carrier of R;

      :: ROUGHS_3:def9

      attr R is negative_alliance means

      : DefNA: the InternalRel of R is_negative_alliance_in the carrier of R;

      :: ROUGHS_3:def10

      attr R is alliance means the InternalRel of R is_alliance_in the carrier of R;

    end

    registration

      cluster reflexive -> positive_alliance for non empty RelStr;

      coherence

      proof

        let R be non empty RelStr;

        assume

         AA: R is reflexive;

        set X = the carrier of R;

        set I = the InternalRel of R;

        the InternalRel of R is_positive_alliance_in the carrier of R

        proof

          let x,y be object;

          assume

           A1: x in X & y in X & not [x, y] in I;

          then

          reconsider x1 = x as Element of R;

           [x1, x1] in I by ORDERS_2:def 5, AA, YELLOW_0:def 1;

          hence thesis by A1;

        end;

        hence thesis;

      end;

      cluster discrete -> negative_alliance for non empty RelStr;

      coherence

      proof

        let R be non empty RelStr;

        assume

         AA: R is discrete;

        set X = the carrier of R;

        set I = the InternalRel of R;

        let x,y be object;

        assume x in X & y in X;

        then

        reconsider x1 = x as Element of R;

        given z be object such that

         E1: z in X & [x, z] in I & not [z, y] in I;

        reconsider z1 = z as Element of R by E1;

        x1 <= z1 by E1, ORDERS_2:def 5;

        hence thesis by E1, AA, ORDERS_3: 1;

      end;

    end

    registration

      cluster positive_alliance negative_alliance for non empty RelStr;

      existence

      proof

        set R = the discrete reflexive non empty RelStr;

        R is positive_alliance;

        hence thesis;

      end;

    end

    registration

      cluster alliance -> positive_alliance negative_alliance for non empty RelStr;

      coherence

      proof

        let R be non empty RelStr;

        set I = the InternalRel of R;

        set X = the carrier of R;

        assume R is alliance;

        then I is_alliance_in X;

        hence thesis;

      end;

      cluster positive_alliance negative_alliance -> alliance for non empty RelStr;

      coherence

      proof

        let R be non empty RelStr;

        set I = the InternalRel of R;

        set X = the carrier of R;

        assume R is positive_alliance negative_alliance;

        then I is_alliance_in X;

        hence thesis;

      end;

    end

    registration

      cluster positive_alliance -> serial for non empty RelStr;

      coherence

      proof

        let R be non empty RelStr;

        assume

         AA: R is positive_alliance;

        set X = the carrier of R;

        set I = the InternalRel of R;

        

         b2: I is_positive_alliance_in X by AA;

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

        proof

          let x be object;

          assume

           B0: x in X;

          ex y be object st y in X & [x, y] in I

          proof

            per cases ;

              suppose [x, x] in I;

              hence thesis by B0;

            end;

              suppose not [x, x] in I;

              then

              consider z be object such that

               B3: z in X & [x, z] in I & not [z, x] in I by B0, b2;

              thus thesis by B3;

            end;

          end;

          hence thesis;

        end;

        hence thesis by ROUGHS_2:def 3, ROUGHS_2:def 1;

      end;

      cluster transitive serial -> positive_alliance for non empty RelStr;

      coherence

      proof

        let R be non empty RelStr;

        assume

         AA: R is transitive serial;

        set X = the carrier of R;

        set I = the InternalRel of R;

        for x,y be object st x in X & y in X & not [x, y] in I holds ex z be object st z in X & [x, z] in I & not [z, y] in I

        proof

          let x,y be object;

          assume

           A0: x in X & y in X & not [x, y] in I;

          then

          consider z be object such that

           A1: z in X & [x, z] in I by ROUGHS_2:def 1, AA, ROUGHS_2:def 3;

          take z;

          thus thesis by A0, A1, AA, ORDERS_2:def 3, RELAT_2:def 8;

        end;

        then I is_positive_alliance_in X;

        hence thesis;

      end;

    end

    theorem :: ROUGHS_3:23

    

     NegReg: for L1,L2 be non empty RelStr st the RelStr of L1 = the RelStr of L2 & L1 is negative_alliance holds L2 is negative_alliance;

    theorem :: ROUGHS_3:24

    

     PosReg: for L1,L2 be non empty RelStr st the RelStr of L1 = the RelStr of L2 & L1 is positive_alliance holds L2 is positive_alliance;

    theorem :: ROUGHS_3:25

    for L1,L2 be non empty RelStr st the RelStr of L1 = the RelStr of L2 & L1 is alliance holds L2 is alliance;

    begin

    definition

      let R be non empty RelStr;

      :: ROUGHS_3:def11

      attr R is satisfying(7H') means for X be Subset of R holds (( UAp X) ` ) c= ( UAp (( UAp X) ` ));

      :: ROUGHS_3:def12

      attr R is satisfying(7L') means for X be Subset of R holds ( LAp (( LAp X) ` )) c= (( LAp X) ` );

    end

    theorem :: ROUGHS_3:26

    

     Sat7Sat: for R be finite non empty RelStr st R is satisfying(7L') holds R is satisfying(7H')

    proof

      let R be finite non empty RelStr;

      assume

       tr: R is satisfying(7L');

      for X be Subset of R holds (( UAp X) ` ) c= ( UAp (( UAp X) ` ))

      proof

        let X be Subset of R;

        

         H1: ( UAp X) = ( Uap X) by ROUGHS_2: 8

        .= (( LAp (X ` )) ` ) by ROUGHS_2:def 8;

        then ((( LAp (X ` )) ` ) ` ) c= (( LAp ( UAp X)) ` ) by tr, SUBSET_1: 12;

        then (( UAp X) ` ) c= (( Lap ( UAp X)) ` ) by H1, ROUGHS_2: 9;

        then (( UAp X) ` ) c= ((( UAp (( UAp X) ` )) ` ) ` ) by ROUGHS_2:def 9;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: ROUGHS_3:27

    

     Sat7Serial: for R be finite non empty RelStr st R is satisfying(7H') holds R is serial

    proof

      let R be finite non empty RelStr;

      set U = ( UAp R);

      assume

       tr: R is satisfying(7H');

      (( UAp ( {} R)) ` ) = ( [#] R);

      then

       Y2: ( [#] R) c= ( UAp ( [#] R)) by tr;

      

       FF: (U . ( [#] R)) = ( UAp ( [#] R)) by ROUGHS_2:def 11

      .= the carrier of R by Y2, XBOOLE_0:def 10;

      

       FO: (U . {} ) = ( UAp ( {} R)) by ROUGHS_2:def 11

      .= {} ;

      for X,Y be Subset of R holds (U . (X \/ Y)) = ((U . X) \/ (U . Y))

      proof

        let X,Y be Subset of R;

        (U . (X \/ Y)) = ( UAp (X \/ Y)) by ROUGHS_2:def 11

        .= (( UAp X) \/ ( UAp Y)) by ROUGHS_2: 13

        .= ((U . X) \/ ( UAp Y)) by ROUGHS_2:def 11

        .= ((U . X) \/ (U . Y)) by ROUGHS_2:def 11;

        hence thesis;

      end;

      then

      consider S be non empty finite serial RelStr such that

       H1: the carrier of S = the carrier of R & U = ( UAp S) by ROUGHS_2: 32, FF, FO;

       the RelStr of S = the RelStr of R by Corr3A, H1;

      hence thesis by NatDay;

    end;

    theorem :: ROUGHS_3:28

    for R be finite non empty RelStr st R is satisfying(7L') holds R is serial by Sat7Serial, Sat7Sat;

    registration

      cluster satisfying(7H') -> serial for finite non empty RelStr;

      coherence by Sat7Serial;

    end

    theorem :: ROUGHS_3:29

    

     Conv: for R be non empty RelStr st (for X be Subset of R holds ( UAp (( UAp X) ` )) c= (( UAp X) ` )) holds for X be Subset of R holds (( LAp X) ` ) c= ( LAp (( LAp X) ` ))

    proof

      let R be non empty RelStr;

      assume

       TR: (for X be Subset of R holds ( UAp (( UAp X) ` )) c= (( UAp X) ` ));

      let X be Subset of R;

      

       H1: ( LAp X) = ( Lap X) by ROUGHS_2: 9

      .= (( UAp (X ` )) ` ) by ROUGHS_2:def 9;

      then ((( UAp (X ` )) ` ) ` ) c= (( UAp ( LAp X)) ` ) by TR, SUBSET_1: 12;

      then (( LAp X) ` ) c= (( Uap ( LAp X)) ` ) by H1, ROUGHS_2: 8;

      then (( LAp X) ` ) c= ((( LAp (( LAp X) ` )) ` ) ` ) by ROUGHS_2:def 8;

      hence thesis;

    end;

    theorem :: ROUGHS_3:30

    

     Conv2: 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 . X) ` ) c= (L . ((L . X) ` ))) holds for X be Subset of A holds (U . ((U . X) ` )) c= ((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 . X) ` ) c= (L . ((L . X) ` ));

      let X be Subset of A;

      

       A3: (U . X) = ((L . (X ` )) ` ) by ROUGHS_2:def 14, A1;

      ((L . (((U . X) ` ) ` )) ` ) = (U . ((U . X) ` )) by ROUGHS_2:def 14, A1;

      hence thesis by A2, A3, SUBSET_1: 12;

    end;

    theorem :: ROUGHS_3:31

    

     Conv3: 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 (U . ((U . X) ` )) c= ((U . X) ` )) holds for X be Subset of A holds ((L . X) ` ) c= (L . ((L . 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 (U . ((U . X) ` )) c= ((U . X) ` );

      let X be Subset of A;

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

      then ((L . ((X ` ) ` )) ` ) c= ((U . ((U . (X ` )) ` )) ` ) by A1, ROUGHS_2:def 14;

      then ((L . X) ` ) c= ((U . (((L . X) ` ) ` )) ` ) by A1, ROUGHS_2:def 14;

      then ((L . X) ` ) c= (((L . ((L . X) ` )) ` ) ` ) by A1, ROUGHS_2:def 14;

      hence thesis;

    end;

    theorem :: ROUGHS_3:32

    

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

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

      then ((U . ((X ` ) ` )) ` ) c= ((L . ((L . (X ` )) ` )) ` ) by A1, ROUGHS_2:def 14;

      then ((U . X) ` ) c= ((L . (((U . X) ` ) ` )) ` ) by A1, ROUGHS_2:def 14;

      hence thesis by A1, ROUGHS_2:def 14;

    end;

    begin

    theorem :: ROUGHS_3:33

    for R be finite positive_alliance non empty RelStr, x be Element of R holds ((( UAp R) . {x}) ` ) c= (( UAp R) . ((( UAp R) . {x}) ` ))

    proof

      let R be finite positive_alliance non empty RelStr, x be Element of R;

      set H = ( UAp R);

      set L = ( Flip H);

      

       w1: (H . {} ) = {} by UApEmpty;

      

       w5: for X,Y be Subset of R holds (H . (X \/ Y)) = ((H . X) \/ (H . Y)) by UApAdditive;

      set RR = ( GeneratedRelStr H);

      

       w3: ( UAp R) = ( UAp ( GeneratedRelStr H)) by KeyTheorem, w1, w5, ROUGHS_4:def 9;

      

       WW: for x,y be Element of RR holds [x, y] in the InternalRel of RR iff x in (H . {y}) by GRDef;

      

       WZ: the InternalRel of RR = the InternalRel of R by Corr3A, w3;

      

       W1: the InternalRel of R is_positive_alliance_in the carrier of R by DefPA;

      let y be object;

      assume

       w2: y in ((H . {x}) ` );

      then

       w1: not y in (H . {x}) by XBOOLE_0:def 5;

      reconsider xx = x, yy = y as Element of RR by w2;

       not [yy, xx] in the InternalRel of RR by w1, GRDef;

      then

      consider z be object such that

       W2: z in the carrier of R & [y, z] in the InternalRel of R and

       W3: not [z, x] in the InternalRel of RR by W1, WZ;

      reconsider zz = z as Element of RR by W2;

      

       W5: yy in (H . {zz}) by W2, GRDef, WZ;

      

       j1: {z} c= the carrier of R by ZFMISC_1: 31, W2;

      

       w6: z in ((H . {x}) ` ) by W3, WW, SUBSET_1: 29, W2;

      for X,Y be Subset of R holds (H . (X \/ Y)) = ((H . X) \/ (H . Y)) by UApAdditive;

      then H is \/-preserving by ROUGHS_4:def 9;

      then (H . {z}) c= (H . ((H . {x}) ` )) by w6, j1, ROUGHS_4:def 8, ZFMISC_1: 31;

      hence thesis by W5;

    end;

    theorem :: ROUGHS_3:34

    

     Prop11: 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 positive_alliance finite non empty 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

       a0: (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)));

      then

      consider R be non empty finite RelStr such that

       a1: the carrier of R = A & ( LAp R) = ( Flip U) & ( UAp R) = U & for x,y be Element of R holds [x, y] in the InternalRel of R iff x in (U . {y}) by YaoTh3;

      set X = the carrier of R;

      set I = the InternalRel of R;

      for x,y be object st x in X & y in X & not [x, y] in I holds ex z be object st z in X & [x, z] in I & not [z, y] in I

      proof

        let x,y be object;

        assume

         W1: x in X & y in X & not [x, y] in I;

        then

        reconsider xx = x, yy = y as Element of R;

        

         a3: ((( UAp R) . {yy}) ` ) c= (U . ((( UAp R) . {yy}) ` )) by a0, a1;

         not xx in (( UAp R) . {yy}) by W1, a1;

        then xx in ((( UAp R) . {yy}) ` ) by XBOOLE_0:def 5;

        then xx in (( UAp R) . ((( UAp R) . {yy}) ` )) by a3, a1;

        then xx in ( UAp ((( UAp R) . {yy}) ` )) by ROUGHS_2:def 11;

        then

        consider z be object such that

         J1: z in ( Class (the InternalRel of R,xx)) & z in ((( UAp R) . {yy}) ` ) by XBOOLE_0: 3, ROUGHS_2: 7;

        reconsider zz = z as Element of R by J1;

        

         J2: [xx, zz] in I by J1, RELAT_1: 169;

         not zz in (( UAp R) . {yy}) by J1, XBOOLE_0:def 5;

        then not [z, y] in I by a1;

        hence thesis by J2;

      end;

      then the InternalRel of R is_positive_alliance_in X;

      then R is positive_alliance;

      hence thesis by a1;

    end;

    theorem :: ROUGHS_3:35

    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 positive_alliance finite non empty 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

       A1: (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));

      set U = ( Flip L);

      

       A2: for X be Subset of A holds ((U . X) ` ) c= (U . ((U . X) ` )) by A1, Conv4;

      

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

      (for X,Y be Subset of A holds (U . (X \/ Y)) = ((U . X) \/ (U . Y))) by ROUGHS_2: 22, A1;

      then

      consider R be positive_alliance finite non empty RelStr such that

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

      L = ( Flip ( UAp R)) by A3, ROUGHS_2: 23;

      then L = ( LAp R) by ROUGHS_2: 27;

      hence thesis by A3;

    end;

    theorem :: ROUGHS_3:36

    

     Prop137H: for R be finite negative_alliance non empty RelStr, x be Element of R holds (( UAp R) . ((( UAp R) . {x}) ` )) c= ((( UAp R) . {x}) ` )

    proof

      let R be finite negative_alliance non empty RelStr, x be Element of R;

      set H = ( UAp R);

      set L = ( Flip H);

      

       w1: (H . {} ) = {} by UApEmpty;

      

       w5: for X,Y be Subset of R holds (H . (X \/ Y)) = ((H . X) \/ (H . Y)) by UApAdditive;

      set RR = ( GeneratedRelStr H);

      

       w3: ( UAp R) = ( UAp ( GeneratedRelStr H)) by KeyTheorem, w1, w5, ROUGHS_4:def 9;

      

       WZ: the InternalRel of RR = the InternalRel of R by Corr3A, w3;

      

       W1: the InternalRel of R is_negative_alliance_in the carrier of R by DefNA;

      let y be object;

      assume

       w2: y in (H . ((H . {x}) ` ));

      reconsider Hx = ((H . {x}) ` ) as Subset of R;

      y in ( UAp Hx) by w2, ROUGHS_2:def 11;

      then

      consider z be object such that

       O1: z in ( Class (the InternalRel of R,y)) & z in Hx by XBOOLE_0: 3, ROUGHS_2: 7;

      

       p1: [y, z] in the InternalRel of R by O1, RELAT_1: 169;

      reconsider zz = z, yy = y as Element of RR by O1, w2;

      reconsider xx = x as Element of RR;

       not zz in (H . {x}) by O1, XBOOLE_0:def 5;

      then

       p2: not [zz, x] in the InternalRel of RR by GRDef;

      set W = the carrier of R, I = the InternalRel of R;

       not [yy, xx] in I by W1, WZ, p2, p1;

      then not yy in (H . {xx}) by GRDef, WZ;

      hence thesis by XBOOLE_0:def 5;

    end;

    theorem :: ROUGHS_3:37

    

     Prop13H: for R be finite negative_alliance non empty RelStr, X be Subset of R holds ( UAp (( UAp X) ` )) c= (( UAp X) ` )

    proof

      let R be finite negative_alliance non empty RelStr;

      let X be Subset of R;

      defpred P[ Subset of R] means ( UAp (( UAp $1) ` )) c= (( UAp $1) ` );

      ( {} R) = {} ;

      then

       A1: P[( {} the carrier of R)];

      

       A2: for B be Subset of R, b be Element of R holds P[B] & not b in B implies P[(B \/ {b})]

      proof

        let B be Subset of R, b be Element of R;

        assume

         z1: P[B] & not b in B;

        reconsider Bb = (B \/ {b}) as Subset of R;

        ( UAp (( UAp Bb) ` )) = ( UAp ((( UAp B) \/ ( UAp {b})) ` )) by ROUGHS_2: 13

        .= ( UAp ((( UAp B) ` ) /\ (( UAp {b}) ` ))) by XBOOLE_1: 53;

        then

         Z2: ( UAp (( UAp Bb) ` )) c= (( UAp (( UAp B) ` )) /\ ( UAp (( UAp {b}) ` ))) by UApCon;

        (( UAp (( UAp B) ` )) /\ ( UAp (( UAp {b}) ` ))) c= ((( UAp B) ` ) /\ ( UAp (( UAp {b}) ` ))) by z1, XBOOLE_1: 26;

        then

         Z3: ( UAp (( UAp Bb) ` )) c= ((( UAp B) ` ) /\ ( UAp (( UAp {b}) ` ))) by Z2, XBOOLE_1: 1;

        (( UAp R) . ((( UAp R) . {b}) ` )) c= ((( UAp R) . {b}) ` ) by Prop137H;

        then (( UAp R) . ((( UAp R) . {b}) ` )) c= (( UAp {b}) ` ) by ROUGHS_2:def 11;

        then (( UAp R) . (( UAp {b}) ` )) c= (( UAp {b}) ` ) by ROUGHS_2:def 11;

        then ( UAp (( UAp {b}) ` )) c= (( UAp {b}) ` ) by ROUGHS_2:def 11;

        then

         z4: ((( UAp B) ` ) /\ ( UAp (( UAp {b}) ` ))) c= ((( UAp B) ` ) /\ (( UAp {b}) ` )) by XBOOLE_1: 26;

        ((( UAp B) ` ) /\ (( UAp {b}) ` )) = ((( UAp B) \/ ( UAp {b})) ` ) by XBOOLE_1: 53

        .= (( UAp Bb) ` ) by ROUGHS_2: 13;

        hence thesis by z4, Z3, XBOOLE_1: 1;

      end;

      for B be Subset of R holds P[B] from FinSubIndA1( A1, A2);

      hence thesis;

    end;

    theorem :: ROUGHS_3:38

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

    proof

      let R be finite negative_alliance non empty RelStr;

      for X be Subset of R holds ( UAp (( UAp X) ` )) c= (( UAp X) ` ) by Prop13H;

      hence thesis by Conv;

    end;

    theorem :: ROUGHS_3:39

    

     Prop14: 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 . ((U . X) ` )) c= ((U . X) ` )) & (for X,Y be Subset of A holds (U . (X \/ Y)) = ((U . X) \/ (U . Y))) holds ex R be negative_alliance finite non empty 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

       a0: (U . {} ) = {} & (for X be Subset of A holds (U . ((U . X) ` )) c= ((U . X) ` )) & (for X,Y be Subset of A holds (U . (X \/ Y)) = ((U . X) \/ (U . Y)));

      then

      consider R be non empty finite RelStr such that

       a1: the carrier of R = A & ( LAp R) = ( Flip U) & ( UAp R) = U & for x,y be Element of R holds [x, y] in the InternalRel of R iff x in (U . {y}) by YaoTh3;

      set X = the carrier of R;

      set I = the InternalRel of R;

      for x,y be object st x in X & y in X holds (ex z be object st z in X & [x, z] in I & not [z, y] in I) implies not [x, y] in I

      proof

        let x,y be object;

        assume x in X & y in X;

        then

        reconsider xx = x, yy = y as Element of R;

        given z be object such that

         A1: z in X & [x, z] in I & not [z, y] in I;

        reconsider zz = z as Element of R by A1;

         not zz in (( UAp R) . {yy}) by A1, a1;

        then

         B0: zz in ((( UAp R) . {yy}) ` ) by XBOOLE_0:def 5;

        

         B1: zz in ( Class (the InternalRel of R,xx)) by RELAT_1: 169, A1;

        

         B5: (( UAp R) . ((( UAp R) . {yy}) ` )) c= ((( UAp R) . {yy}) ` ) by a0, a1;

        ( Class (the InternalRel of R,xx)) meets ((( UAp R) . {yy}) ` ) by B1, XBOOLE_0: 3, B0;

        then xx in { x where x be Element of R : ( Class (the InternalRel of R,x)) meets ((( UAp R) . {yy}) ` ) };

        then xx in ( UAp ((( UAp R) . {yy}) ` )) by ROUGHS_1:def 5;

        then xx in (( UAp R) . ((( UAp R) . {yy}) ` )) by ROUGHS_2:def 11;

        then not xx in (( UAp R) . {yy}) by B5, XBOOLE_0:def 5;

        hence thesis by a1;

      end;

      then the InternalRel of R is_negative_alliance_in X;

      then R is negative_alliance;

      hence thesis by a1;

    end;

    theorem :: ROUGHS_3:40

    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 . ((L . X) ` ))) & (for X,Y be Subset of A holds (L . (X /\ Y)) = ((L . X) /\ (L . Y))) holds ex R be negative_alliance finite non empty 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

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

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

      set U = ( Flip L);

      

       C1: (U . {} ) = {} by A1, ROUGHS_2: 19;

      

       C2: for X be Subset of A holds (U . ((U . X) ` )) c= ((U . X) ` ) by A3, Conv2;

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

      then

      consider R be negative_alliance finite non empty RelStr such that

       A2: the carrier of R = A & U = ( UAp R) by Prop14, C1, C2;

      ( Flip U) = ( LAp R) by A2, ROUGHS_2: 27;

      then L = ( LAp R) by ROUGHS_2: 23;

      hence thesis by A2;

    end;

    

     Prop18: for R1,R2 be non empty RelStr st the carrier of R1 = the carrier of R2 & ( LAp R1) cc= ( LAp R2) holds the InternalRel of R2 c= the InternalRel of R1

    proof

      let R1,R2 be non empty RelStr;

      assume

       A1: the carrier of R1 = the carrier of R2 & ( LAp R1) cc= ( LAp R2);

      ( UAp R1) = ( Flip ( LAp R1)) & ( UAp R2) = ( Flip ( LAp R2)) by ROUGHS_2: 28;

      hence thesis by Prop17A, A1, FlipCC;

    end;

    

     The5: for R1,R2 be non empty RelStr st the carrier of R1 = the carrier of R2 holds ( UAp R1) = ( UAp R2) iff the InternalRel of R1 = the InternalRel of R2

    proof

      let R1,R2 be non empty RelStr;

      assume

       A1: the carrier of R1 = the carrier of R2;

      hence ( UAp R1) = ( UAp R2) implies the InternalRel of R1 = the InternalRel of R2 by Corr3A;

      assume the InternalRel of R1 = the InternalRel of R2;

      then

       A2: the RelStr of R1 = the RelStr of R2 by A1;

      for x be Subset of R1 holds (( UAp R1) . x) = (( UAp R2) . x)

      proof

        let x be Subset of R1;

        reconsider xx = x as Subset of R2 by A1;

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

        .= ( UAp xx) by A2, Pom1

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

        hence thesis;

      end;

      hence thesis by FUNCT_2: 63, A1;

    end;

    theorem :: ROUGHS_3:41

    

     Th2H: 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 . ((U . X) ` )) = ((U . X) ` )) & (for X,Y be Subset of A holds (U . (X \/ Y)) = ((U . X) \/ (U . Y))) holds ex R be alliance finite non empty RelStr st the carrier of R = A & U = ( UAp R)

    proof

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

      assume

       A1: (U . {} ) = {} & (for X be Subset of A holds (U . ((U . X) ` )) = ((U . X) ` )) & (for X,Y be Subset of A holds (U . (X \/ Y)) = ((U . X) \/ (U . Y)));

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

      then

      consider R be negative_alliance finite non empty RelStr such that

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

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

      then

      consider S be positive_alliance finite non empty RelStr such that

       A3: the carrier of S = A & U = ( UAp S) by Prop11, A1;

      

       A4: the RelStr of S = the RelStr of R by A2, A3, Corr3A;

      set RR = the RelStr of R;

      

       A5: RR is positive_alliance by A4, PosReg;

      RR is negative_alliance by NegReg;

      then

      reconsider RR as alliance finite non empty RelStr by A5;

      ( UAp RR) = ( UAp R) by The5;

      hence thesis by A2;

    end;

    theorem :: ROUGHS_3: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 . X) ` ) = (L . ((L . X) ` ))) & (for X,Y be Subset of A holds (L . (X /\ Y)) = ((L . X) /\ (L . Y))) holds ex R be alliance finite non empty 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

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

      set U = ( Flip L);

      

       A2: (U . {} ) = {} by A0, ROUGHS_2: 19;

      

       A3: for X be Subset of A holds (U . ((U . X) ` )) = ((U . X) ` )

      proof

        let X be Subset of A;

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

        then

         Z1: (U . ((U . X) ` )) c= ((U . X) ` ) by Conv2;

        

         Z2: L = ( Flip U) by ROUGHS_2: 23;

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

        then ((U . X) ` ) c= (U . ((U . X) ` )) by Conv3, Z2;

        hence thesis by Z1, XBOOLE_0:def 10;

      end;

      for X,Y be Subset of A holds (U . (X \/ Y)) = ((U . X) \/ (U . Y)) by A0, ROUGHS_2: 22;

      then

      consider R be alliance finite non empty RelStr such that

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

      ( Flip U) = L by ROUGHS_2: 23;

      then L = ( LAp R) by A1, ROUGHS_2: 27;

      hence thesis by A1;

    end;

    begin

    theorem :: ROUGHS_3:43

    for R1,R2,R be non empty RelStr, X be Subset of R, X1 be Subset of R1, X2 be Subset of R2 st R = ( Union (R1,R2)) & X = X1 & X = X2 & the carrier of R1 = the carrier of R2 holds ( UAp X) = (( UAp X1) \/ ( UAp X2))

    proof

      let R1,R2,R be non empty RelStr, X be Subset of R, X1 be Subset of R1, X2 be Subset of R2;

      assume

       A1: R = ( Union (R1,R2)) & X = X1 & X = X2 & the carrier of R1 = the carrier of R2;

      then

       A0: the InternalRel of R = (the InternalRel of R1 \/ the InternalRel of R2) by DefUnion;

      

       b1: the carrier of R = (the carrier of R1 \/ the carrier of R2) by A1, DefUnion;

      

       C1: ( UAp X) c= (( UAp X1) \/ ( UAp X2))

      proof

        let x be object;

        assume x in ( UAp X);

        then x in { x where x be Element of R : ( Class (the InternalRel of R,x)) meets X } by ROUGHS_1:def 5;

        then

        consider xx be Element of R such that

         A2: xx = x & ( Class (the InternalRel of R,xx)) meets X;

        consider z be object such that

         A3: z in ( Class (the InternalRel of R,xx)) & z in X by A2, XBOOLE_0: 3;

        reconsider zz = z as Element of R by A3;

         [xx, zz] in the InternalRel of R by A3, RELAT_1: 169;

        then

         B2: [xx, zz] in the InternalRel of R1 or [xx, zz] in the InternalRel of R2 by XBOOLE_0:def 3, A0;

        reconsider x1 = xx, z1 = zz as Element of R1 by A1, b1;

        reconsider x2 = xx, z2 = zz as Element of R2 by A1, b1;

        z1 in ( Class (the InternalRel of R1,x1)) or z2 in ( Class (the InternalRel of R2,x2)) by B2, RELAT_1: 169;

        then ( Class (the InternalRel of R1,x1)) meets X or ( Class (the InternalRel of R2,x2)) meets X by A3, XBOOLE_0: 3;

        then x1 in { x where x be Element of R1 : ( Class (the InternalRel of R1,x)) meets X1 } or x2 in { x where x be Element of R2 : ( Class (the InternalRel of R2,x)) meets X2 } by A1;

        then x1 in ( UAp X1) or x2 in ( UAp X2) by ROUGHS_1:def 5;

        hence thesis by A2, XBOOLE_0:def 3;

      end;

      (( UAp X1) \/ ( UAp X2)) c= ( UAp X)

      proof

        let x be object;

        assume x in (( UAp X1) \/ ( UAp X2));

        per cases by XBOOLE_0:def 3;

          suppose x in ( UAp X1);

          then x in { x where x be Element of R1 : ( Class (the InternalRel of R1,x)) meets X1 } by ROUGHS_1:def 5;

          then

          consider xx be Element of R1 such that

           C1: xx = x & ( Class (the InternalRel of R1,xx)) meets X1;

          reconsider xxx = xx as Element of R by A1, b1;

          consider z be object such that

           C2: z in ( Class (the InternalRel of R1,xx)) & z in X1 by C1, XBOOLE_0: 3;

          reconsider zz = z as Element of R1 by C2;

           [xx, zz] in the InternalRel of R1 by C2, RELAT_1: 169;

          then [xx, zz] in (the InternalRel of R1 \/ the InternalRel of R2) by XBOOLE_0:def 3;

          then zz in ( Class (the InternalRel of R,xx)) by A0, RELAT_1: 169;

          then ( Class (the InternalRel of R,xx)) meets X1 by C2, XBOOLE_0: 3;

          then xxx in { x where x be Element of R : ( Class (the InternalRel of R,x)) meets X } by A1;

          hence thesis by C1, ROUGHS_1:def 5;

        end;

          suppose x in ( UAp X2);

          then x in { x where x be Element of R2 : ( Class (the InternalRel of R2,x)) meets X2 } by ROUGHS_1:def 5;

          then

          consider xx be Element of R2 such that

           C1: xx = x & ( Class (the InternalRel of R2,xx)) meets X2;

          reconsider xxx = xx as Element of R by b1, A1;

          consider z be object such that

           C2: z in ( Class (the InternalRel of R2,xx)) & z in X2 by C1, XBOOLE_0: 3;

          reconsider zz = z as Element of R2 by C2;

           [xx, zz] in the InternalRel of R2 by C2, RELAT_1: 169;

          then [xx, zz] in (the InternalRel of R1 \/ the InternalRel of R2) by XBOOLE_0:def 3;

          then zz in ( Class (the InternalRel of R,xx)) by A0, RELAT_1: 169;

          then ( Class (the InternalRel of R,xx)) meets X2 by C2, XBOOLE_0: 3;

          then xxx in { x where x be Element of R : ( Class (the InternalRel of R,x)) meets X } by A1;

          hence thesis by C1, ROUGHS_1:def 5;

        end;

      end;

      hence thesis by XBOOLE_0:def 10, C1;

    end;

    theorem :: ROUGHS_3:44

    for R1,R2,R be non empty RelStr, X be Subset of R, X1 be Subset of R1, X2 be Subset of R2 st R = ( Union (R1,R2)) & X = X1 & X = X2 & the carrier of R1 = the carrier of R2 holds ( LAp X) = (( LAp X1) /\ ( LAp X2))

    proof

      let R1,R2,R be non empty RelStr, X be Subset of R, X1 be Subset of R1, X2 be Subset of R2;

      assume

       A1: R = ( Union (R1,R2)) & X = X1 & X = X2 & the carrier of R1 = the carrier of R2;

      then

       A0: the InternalRel of R = (the InternalRel of R1 \/ the InternalRel of R2) by DefUnion;

      

       b1: the carrier of R = (the carrier of R1 \/ the carrier of R2) by A1, DefUnion;

      

       D1: ( LAp X) c= (( LAp X1) /\ ( LAp X2))

      proof

        let x be object;

        assume x in ( LAp X);

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

        then

        consider xx be Element of R such that

         E1: xx = x & ( Class (the InternalRel of R,xx)) c= X;

        reconsider x1 = xx as Element of R1 by A1, b1;

        ( Class (the InternalRel of R1,x1)) c= X1

        proof

          let y be object;

          assume

           F1: y in ( Class (the InternalRel of R1,x1));

          then

          reconsider y1 = y as Element of R1;

           [x1, y1] in the InternalRel of R1 by F1, RELAT_1: 169;

          then [x1, y1] in (the InternalRel of R1 \/ the InternalRel of R2) by XBOOLE_0:def 3;

          then y1 in ( Class (the InternalRel of R,xx)) by A0, RELAT_1: 169;

          hence thesis by E1, A1;

        end;

        then x1 in { x where x be Element of R1 : ( Class (the InternalRel of R1,x)) c= X1 };

        then

         T1: x1 in ( LAp X1) by ROUGHS_1:def 4;

        reconsider x2 = xx as Element of R2 by A1, b1;

        ( Class (the InternalRel of R2,x2)) c= X2

        proof

          let y be object;

          assume

           F1: y in ( Class (the InternalRel of R2,x2));

          then

          reconsider y2 = y as Element of R2;

           [x2, y2] in the InternalRel of R2 by F1, RELAT_1: 169;

          then [x2, y2] in (the InternalRel of R1 \/ the InternalRel of R2) by XBOOLE_0:def 3;

          then y2 in ( Class (the InternalRel of R,xx)) by A0, RELAT_1: 169;

          hence thesis by E1, A1;

        end;

        then x2 in { x where x be Element of R2 : ( Class (the InternalRel of R2,x)) c= X2 };

        then x2 in ( LAp X2) by ROUGHS_1:def 4;

        hence thesis by T1, E1, XBOOLE_0:def 4;

      end;

      (( LAp X1) /\ ( LAp X2)) c= ( LAp X)

      proof

        let x be object;

        assume x in (( LAp X1) /\ ( LAp X2));

        then

         H0: x in ( LAp X1) & x in ( LAp X2) by XBOOLE_0:def 4;

        then x in { x where x be Element of R1 : ( Class (the InternalRel of R1,x)) c= X1 } by ROUGHS_1:def 4;

        then

        consider x1 be Element of R1 such that

         H1: x1 = x & ( Class (the InternalRel of R1,x1)) c= X1;

        x in { x where x be Element of R2 : ( Class (the InternalRel of R2,x)) c= X2 } by H0, ROUGHS_1:def 4;

        then

        consider x2 be Element of R2 such that

         H2: x2 = x & ( Class (the InternalRel of R2,x2)) c= X2;

        reconsider xx = x as Element of R by A1, b1, H1;

        ( Class (the InternalRel of R,xx)) c= X

        proof

          let y be object;

          assume

           S1: y in ( Class (the InternalRel of R,xx));

          then

          reconsider yy = y as Element of R;

           [xx, yy] in the InternalRel of R by S1, RELAT_1: 169;

          then [xx, yy] in the InternalRel of R1 or [xx, yy] in the InternalRel of R2 by A0, XBOOLE_0:def 3;

          then yy in ( Class (the InternalRel of R1,xx)) or yy in ( Class (the InternalRel of R2,xx)) by RELAT_1: 169;

          hence thesis by A1, H2, H1;

        end;

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

        hence thesis by ROUGHS_1:def 4;

      end;

      hence thesis by D1, XBOOLE_0:def 10;

    end;

    theorem :: ROUGHS_3:45

    

     Prop16H: for R1,R2 be non empty RelStr st the carrier of R1 = the carrier of R2 & the InternalRel of R1 c= the InternalRel of R2 holds ( UAp R1) cc= ( UAp R2)

    proof

      let R1,R2 be non empty RelStr;

      assume

       A0: the carrier of R1 = the carrier of R2 & the InternalRel of R1 c= the InternalRel of R2;

      

       a1: ( dom ( UAp R2)) = ( bool the carrier of R2) by FUNCT_2:def 1;

      for x be set st x in ( dom ( UAp R1)) holds (( UAp R1) . x) c= (( UAp R2) . x)

      proof

        let x be set;

        assume

         A2: x in ( dom ( UAp R1));

        then

        reconsider x1 = x as Subset of R1;

        reconsider x2 = x as Subset of R2 by A0, A2;

        

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

        ( UAp x1) c= ( UAp x2)

        proof

          let y be object;

          assume y in ( UAp x1);

          then y in { x where x be Element of R1 : ( Class (the InternalRel of R1,x)) meets x1 } by ROUGHS_1:def 5;

          then

          consider xx be Element of R1 such that

           C1: xx = y & ( Class (the InternalRel of R1,xx)) meets x1;

          reconsider xxx = xx as Element of R2 by A0;

          consider z be object such that

           C2: z in ( Class (the InternalRel of R1,xx)) & z in x1 by C1, XBOOLE_0: 3;

          ( Class (the InternalRel of R1,xx)) c= ( Class (the InternalRel of R2,xx)) by RELAT_1: 124, A0;

          then ( Class (the InternalRel of R2,xx)) meets x2 by C2, XBOOLE_0: 3;

          then xxx in { x where x be Element of R2 : ( Class (the InternalRel of R2,x)) meets x2 };

          hence thesis by C1, ROUGHS_1:def 5;

        end;

        hence thesis by ROUGHS_2:def 11, A4;

      end;

      hence thesis by a1, A0, ALTCAT_2:def 1;

    end;

    theorem :: ROUGHS_3:46

    

     Prop16L: for R1,R2 be non empty RelStr st the carrier of R1 = the carrier of R2 & the InternalRel of R1 c= the InternalRel of R2 holds ( LAp R2) cc= ( LAp R1)

    proof

      let R1,R2 be non empty RelStr;

      assume

       A0: the carrier of R1 = the carrier of R2 & the InternalRel of R1 c= the InternalRel of R2;

      

       A5: ( dom ( LAp R1)) = ( bool the carrier of R1) by FUNCT_2:def 1;

      for x be set st x in ( dom ( LAp R2)) holds (( LAp R2) . x) c= (( LAp R1) . x)

      proof

        let x be set;

        assume

         A2: x in ( dom ( LAp R2));

        then

        reconsider x1 = x as Subset of R1 by A0;

        

         A3: (( LAp R1) . x) = ( LAp x1) by ROUGHS_2:def 10;

        reconsider x2 = x as Subset of R2 by A2;

        ( LAp x2) c= ( LAp x1)

        proof

          let y be object;

          assume y in ( LAp x2);

          then y in { x where x be Element of R2 : ( Class (the InternalRel of R2,x)) c= x2 } by ROUGHS_1:def 4;

          then

          consider xx be Element of R2 such that

           C1: xx = y & ( Class (the InternalRel of R2,xx)) c= x2;

          reconsider xxx = xx as Element of R2;

          ( Class (the InternalRel of R1,xx)) c= ( Class (the InternalRel of R2,xx)) by RELAT_1: 124, A0;

          then

           C2: ( Class (the InternalRel of R1,xx)) c= x1 by C1, XBOOLE_1: 1;

          reconsider xx1 = xx as Element of R1 by A0;

          xx1 in { x where x be Element of R1 : ( Class (the InternalRel of R1,x)) c= x1 } by C2;

          hence thesis by C1, ROUGHS_1:def 4;

        end;

        hence thesis by A3, ROUGHS_2:def 10;

      end;

      hence thesis by A5, A0, ALTCAT_2:def 1;

    end;

    theorem :: ROUGHS_3:47

    for R1,R2,R be non empty RelStr, X be Subset of R, X1 be Subset of R1, X2 be Subset of R2 st R = ( Meet (R1,R2)) & X = X1 & X = X2 & the carrier of R1 = the carrier of R2 holds ( UAp X) c= (( UAp X1) /\ ( UAp X2))

    proof

      let R1,R2,R be non empty RelStr, X be Subset of R, X1 be Subset of R1, X2 be Subset of R2;

      assume

       A1: R = ( Meet (R1,R2)) & X = X1 & X = X2 & the carrier of R1 = the carrier of R2;

      

       SS: the InternalRel of R = (the InternalRel of R1 /\ the InternalRel of R2) by A1, DefMeet;

      

       sz: the carrier of R = (the carrier of R1 /\ the carrier of R2) by A1, DefMeet;

      reconsider XX1 = X as Subset of R1 by A1;

      reconsider XX2 = X as Subset of R2 by A1;

      reconsider XX = X as Subset of R;

      

       zz: ( dom ( UAp R)) = ( bool the carrier of R) by FUNCT_2:def 1;

      ( UAp X) c= (( UAp X1) /\ ( UAp X2))

      proof

        let x be object;

        assume

         S2: x in ( UAp X);

        ( UAp R) cc= ( UAp R1) by Prop16H, SS, sz, A1, XBOOLE_1: 17;

        then (( UAp R) . XX) c= (( UAp R1) . XX1) by zz, ALTCAT_2:def 1;

        then (( UAp R) . XX) c= ( UAp XX1) by ROUGHS_2:def 11;

        then

         hh: ( UAp XX) c= ( UAp XX1) by ROUGHS_2:def 11;

        ( UAp R) cc= ( UAp R2) by Prop16H, A1, SS, XBOOLE_1: 17, sz;

        then (( UAp R) . XX) c= (( UAp R2) . XX2) by zz, ALTCAT_2:def 1;

        then (( UAp R) . XX) c= ( UAp XX2) by ROUGHS_2:def 11;

        then ( UAp XX) c= ( UAp XX2) by ROUGHS_2:def 11;

        hence thesis by hh, XBOOLE_0:def 4, S2, A1;

      end;

      hence thesis;

    end;

    theorem :: ROUGHS_3:48

    for R1,R2,R be non empty RelStr, X be Subset of R, X1 be Subset of R1, X2 be Subset of R2 st R = ( Meet (R1,R2)) & X = X1 & X = X2 & the carrier of R1 = the carrier of R2 holds (( LAp X1) \/ ( LAp X2)) c= ( LAp X)

    proof

      let R1,R2,R be non empty RelStr, X be Subset of R, X1 be Subset of R1, X2 be Subset of R2;

      assume

       A1: R = ( Meet (R1,R2)) & X = X1 & X = X2 & the carrier of R1 = the carrier of R2;

      

       SS: the InternalRel of R = (the InternalRel of R1 /\ the InternalRel of R2) by A1, DefMeet;

      

       sa: ( dom ( LAp R1)) = ( bool the carrier of R1) by FUNCT_2:def 1;

      

       sw: ( dom ( LAp R2)) = ( bool the carrier of R2) by FUNCT_2:def 1;

      

       aa: the carrier of R = (the carrier of R1 /\ the carrier of R2) by A1, DefMeet;

      reconsider XX1 = X as Subset of R1 by A1;

      reconsider XX2 = X as Subset of R2 by A1;

      reconsider XX = X as Subset of R;

      (( LAp X1) \/ ( LAp X2)) c= ( LAp X)

      proof

        let x be object;

        assume x in (( LAp X1) \/ ( LAp X2));

        per cases by XBOOLE_0:def 3;

          suppose

           S2: x in ( LAp X1);

          ( LAp R1) cc= ( LAp R) by aa, A1, Prop16L, SS, XBOOLE_1: 17;

          then (( LAp R1) . XX1) c= (( LAp R) . XX) by sa, ALTCAT_2:def 1;

          then (( LAp R1) . XX1) c= ( LAp XX) by ROUGHS_2:def 10;

          then ( LAp XX1) c= ( LAp XX) by ROUGHS_2:def 10;

          hence thesis by S2, A1;

        end;

          suppose

           S2: x in ( LAp X2);

          ( LAp R2) cc= ( LAp R) by aa, Prop16L, A1, SS, XBOOLE_1: 17;

          then (( LAp R2) . XX2) c= (( LAp R) . XX) by sw, ALTCAT_2:def 1;

          then (( LAp R2) . XX2) c= ( LAp XX) by ROUGHS_2:def 10;

          then ( LAp XX2) c= ( LAp XX) by ROUGHS_2:def 10;

          hence thesis by S2, A1;

        end;

      end;

      hence thesis;

    end;

    theorem :: ROUGHS_3:49

    for R1,R2 be non empty RelStr st the carrier of R1 = the carrier of R2 & ( UAp R1) cc= ( UAp R2) holds the InternalRel of R1 c= the InternalRel of R2 by Prop17A;

    theorem :: ROUGHS_3:50

    for R1,R2 be non empty RelStr st the carrier of R1 = the carrier of R2 & ( UAp R1) = ( UAp R2) holds the InternalRel of R1 = the InternalRel of R2 by Corr3A;

    theorem :: ROUGHS_3:51

    for R1,R2 be non empty RelStr st the carrier of R1 = the carrier of R2 holds ( UAp R1) = ( UAp R2) iff the InternalRel of R1 = the InternalRel of R2 by The5;

    theorem :: ROUGHS_3:52

    for R1,R2 be non empty RelStr st the carrier of R1 = the carrier of R2 & ( LAp R1) cc= ( LAp R2) holds the InternalRel of R2 c= the InternalRel of R1 by Prop18;

    theorem :: ROUGHS_3:53

    

     Corr4: for R1,R2 be non empty RelStr st the carrier of R1 = the carrier of R2 & ( LAp R1) = ( LAp R2) holds the InternalRel of R2 = the InternalRel of R1

    proof

      let R1,R2 be non empty RelStr;

      assume

       A1: the carrier of R1 = the carrier of R2 & ( LAp R1) = ( LAp R2);

      the InternalRel of R2 c= the InternalRel of R1 & the InternalRel of R1 c= the InternalRel of R2 by Prop18, A1;

      hence thesis by XBOOLE_0:def 10;

    end;

    theorem :: ROUGHS_3:54

    for R1,R2 be non empty RelStr st the carrier of R1 = the carrier of R2 holds ( LAp R1) = ( LAp R2) iff the InternalRel of R1 = the InternalRel of R2

    proof

      let R1,R2 be non empty RelStr;

      assume

       A1: the carrier of R1 = the carrier of R2;

      hence ( LAp R1) = ( LAp R2) implies the InternalRel of R1 = the InternalRel of R2 by Corr4;

      assume the InternalRel of R1 = the InternalRel of R2;

      then

       A2: the RelStr of R1 = the RelStr of R2 by A1;

      for x be Subset of R1 holds (( LAp R1) . x) = (( LAp R2) . x)

      proof

        let x be Subset of R1;

        reconsider xx = x as Subset of R2 by A1;

        (( LAp R1) . x) = ( LAp x) by ROUGHS_2:def 10

        .= ( LAp xx) by A2, Pom2

        .= (( LAp R2) . x) by ROUGHS_2:def 10;

        hence thesis;

      end;

      hence thesis by FUNCT_2: 63, A1;

    end;