:: Binary Relations-Based Rough Sets -- An Automated Approach
:: by Adam Grabowski
::
:: Received February 15, 2016
:: Copyright (c) 2016-2021 Association of Mizar Users

registration

let X be non empty set ;

cluster bool X -> d.union-closed ;

coherence
bool X is d.union-closed ;

end;

scheme :: ROUGHS_3:sch 1
FinSubIndA1{ F₁() -> non empty finite set , P₁[ Subset of F₁()] } :

for B being Subset of F₁() holds P₁[B]

provided

A1: P₁[ {} F₁()] and
A2: for B9 being Subset of F₁()
for b being Element of F₁() st P₁[B9] & not b in B9 holds
P₁[B9 \/ {b}]

proof end;

scheme :: ROUGHS_3:sch 2
FinSubIndA2{ F₁() -> non empty finite set , P₁[ Subset of F₁()] } :

for B being non empty Subset of F₁() holds P₁[B]

provided

A1: for x being Element of F₁() holds P₁[{x}] and
A2: for B1, B2 being non empty Subset of F₁() st P₁[B1] & P₁[B2] holds
P₁[B1 \/ B2]

proof 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 )

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} )

proof end;

::: Should be consulted with PCS_0

definition

let R1, R2 be RelStr ;

::: 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
ex b₁ being strict RelStr st
( the carrier of b₁ = the carrier of R1 \/ the carrier of R2 & the InternalRel of b₁ = the InternalRel of R1 \/ the InternalRel of R2 )

proof end;

uniqueness
for b₁, b₂ being strict RelStr st the carrier of b₁ = the carrier of R1 \/ the carrier of R2 & the InternalRel of b₁ = the InternalRel of R1 \/ the InternalRel of R2 & the carrier of b₂ = the carrier of R1 \/ the carrier of R2 & the InternalRel of b₂ = the InternalRel of R1 \/ the InternalRel of R2 holds
b₁ = b₂ ;
commutativity
for b₁ being strict RelStr
for R1, R2 being RelStr st the carrier of b₁ = the carrier of R1 \/ the carrier of R2 & the InternalRel of b₁ = the InternalRel of R1 \/ the InternalRel of R2 holds
( the carrier of b₁ = the carrier of R2 \/ the carrier of R1 & the InternalRel of b₁ = the InternalRel of R2 \/ the InternalRel of R1 ) ;

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
ex b₁ being strict RelStr st
( the carrier of b₁ = the carrier of R1 /\ the carrier of R2 & the InternalRel of b₁ = the InternalRel of R1 /\ the InternalRel of R2 )

proof end;

uniqueness
for b₁, b₂ being strict RelStr st the carrier of b₁ = the carrier of R1 /\ the carrier of R2 & the InternalRel of b₁ = the InternalRel of R1 /\ the InternalRel of R2 & the carrier of b₂ = the carrier of R1 /\ the carrier of R2 & the InternalRel of b₂ = the InternalRel of R1 /\ the InternalRel of R2 holds
b₁ = b₂ ;
commutativity
for b₁ being strict RelStr
for R1, R2 being RelStr st the carrier of b₁ = the carrier of R1 /\ the carrier of R2 & the InternalRel of b₁ = the InternalRel of R1 /\ the InternalRel of R2 holds
( the carrier of b₁ = the carrier of R2 /\ the carrier of R1 & the InternalRel of b₁ = the InternalRel of R2 /\ the InternalRel of R1 ) ;

end;

:: deftheorem DefUnion defines Union ROUGHS_3:def 1 :
for R1, R2 being RelStr
for b₃ being strict RelStr holds
( b₃ = Union (R1,R2) iff ( the carrier of b₃ = the carrier of R1 \/ the carrier of R2 & the InternalRel of b₃ = the InternalRel of R1 \/ the InternalRel of R2 ) );

:: deftheorem DefMeet defines Meet ROUGHS_3:def 2 :
for R1, R2 being RelStr
for b₃ being strict RelStr holds
( b₃ = Meet (R1,R2) iff ( the carrier of b₃ = the carrier of R1 /\ the carrier of R2 & the InternalRel of b₃ = the InternalRel of R1 /\ the InternalRel of R2 ) );

registration

let R1 be RelStr ;
let R2 be non empty RelStr ;

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

coherence
not Union (R1,R2) is empty

proof end;

end;

registration

let A be set ;

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

existence
ex b₁ being Function of (bool A),(bool A) st
( b₁ is /\-preserving & b₁ is \/-preserving )

proof end;

end;

registration

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

cluster Flip f -> \/-preserving ;

coherence
Flip f is \/-preserving

proof end;

end;

registration

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

cluster Flip f -> /\-preserving ;

coherence
Flip f is /\-preserving

proof end;

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

proof end;

registration

cluster non empty transitive mediate for RelStr ;

