:: 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{ F1() -> non empty finite set , P1[ Subset of F1()] } :
for B being Subset of F1() holds P1[B]
provided
A1: P1[ {} F1()] and
A2: for B9 being Subset of F1()
for b being Element of F1() st P1[B9] & not b in B9 holds
P1[B9 \/ {b}]
proof end;

scheme :: ROUGHS_3:sch 2
FinSubIndA2{ F1() -> non empty finite set , P1[ Subset of F1()] } :
for B being non empty Subset of F1() holds P1[B]
provided
A1: for x being Element of F1() holds P1[{x}] and
A2: for B1, B2 being non empty Subset of F1() st P1[B1] & P1[B2] holds
P1[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 b1 being strict RelStr st
( the carrier of b1 = the carrier of R1 \/ the carrier of R2 & the InternalRel of b1 = the InternalRel of R1 \/ the InternalRel of R2 )
proof end;
uniqueness
for b1, b2 being strict RelStr st the carrier of b1 = the carrier of R1 \/ the carrier of R2 & the InternalRel of b1 = the InternalRel of R1 \/ the InternalRel of R2 & the carrier of b2 = the carrier of R1 \/ the carrier of R2 & the InternalRel of b2 = the InternalRel of R1 \/ the InternalRel of R2 holds
b1 = b2
;
commutativity
for b1 being strict RelStr
for R1, R2 being RelStr st the carrier of b1 = the carrier of R1 \/ the carrier of R2 & the InternalRel of b1 = the InternalRel of R1 \/ the InternalRel of R2 holds
( the carrier of b1 = the carrier of R2 \/ the carrier of R1 & the InternalRel of b1 = 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 b1 being strict RelStr st
( the carrier of b1 = the carrier of R1 /\ the carrier of R2 & the InternalRel of b1 = the InternalRel of R1 /\ the InternalRel of R2 )
proof end;
uniqueness
for b1, b2 being strict RelStr st the carrier of b1 = the carrier of R1 /\ the carrier of R2 & the InternalRel of b1 = the InternalRel of R1 /\ the InternalRel of R2 & the carrier of b2 = the carrier of R1 /\ the carrier of R2 & the InternalRel of b2 = the InternalRel of R1 /\ the InternalRel of R2 holds
b1 = b2
;
commutativity
for b1 being strict RelStr
for R1, R2 being RelStr st the carrier of b1 = the carrier of R1 /\ the carrier of R2 & the InternalRel of b1 = the InternalRel of R1 /\ the InternalRel of R2 holds
( the carrier of b1 = the carrier of R2 /\ the carrier of R1 & the InternalRel of b1 = the InternalRel of R2 /\ the InternalRel of R1 )
;
end;

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

:: deftheorem DefMeet defines Meet ROUGHS_3:def 2 :
for R1, R2 being RelStr
for b3 being strict RelStr holds
( b3 = Meet (R1,R2) iff ( the carrier of b3 = the carrier of R1 /\ the carrier of R2 & the InternalRel of b3 = 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 b1 being Function of (bool A),(bool A) st
( b1 is /\-preserving & b1 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 b1 being RelStr st
( not b1 is empty & b1 is mediate & b1 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 b1 being Relation of the carrier of R st
for x, y being Element of R holds
( [x,y] in b1 iff x in H . {y} )
proof end;
uniqueness
for b1, b2 being Relation of the carrier of R st ( for x, y being Element of R holds
( [x,y] in b1 iff x in H . {y} ) ) & ( for x, y being Element of R holds
( [x,y] in b2 iff x in H . {y} ) ) holds
b1 = b2
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 b3 being Relation of the carrier of R holds
( b3 = GeneratedRelation (R,H) iff for x, y being Element of R holds
( [x,y] in b3 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 b1 being non empty RelStr st b1 is reflexive holds
b1 is positive_alliance
proof end;
cluster non empty discrete -> non empty negative_alliance for RelStr ;
coherence
for b1 being non empty RelStr st b1 is discrete holds
b1 is negative_alliance
proof end;
end;

registration
cluster non empty positive_alliance negative_alliance for RelStr ;
existence
ex b1 being non empty RelStr st
( b1 is positive_alliance & b1 is negative_alliance )
proof end;
end;

registration
cluster non empty alliance -> non empty positive_alliance negative_alliance for RelStr ;
coherence
for b1 being non empty RelStr st b1 is alliance holds
( b1 is positive_alliance & b1 is negative_alliance )
proof end;
cluster non empty positive_alliance negative_alliance -> non empty alliance for RelStr ;
coherence
for b1 being non empty RelStr st b1 is positive_alliance & b1 is negative_alliance holds
b1 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 b1 being non empty RelStr st b1 is positive_alliance holds
b1 is serial
proof end;
cluster non empty transitive serial -> non empty positive_alliance for RelStr ;
coherence
for b1 being non empty RelStr st b1 is transitive & b1 is serial holds
b1 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 b1 being non empty finite RelStr st b1 is satisfying(7H') holds
b1 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;