:: by Adam Grabowski

::

:: Received February 15, 2016

:: Copyright (c) 2016-2018 Association of Mizar Users

registration
end;

theorem Th21: :: ROUGHS_3:1

for f being Function st dom f is subset-closed & dom f is d.union-closed & f is d.union-distributive holds

for a, y being set st a in dom f & y in f . a holds

ex b being set st

( b is finite & b c= a & y in f . b )

for a, y being set st a in dom f & y in f . a holds

ex b being set st

( b is finite & b c= a & y in f . b )

proof end;

theorem KeyLemma: :: ROUGHS_3:2

for f being Function st dom f is subset-closed & f is union-distributive & dom f is d.union-closed holds

for a, y being set st a in dom f & y in f . a holds

ex x being set st

( x in a & y in f . {x} )

for a, y being set st a in dom f & y in f . a holds

ex x being set st

( x in a & y in f . {x} )

proof end;

::: Should be consulted with PCS_0

definition

let R1, R2 be RelStr ;

ex b_{1} being strict RelStr st

( the carrier of b_{1} = the carrier of R1 \/ the carrier of R2 & the InternalRel of b_{1} = the InternalRel of R1 \/ the InternalRel of R2 )

for b_{1}, b_{2} being strict RelStr st the carrier of b_{1} = the carrier of R1 \/ the carrier of R2 & the InternalRel of b_{1} = the InternalRel of R1 \/ the InternalRel of R2 & the carrier of b_{2} = the carrier of R1 \/ the carrier of R2 & the InternalRel of b_{2} = the InternalRel of R1 \/ the InternalRel of R2 holds

b_{1} = b_{2}
;

commutativity

for b_{1} being strict RelStr

for R1, R2 being RelStr st the carrier of b_{1} = the carrier of R1 \/ the carrier of R2 & the InternalRel of b_{1} = the InternalRel of R1 \/ the InternalRel of R2 holds

( the carrier of b_{1} = the carrier of R2 \/ the carrier of R1 & the InternalRel of b_{1} = the InternalRel of R2 \/ the InternalRel of R1 )
;

ex b_{1} being strict RelStr st

( the carrier of b_{1} = the carrier of R1 /\ the carrier of R2 & the InternalRel of b_{1} = the InternalRel of R1 /\ the InternalRel of R2 )

for b_{1}, b_{2} being strict RelStr st the carrier of b_{1} = the carrier of R1 /\ the carrier of R2 & the InternalRel of b_{1} = the InternalRel of R1 /\ the InternalRel of R2 & the carrier of b_{2} = the carrier of R1 /\ the carrier of R2 & the InternalRel of b_{2} = the InternalRel of R1 /\ the InternalRel of R2 holds

b_{1} = b_{2}
;

commutativity

for b_{1} being strict RelStr

for R1, R2 being RelStr st the carrier of b_{1} = the carrier of R1 /\ the carrier of R2 & the InternalRel of b_{1} = the InternalRel of R1 /\ the InternalRel of R2 holds

( the carrier of b_{1} = the carrier of R2 /\ the carrier of R1 & the InternalRel of b_{1} = the InternalRel of R2 /\ the InternalRel of R1 )
;

end;
::: Should be consulted with PCS_0

func Union (R1,R2) -> strict RelStr means :DefUnion: :: ROUGHS_3:def 1