existence
ex b₁ being RelStr st
( not b₁ is empty & b₁ is mediate & b₁ is transitive )

proof end;

end;

registration

let R be total mediate RelStr ;

cluster the InternalRel of R -> mediate ;

coherence
the InternalRel of R is mediate

proof end;

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

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

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

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}

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)

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)

proof end;

theorem UApEmpty: :: ROUGHS_3:10

for R being non empty RelStr holds (UAp R) . {} = {}

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

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

proof end;

definition

let R be non empty RelStr ;
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
ex b₁ being Relation of the carrier of R st
for x, y being Element of R holds
( [x,y] in b₁ iff x in H . {y} )

proof end;

uniqueness
for b₁, b₂ being Relation of the carrier of R st ( for x, y being Element of R holds
( [x,y] in b₁ iff x in H . {y} ) ) & ( for x, y being Element of R holds
( [x,y] in b₂ iff x in H . {y} ) ) holds
b₁ = b₂

proof end;

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₃ being Relation of the carrier of R holds
( b₃ = GeneratedRelation (R,H) iff for x, y being Element of R holds
( [x,y] in b₃ iff x in H . {y} ) );

definition

let R be non empty RelStr ;
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)) #) is RelStr ;

end;

:: 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)) #);

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
not GeneratedRelStr H is empty ;

end;

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

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} ) ) ) )

proof end;

theorem Th95L: :: ROUGHS_3:15

for R being non empty transitive RelStr
for X being Subset of R holds LAp X c= LAp (LAp X)

proof end;

theorem Th95H: :: ROUGHS_3:16

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

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 )

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 )

proof end;

theorem :: ROUGHS_3:19

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

proof end;

theorem :: ROUGHS_3:20

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

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 )

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 )

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))

definition

let X be set ;
let R be Relation of X;

pred R is_positive_alliance_in X means :: ROUGHS_3:def 5
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 );

pred R is_negative_alliance_in X means :: ROUGHS_3:def 6
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;

end;

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

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

definition

let X be set ;
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 );

end;

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

definition

let R be non empty RelStr ;

attr R is positive_alliance means :DefPA: :: ROUGHS_3:def 8
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;

attr R is alliance means :: ROUGHS_3:def 10
the InternalRel of R is_alliance_in the carrier of R;

end;

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

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

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

registration

cluster non empty reflexive -> non empty positive_alliance for RelStr ;

coherence
for b₁ being non empty RelStr st b₁ is reflexive holds
b₁ is positive_alliance

proof end;

cluster non empty discrete -> non empty negative_alliance for RelStr ;

coherence
for b₁ being non empty RelStr st b₁ is discrete holds
b₁ is negative_alliance

proof end;

end;

registration

cluster non empty positive_alliance negative_alliance for RelStr ;

existence
ex b₁ being non empty RelStr st
( b₁ is positive_alliance & b₁ is negative_alliance )

proof end;

end;

registration

cluster non empty alliance -> non empty positive_alliance negative_alliance for RelStr ;

coherence
for b₁ being non empty RelStr st b₁ is alliance holds
( b₁ is positive_alliance & b₁ is negative_alliance )

proof end;

cluster non empty positive_alliance negative_alliance -> non empty alliance for RelStr ;

coherence
for b₁ being non empty RelStr st b₁ is positive_alliance & b₁ is negative_alliance holds
b₁ is alliance

proof end;

end;

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

registration

cluster non empty positive_alliance -> non empty serial for RelStr ;

coherence
for b₁ being non empty RelStr st b₁ is positive_alliance holds
b₁ is serial

proof end;

cluster non empty transitive serial -> non empty positive_alliance for RelStr ;

coherence
for b₁ being non empty RelStr st b₁ is transitive & b₁ is serial holds
b₁ is positive_alliance

proof end;

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 ;

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 ;

theorem :: ROUGHS_3:25

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 alliance holds
L2 is alliance ;

definition

let R be non empty RelStr ;

attr R is satisfying(7H') means :: ROUGHS_3:def 11
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) ` ;

end;

:: 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) `) );

:: 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) ` );

theorem Sat7Sat: :: ROUGHS_3:26

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

proof end;

theorem Sat7Serial: :: ROUGHS_3:27

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

proof end;

theorem :: ROUGHS_3:28

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

registration

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

coherence
for b₁ being non empty finite RelStr st b₁ is satisfying(7H') holds
b₁ is serial by Sat7Serial;

end;

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) `)

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) `

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) `)

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) `)

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}) `)

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)`);

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 )

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 )

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}) `

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) `

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) `)

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 )

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 )

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 )

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 )

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)

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)

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

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

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)

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

proof end;

theorem :: ROUGHS_3:49

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 by Prop17A;

theorem :: ROUGHS_3:50

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 by Corr3A;

theorem :: ROUGHS_3:51

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 ) by The5;

theorem :: ROUGHS_3:52

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 by Prop18;

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

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 )

proof end;