( 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 ( the carrier of it = the carrier of R1 \/ the carrier of R2 & the InternalRel of it = the InternalRel of R1 \/ the InternalRel of R2 );

ex b

( the carrier of b

proof end;

uniqueness for b

b

commutativity

for b

for R1, R2 being RelStr st the carrier of b

( the carrier of b

func Meet (R1,R2) -> strict RelStr means :DefMeet: :: ROUGHS_3:def 2

( 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 ( the carrier of it = the carrier of R1 /\ the carrier of R2 & the InternalRel of it = the InternalRel of R1 /\ the InternalRel of R2 );

ex b

( the carrier of b

proof end;

uniqueness for b

b

commutativity

for b

for R1, R2 being RelStr st the carrier of b

( the carrier of b

:: deftheorem DefUnion defines Union ROUGHS_3:def 1 :

for R1, R2 being RelStr

for b_{3} being strict RelStr holds

( b_{3} = Union (R1,R2) iff ( the carrier of b_{3} = the carrier of R1 \/ the carrier of R2 & the InternalRel of b_{3} = the InternalRel of R1 \/ the InternalRel of R2 ) );

for R1, R2 being RelStr

for b

( b

:: deftheorem DefMeet defines Meet ROUGHS_3:def 2 :

for R1, R2 being RelStr

for b_{3} being strict RelStr holds

( b_{3} = Meet (R1,R2) iff ( the carrier of b_{3} = the carrier of R1 /\ the carrier of R2 & the InternalRel of b_{3} = the InternalRel of R1 /\ the InternalRel of R2 ) );

for R1, R2 being RelStr

for b

( b

registration
end;

registration

let A be set ;

ex b_{1} being Function of (bool A),(bool A) st

( b_{1} is /\-preserving & b_{1} is \/-preserving )

end;
cluster non empty Relation-like bool A -defined bool A -valued Function-like V25( bool A) quasi_total \/-preserving /\-preserving for Function of ,;

existence ex b

( b

proof end;

registration

let A be set ;

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

coherence

Flip f is \/-preserving

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

coherence

Flip f is \/-preserving

proof end;

registration

let A be set ;

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

coherence

Flip f is /\-preserving

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

coherence

Flip f is /\-preserving

proof end;

theorem FlipCC: :: ROUGHS_3:3

for A being non empty set

for f, g being Function of (bool A),(bool A) st f cc= g holds

Flip g cc= Flip f

for f, g being Function of (bool A),(bool A) st f cc= g holds

Flip g cc= Flip f

proof end;

registration

existence

ex b_{1} being RelStr st

( not b_{1} is empty & b_{1} is mediate & b_{1} is transitive )

end;
ex b

( not b

proof end;

registration
end;

theorem Th13: :: ROUGHS_3:4

for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is mediate holds

L2 is mediate

L2 is mediate

proof end;

theorem NatDay: :: ROUGHS_3:5

for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is serial holds

L2 is serial

L2 is serial

proof end;

theorem R224: :: ROUGHS_3:6

for A being non empty set

for L, U being Function of (bool A),(bool A) st U = Flip L & ( for X being Subset of A holds L . X c= L . (L . X) ) holds

for X being Subset of A holds U . (U . X) c= U . X

for L, U being Function of (bool A),(bool A) st U = Flip L & ( for X being Subset of A holds L . X c= L . (L . X) ) holds

for X being Subset of A holds U . (U . X) c= U . X

proof end;

theorem Th5A: :: ROUGHS_3:7

for R being non empty RelStr

for a, b being Element of R st [a,b] in the InternalRel of R holds

a in UAp {b}

for a, b being Element of R st [a,b] in the InternalRel of R holds

a in UAp {b}

proof end;

UApCon: for R being non empty RelStr

for X, Y being Subset of R holds UAp (X /\ Y) c= (UAp X) /\ (UAp Y)

proof end;

theorem UApAdditive: :: ROUGHS_3:8

for R being non empty RelStr

for A, B being Subset of R holds (UAp R) . (A \/ B) = ((UAp R) . A) \/ ((UAp R) . B)

for A, B being Subset of R holds (UAp R) . (A \/ B) = ((UAp R) . A) \/ ((UAp R) . B)

proof end;

theorem :: ROUGHS_3:9

for R being non empty RelStr

for A, B being Subset of R holds (LAp R) . (A /\ B) = ((LAp R) . A) /\ ((LAp R) . B)

for A, B being Subset of R holds (LAp R) . (A /\ B) = ((LAp R) . A) /\ ((LAp R) . B)

proof end;

theorem Pom1: :: ROUGHS_3:11

for R1, R2 being non empty RelStr

for X being Subset of R1

for Y being Subset of R2 st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) & X = Y holds

UAp X = UAp Y

for X being Subset of R1

for Y being Subset of R2 st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) & X = Y holds

UAp X = UAp Y

proof end;

theorem Pom2: :: ROUGHS_3:12

for R1, R2 being non empty RelStr

for X being Subset of R1

for Y being Subset of R2 st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) & X = Y holds

LAp X = LAp Y

for X being Subset of R1

for Y being Subset of R2 st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) & X = Y holds

LAp X = LAp Y

proof end;

definition

let R be non empty RelStr ;

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

ex b_{1} being Relation of the carrier of R st

for x, y being Element of R holds

( [x,y] in b_{1} iff x in H . {y} )

for b_{1}, b_{2} being Relation of the carrier of R st ( for x, y being Element of R holds

( [x,y] in b_{1} iff x in H . {y} ) ) & ( for x, y being Element of R holds

( [x,y] in b_{2} iff x in H . {y} ) ) holds

b_{1} = b_{2}

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

func GeneratedRelation (R,H) -> Relation of the carrier of R means :GRDef: :: ROUGHS_3:def 3

for x, y being Element of R holds

( [x,y] in it iff x in H . {y} );

existence for x, y being Element of R holds

( [x,y] in it iff x in H . {y} );

ex b

for x, y being Element of R holds

( [x,y] in b

proof end;

uniqueness for b

( [x,y] in b

( [x,y] in b

b

proof end;

:: deftheorem GRDef defines GeneratedRelation ROUGHS_3:def 3 :

for R being non empty RelStr

for H being Function of (bool the carrier of R),(bool the carrier of R)

for b_{3} being Relation of the carrier of R holds

( b_{3} = GeneratedRelation (R,H) iff for x, y being Element of R holds

( [x,y] in b_{3} iff x in H . {y} ) );

for R being non empty RelStr

for H being Function of (bool the carrier of R),(bool the carrier of R)

for b

( b

( [x,y] in b

definition

let R be non empty RelStr ;

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

RelStr(# the carrier of R,(GeneratedRelation (R,H)) #) is RelStr ;

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

func GeneratedRelStr H -> RelStr equals :: ROUGHS_3:def 4

RelStr(# the carrier of R,(GeneratedRelation (R,H)) #);

coherence RelStr(# the carrier of R,(GeneratedRelation (R,H)) #);

RelStr(# the carrier of R,(GeneratedRelation (R,H)) #) is RelStr ;

:: deftheorem defines GeneratedRelStr ROUGHS_3:def 4 :

for R being non empty RelStr

for H being Function of (bool the carrier of R),(bool the carrier of R) holds GeneratedRelStr H = RelStr(# the carrier of R,(GeneratedRelation (R,H)) #);

for R being non empty RelStr

for H being Function of (bool the carrier of R),(bool the carrier of R) holds GeneratedRelStr H = RelStr(# the carrier of R,(GeneratedRelation (R,H)) #);

registration

let R be non empty RelStr ;

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

coherence

not GeneratedRelStr H is empty ;

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

coherence

not GeneratedRelStr H is empty ;

theorem KeyTheorem: :: ROUGHS_3:13

for R being non empty finite RelStr

for H being Function of (bool the carrier of R),(bool the carrier of R) st H . {} = {} & H is \/-preserving holds

UAp (GeneratedRelStr H) = H

for H being Function of (bool the carrier of R),(bool the carrier of R) st H . {} = {} & H is \/-preserving holds

UAp (GeneratedRelStr H) = H

proof end;

theorem YaoTh3: :: ROUGHS_3:14

for A being non empty finite set

for L, H being Function of (bool A),(bool A) st L = Flip H holds

( ( H . {} = {} & ( for X, Y being Subset of A holds H . (X \/ Y) = (H . X) \/ (H . Y) ) ) iff ex R being non empty finite RelStr st

( the carrier of R = A & LAp R = L & UAp R = H & ( for x, y being Element of R holds

( [x,y] in the InternalRel of R iff x in H . {y} ) ) ) )

for L, H being Function of (bool A),(bool A) st L = Flip H holds

( ( H . {} = {} & ( for X, Y being Subset of A holds H . (X \/ Y) = (H . X) \/ (H . Y) ) ) iff ex R being non empty finite RelStr st

( the carrier of R = A & LAp R = L & UAp R = H & ( for x, y being Element of R holds

( [x,y] in the InternalRel of R iff x in H . {y} ) ) ) )

proof end;

theorem ThProposition9: :: ROUGHS_3:17

for A being non empty finite set

for L being Function of (bool A),(bool A) st L . A = A & ( for X being Subset of A holds L . X c= L . (L . X) ) & ( for X, Y being Subset of A holds L . (X /\ Y) = (L . X) /\ (L . Y) ) holds

ex R being non empty finite transitive RelStr st

( the carrier of R = A & L = LAp R )

for L being Function of (bool A),(bool A) st L . A = A & ( for X being Subset of A holds L . X c= L . (L . X) ) & ( for X, Y being Subset of A holds L . (X /\ Y) = (L . X) /\ (L . Y) ) holds

ex R being non empty finite transitive RelStr st

( the carrier of R = A & L = LAp R )

proof end;

theorem ThProposition9U: :: ROUGHS_3:18

for A being non empty finite set

for U being Function of (bool A),(bool A) st U . {} = {} & ( for X being Subset of A holds U . (U . X) c= U . X ) & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) holds

ex R being non empty finite transitive RelStr st

( the carrier of R = A & U = UAp R )

for U being Function of (bool A),(bool A) st U . {} = {} & ( for X being Subset of A holds U . (U . X) c= U . X ) & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) holds

ex R being non empty finite transitive RelStr st

( the carrier of R = A & U = UAp R )

proof end;

Prop17A: for R1, R2 being 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 end;

Corr3A: for R1, R2 being 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 end;

theorem :: ROUGHS_3:21

for A being non empty finite set

for L being Function of (bool A),(bool A) st L . A = A & ( for X being Subset of A holds L . X = L . (L . X) ) & ( for X, Y being Subset of A holds L . (X /\ Y) = (L . X) /\ (L . Y) ) holds

ex R being non empty finite transitive mediate RelStr st

( the carrier of R = A & L = LAp R )

for L being Function of (bool A),(bool A) st L . A = A & ( for X being Subset of A holds L . X = L . (L . X) ) & ( for X, Y being Subset of A holds L . (X /\ Y) = (L . X) /\ (L . Y) ) holds

ex R being non empty finite transitive mediate RelStr st

( the carrier of R = A & L = LAp R )

proof end;

theorem :: ROUGHS_3:22

for A being non empty finite set

for U being Function of (bool A),(bool A) st U . {} = {} & ( for X being Subset of A holds U . (U . X) = U . X ) & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) holds

ex R being non empty finite transitive mediate RelStr st

( the carrier of R = A & U = UAp R )

for U being Function of (bool A),(bool A) st U . {} = {} & ( for X being Subset of A holds U . (U . X) = U . X ) & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) holds

ex R being non empty finite transitive mediate RelStr st

( the carrier of R = A & U = UAp R )

proof end;

:: (7L) L(-L(X)) = -L(X)

:: (7L') L(-L(X)) c= -L(X)

:: (7L") -L(X) c= L(-L(X))

:: (7H) H(-H(X)) = -H(X)

:: (7H') H(-H(X)) c= -H(X)

:: (7H") -H(X) c= H(-H(X))

:: (7L') L(-L(X)) c= -L(X)

:: (7L") -L(X) c= L(-L(X))

:: (7H) H(-H(X)) = -H(X)

:: (7H') H(-H(X)) c= -H(X)

:: (7H") -H(X) c= H(-H(X))

definition

let X be set ;

let R be Relation of X;

end;
let R be Relation of X;

:: deftheorem defines is_positive_alliance_in ROUGHS_3:def 5 :

for X being set

for R being Relation of X holds

( R is_positive_alliance_in X iff for x, y being object st x in X & y in X & not [x,y] in R holds

ex z being object st

( z in X & [x,z] in R & not [z,y] in R ) );

for X being set

for R being Relation of X holds

( R is_positive_alliance_in X iff for x, y being object st x in X & y in X & not [x,y] in R holds

ex z being object st

( z in X & [x,z] in R & not [z,y] in R ) );

:: deftheorem defines is_negative_alliance_in ROUGHS_3:def 6 :

for X being set

for R being Relation of X holds

( R is_negative_alliance_in X iff for x, y being object st x in X & y in X & ex z being object st

( z in X & [x,z] in R & not [z,y] in R ) holds

not [x,y] in R );

for X being set

for R being Relation of X holds

( R is_negative_alliance_in X iff for x, y being object st x in X & y in X & ex z being object st

( z in X & [x,z] in R & not [z,y] in R ) holds

not [x,y] in R );

definition

let X be set ;

let R be Relation of X;

end;
let R be Relation of X;

pred R is_alliance_in X means :: ROUGHS_3:def 7

( R is_negative_alliance_in X & R is_positive_alliance_in X );

( R is_negative_alliance_in X & R is_positive_alliance_in X );

:: deftheorem defines is_alliance_in ROUGHS_3:def 7 :

for X being set

for R being Relation of X holds

( R is_alliance_in X iff ( R is_negative_alliance_in X & R is_positive_alliance_in X ) );

for X being set

for R being Relation of X holds

( R is_alliance_in X iff ( R is_negative_alliance_in X & R is_positive_alliance_in X ) );

definition

let R be non empty RelStr ;

end;
attr R is positive_alliance means :DefPA: :: ROUGHS_3:def 8

the InternalRel of R is_positive_alliance_in the carrier of R;

the InternalRel of R is_positive_alliance_in the carrier of R;

attr R is negative_alliance means :DefNA: :: ROUGHS_3:def 9

the InternalRel of R is_negative_alliance_in the carrier of R;

the InternalRel of R is_negative_alliance_in the carrier of R;

:: deftheorem DefPA defines positive_alliance ROUGHS_3:def 8 :

for R being non empty RelStr holds

( R is positive_alliance iff the InternalRel of R is_positive_alliance_in the carrier of R );

for R being non empty RelStr holds

( R is positive_alliance iff the InternalRel of R is_positive_alliance_in the carrier of R );

:: deftheorem DefNA defines negative_alliance ROUGHS_3:def 9 :

for R being non empty RelStr holds

( R is negative_alliance iff the InternalRel of R is_negative_alliance_in the carrier of R );

for R being non empty RelStr holds

( R is negative_alliance iff the InternalRel of R is_negative_alliance_in the carrier of R );

:: deftheorem defines alliance ROUGHS_3:def 10 :

for R being non empty RelStr holds

( R is alliance iff the InternalRel of R is_alliance_in the carrier of R );

for R being non empty RelStr holds

( R is alliance iff the InternalRel of R is_alliance_in the carrier of R );

registration

coherence

for b_{1} being non empty RelStr st b_{1} is reflexive holds

b_{1} is positive_alliance

for b_{1} being non empty RelStr st b_{1} is discrete holds

b_{1} is negative_alliance

end;
for b

b

proof end;

coherence for b

b

proof end;

registration

existence

ex b_{1} being non empty RelStr st

( b_{1} is positive_alliance & b_{1} is negative_alliance )

end;
ex b

( b

proof end;

registration

coherence

for b_{1} being non empty RelStr st b_{1} is alliance holds

( b_{1} is positive_alliance & b_{1} is negative_alliance )

for b_{1} being non empty RelStr st b_{1} is positive_alliance & b_{1} is negative_alliance holds

b_{1} is alliance

end;
for b

( b

proof end;

coherence for b

b

proof end;

:: But soon we realized a more general proof can be provided

registration

coherence

for b_{1} being non empty RelStr st b_{1} is positive_alliance holds

b_{1} is serial

for b_{1} being non empty RelStr st b_{1} is transitive & b_{1} is serial holds

b_{1} is positive_alliance

end;
for b

b

proof end;

coherence for b

b

proof end;

theorem NegReg: :: ROUGHS_3:23

for L1, L2 being non empty RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is negative_alliance holds

L2 is negative_alliance ;

L2 is negative_alliance ;

theorem PosReg: :: ROUGHS_3:24

for L1, L2 being non empty RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is positive_alliance holds

L2 is positive_alliance ;

L2 is positive_alliance ;

theorem :: ROUGHS_3:25

definition

let R be non empty RelStr ;

end;
attr R is satisfying(7H') means :: ROUGHS_3:def 11

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

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

attr R is satisfying(7L') means :: ROUGHS_3:def 12

for X being Subset of R holds LAp ((LAp X) `) c= (LAp X) ` ;

for X being Subset of R holds LAp ((LAp X) `) c= (LAp X) ` ;

:: deftheorem defines satisfying(7H') ROUGHS_3:def 11 :

for R being non empty RelStr holds

( R is satisfying(7H') iff for X being Subset of R holds (UAp X) ` c= UAp ((UAp X) `) );

for R being non empty RelStr holds

( R is satisfying(7H') iff for X being Subset of R holds (UAp X) ` c= UAp ((UAp X) `) );

:: deftheorem defines satisfying(7L') ROUGHS_3:def 12 :

for R being non empty RelStr holds

( R is satisfying(7L') iff for X being Subset of R holds LAp ((LAp X) `) c= (LAp X) ` );

for R being non empty RelStr holds

( R is satisfying(7L') iff for X being Subset of R holds LAp ((LAp X) `) c= (LAp X) ` );

theorem :: ROUGHS_3:28

for R being non empty finite RelStr st R is satisfying(7L') holds

R is serial by Sat7Serial, Sat7Sat;

R is serial by Sat7Serial, Sat7Sat;

registration

coherence

for b_{1} being non empty finite RelStr st b_{1} is satisfying(7H') holds

b_{1} is serial
by Sat7Serial;

end;
for b

b

theorem Conv: :: ROUGHS_3:29

for R being non empty RelStr st ( for X being Subset of R holds UAp ((UAp X) `) c= (UAp X) ` ) holds

for X being Subset of R holds (LAp X) ` c= LAp ((LAp X) `)

for X being Subset of R holds (LAp X) ` c= LAp ((LAp X) `)

proof end;

theorem Conv2: :: ROUGHS_3:30

for A being non empty set

for L, U being Function of (bool A),(bool A) st U = Flip L & ( for X being Subset of A holds (L . X) ` c= L . ((L . X) `) ) holds

for X being Subset of A holds U . ((U . X) `) c= (U . X) `

for L, U being Function of (bool A),(bool A) st U = Flip L & ( for X being Subset of A holds (L . X) ` c= L . ((L . X) `) ) holds

for X being Subset of A holds U . ((U . X) `) c= (U . X) `

proof end;

theorem Conv3: :: ROUGHS_3:31

for A being non empty set

for L, U being Function of (bool A),(bool A) st U = Flip L & ( for X being Subset of A holds U . ((U . X) `) c= (U . X) ` ) holds

for X being Subset of A holds (L . X) ` c= L . ((L . X) `)

for L, U being Function of (bool A),(bool A) st U = Flip L & ( for X being Subset of A holds U . ((U . X) `) c= (U . X) ` ) holds

for X being Subset of A holds (L . X) ` c= L . ((L . X) `)

proof end;

theorem Conv4: :: ROUGHS_3:32

for A being non empty set

for L, U being Function of (bool A),(bool A) st U = Flip L & ( for X being Subset of A holds L . ((L . X) `) c= (L . X) ` ) holds

for X being Subset of A holds (U . X) ` c= U . ((U . X) `)

for L, U being Function of (bool A),(bool A) st U = Flip L & ( for X being Subset of A holds L . ((L . X) `) c= (L . X) ` ) holds

for X being Subset of A holds (U . X) ` c= U . ((U . X) `)

proof end;

theorem :: ROUGHS_3:33

for R being non empty finite positive_alliance RelStr

for x being Element of R holds ((UAp R) . {x}) ` c= (UAp R) . (((UAp R) . {x}) `)

for x being Element of R holds ((UAp R) . {x}) ` c= (UAp R) . (((UAp R) . {x}) `)

proof end;

::theorem :: Proposition 10 (7H') general case - FAILED

:: for R being finite positive_alliance non empty RelStr,

:: X being Subset of R holds

:: ((UAp R).X)` c= (UAp R).(((UAp R).X)`);

:: for R being finite positive_alliance non empty RelStr,

:: X being Subset of R holds

:: ((UAp R).X)` c= (UAp R).(((UAp R).X)`);

theorem Prop11: :: ROUGHS_3:34

for A being non empty finite set

for U being Function of (bool A),(bool A) st U . {} = {} & ( for X being Subset of A holds (U . X) ` c= U . ((U . X) `) ) & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) holds

ex R being non empty finite positive_alliance RelStr st

( the carrier of R = A & U = UAp R )

for U being Function of (bool A),(bool A) st U . {} = {} & ( for X being Subset of A holds (U . X) ` c= U . ((U . X) `) ) & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) holds

ex R being non empty finite positive_alliance RelStr st

( the carrier of R = A & U = UAp R )

proof end;

theorem :: ROUGHS_3:35

for A being non empty finite set

for L being Function of (bool A),(bool A) st L . A = A & ( for X being Subset of A holds L . ((L . X) `) c= (L . X) ` ) & ( for X, Y being Subset of A holds L . (X /\ Y) = (L . X) /\ (L . Y) ) holds

ex R being non empty finite positive_alliance RelStr st

( the carrier of R = A & L = LAp R )

for L being Function of (bool A),(bool A) st L . A = A & ( for X being Subset of A holds L . ((L . X) `) c= (L . X) ` ) & ( for X, Y being Subset of A holds L . (X /\ Y) = (L . X) /\ (L . Y) ) holds

ex R being non empty finite positive_alliance RelStr st

( the carrier of R = A & L = LAp R )

proof end;

theorem Prop137H: :: ROUGHS_3:36

for R being non empty finite negative_alliance RelStr

for x being Element of R holds (UAp R) . (((UAp R) . {x}) `) c= ((UAp R) . {x}) `

for x being Element of R holds (UAp R) . (((UAp R) . {x}) `) c= ((UAp R) . {x}) `

proof end;

theorem Prop13H: :: ROUGHS_3:37

for R being non empty finite negative_alliance RelStr

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

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

proof end;

theorem :: ROUGHS_3:38

for R being non empty finite negative_alliance RelStr

for X being Subset of R holds (LAp X) ` c= LAp ((LAp X) `)

for X being Subset of R holds (LAp X) ` c= LAp ((LAp X) `)

proof end;

theorem Prop14: :: ROUGHS_3:39

for A being non empty finite set

for U being Function of (bool A),(bool A) st U . {} = {} & ( for X being Subset of A holds U . ((U . X) `) c= (U . X) ` ) & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) holds

ex R being non empty finite negative_alliance RelStr st

( the carrier of R = A & U = UAp R )

for U being Function of (bool A),(bool A) st U . {} = {} & ( for X being Subset of A holds U . ((U . X) `) c= (U . X) ` ) & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) holds

ex R being non empty finite negative_alliance RelStr st

( the carrier of R = A & U = UAp R )

proof end;

theorem :: ROUGHS_3:40

for A being non empty finite set

for L being Function of (bool A),(bool A) st L . A = A & ( for X being Subset of A holds (L . X) ` c= L . ((L . X) `) ) & ( for X, Y being Subset of A holds L . (X /\ Y) = (L . X) /\ (L . Y) ) holds

ex R being non empty finite negative_alliance RelStr st

( the carrier of R = A & L = LAp R )

for L being Function of (bool A),(bool A) st L . A = A & ( for X being Subset of A holds (L . X) ` c= L . ((L . X) `) ) & ( for X, Y being Subset of A holds L . (X /\ Y) = (L . X) /\ (L . Y) ) holds

ex R being non empty finite negative_alliance RelStr st

( the carrier of R = A & L = LAp R )

proof end;

Prop18: for R1, R2 being 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 end;

The5: for R1, R2 being 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 end;

:: Theorem 2 (7H) left without a proof

theorem Th2H: :: ROUGHS_3:41

for A being non empty finite set

for U being Function of (bool A),(bool A) st U . {} = {} & ( for X being Subset of A holds U . ((U . X) `) = (U . X) ` ) & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) holds

ex R being non empty finite alliance RelStr st

( the carrier of R = A & U = UAp R )

for U being Function of (bool A),(bool A) st U . {} = {} & ( for X being Subset of A holds U . ((U . X) `) = (U . X) ` ) & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) holds

ex R being non empty finite alliance RelStr st

( the carrier of R = A & U = UAp R )

proof end;

theorem :: ROUGHS_3:42

for A being non empty finite set

for L being Function of (bool A),(bool A) st L . A = A & ( for X being Subset of A holds (L . X) ` = L . ((L . X) `) ) & ( for X, Y being Subset of A holds L . (X /\ Y) = (L . X) /\ (L . Y) ) holds

ex R being non empty finite alliance RelStr st

( the carrier of R = A & L = LAp R )

for L being Function of (bool A),(bool A) st L . A = A & ( for X being Subset of A holds (L . X) ` = L . ((L . X) `) ) & ( for X, Y being Subset of A holds L . (X /\ Y) = (L . X) /\ (L . Y) ) holds

ex R being non empty finite alliance RelStr st

( the carrier of R = A & L = LAp R )

proof end;

theorem :: ROUGHS_3:43

for R1, R2, R being non empty RelStr

for X being Subset of R

for X1 being Subset of R1

for X2 being 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)

for X being Subset of R

for X1 being Subset of R1

for X2 being 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 end;

theorem :: ROUGHS_3:44

for R1, R2, R being non empty RelStr

for X being Subset of R

for X1 being Subset of R1

for X2 being 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)

for X being Subset of R

for X1 being Subset of R1

for X2 being 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 end;

theorem Prop16H: :: ROUGHS_3:45

for R1, R2 being 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

UAp R1 cc= UAp R2

proof end;

theorem Prop16L: :: ROUGHS_3:46

for R1, R2 being 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

LAp R2 cc= LAp R1

proof end;

theorem :: ROUGHS_3:47

for R1, R2, R being non empty RelStr

for X being Subset of R

for X1 being Subset of R1

for X2 being 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)

for X being Subset of R

for X1 being Subset of R1

for X2 being 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 end;

theorem :: ROUGHS_3:48

for R1, R2, R being non empty RelStr

for X being Subset of R

for X1 being Subset of R1

for X2 being 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

for X being Subset of R

for X1 being Subset of R1

for X2 being 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 end;

theorem :: ROUGHS_3:49

theorem :: ROUGHS_3:50

theorem :: ROUGHS_3:51

theorem :: ROUGHS_3:52

theorem Corr4: :: ROUGHS_3:53

for R1, R2 being 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

the InternalRel of R2 = the InternalRel of R1

proof end;

theorem :: ROUGHS_3:54

for R1, R2 being 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 )

( LAp R1 = LAp R2 iff the InternalRel of R1 = the InternalRel of R2 )

proof end;