:: On the Lattice of Intervals and Rough Sets
:: by Adam Grabowski and Magdalena Jastrz\c{e}bska
::
:: Received October 10, 2009
:: Copyright (c) 2009-2011 Association of Mizar Users


begin

definition
let U be set ;
let X, Y be Subset of U;
func Inter (X,Y) -> Subset-Family of U equals :: INTERVA1:def 1
{ A where A is Subset of U : ( X c= A & A c= Y ) } ;
coherence
{ A where A is Subset of U : ( X c= A & A c= Y ) } is Subset-Family of U
proof end;
end;

:: deftheorem defines Inter INTERVA1:def 1 :
for U being set
for X, Y being Subset of U holds Inter (X,Y) = { A where A is Subset of U : ( X c= A & A c= Y ) } ;

theorem Th1: :: INTERVA1:1
for U being set
for X, Y being Subset of U
for x being set holds
( x in Inter (X,Y) iff ( X c= x & x c= Y ) )
proof end;

theorem Th2: :: INTERVA1:2
for U being set
for X, Y being Subset of U st Inter (X,Y) <> {} holds
( X in Inter (X,Y) & Y in Inter (X,Y) )
proof end;

theorem Th3: :: INTERVA1:3
for U being set
for A, B being Subset of U st not A c= B holds
Inter (A,B) = {}
proof end;

theorem :: INTERVA1:4
for U being set
for A, B being Subset of U st Inter (A,B) = {} holds
not A c= B by Th1;

theorem Th5: :: INTERVA1:5
for U being set
for A, B being Subset of U st Inter (A,B) <> {} holds
A c= B
proof end;

theorem Th6: :: INTERVA1:6
for U being set
for A, B, C, D being Subset of U st Inter (A,B) <> {} & Inter (A,B) = Inter (C,D) holds
( A = C & B = D )
proof end;

theorem Th7: :: INTERVA1:7
for U being non empty set
for A being non empty Subset of U holds Inter (A,({} U)) = {}
proof end;

theorem Th8: :: INTERVA1:8
for U being set
for A being Subset of U holds Inter (A,A) = {A}
proof end;

definition
let U be set ;
mode IntervalSet of U -> Subset-Family of U means :Def2: :: INTERVA1:def 2
ex A, B being Subset of U st it = Inter (A,B);
existence
ex b1 being Subset-Family of U ex A, B being Subset of U st b1 = Inter (A,B)
proof end;
end;

:: deftheorem Def2 defines IntervalSet INTERVA1:def 2 :
for U being set
for b2 being Subset-Family of U holds
( b2 is IntervalSet of U iff ex A, B being Subset of U st b2 = Inter (A,B) );

theorem :: INTERVA1:9
for U being non empty set holds {} is IntervalSet of U
proof end;

theorem Th10: :: INTERVA1:10
for U being non empty set
for A being Subset of U holds {A} is IntervalSet of U
proof end;

definition
let U be set ;
let A, B be Subset of U;
:: original: Inter
redefine func Inter (A,B) -> IntervalSet of U;
correctness
coherence
Inter (A,B) is IntervalSet of U
;
by Def2;
end;

registration
let U be non empty set ;
cluster non empty IntervalSet of U;
existence
not for b1 being IntervalSet of U holds b1 is empty
proof end;
end;

theorem Th11: :: INTERVA1:11
for U being non empty set
for A being set holds
( A is non empty IntervalSet of U iff ex A1, A2 being Subset of U st
( A1 c= A2 & A = Inter (A1,A2) ) )
proof end;

theorem Th12: :: INTERVA1:12
for U being non empty set
for A1, A2, B1, B2 being Subset of U st A1 c= A2 & B1 c= B2 holds
INTERSECTION ((Inter (A1,A2)),(Inter (B1,B2))) = { C where C is Subset of U : ( A1 /\ B1 c= C & C c= A2 /\ B2 ) }
proof end;

theorem Th13: :: INTERVA1:13
for U being non empty set
for A1, A2, B1, B2 being Subset of U st A1 c= A2 & B1 c= B2 holds
UNION ((Inter (A1,A2)),(Inter (B1,B2))) = { C where C is Subset of U : ( A1 \/ B1 c= C & C c= A2 \/ B2 ) }
proof end;

definition
let U be non empty set ;
let A, B be non empty IntervalSet of U;
func A _/\_ B -> IntervalSet of U equals :: INTERVA1:def 3
INTERSECTION (A,B);
coherence
INTERSECTION (A,B) is IntervalSet of U
proof end;
func A _\/_ B -> IntervalSet of U equals :: INTERVA1:def 4
UNION (A,B);
coherence
UNION (A,B) is IntervalSet of U
proof end;
end;

:: deftheorem defines _/\_ INTERVA1:def 3 :
for U being non empty set
for A, B being non empty IntervalSet of U holds A _/\_ B = INTERSECTION (A,B);

:: deftheorem defines _\/_ INTERVA1:def 4 :
for U being non empty set
for A, B being non empty IntervalSet of U holds A _\/_ B = UNION (A,B);

registration
let U be non empty set ;
let A, B be non empty IntervalSet of U;
cluster A _/\_ B -> non empty ;
coherence
not A _/\_ B is empty
by TOPGEN_4:31;
cluster A _\/_ B -> non empty ;
coherence
not A _\/_ B is empty
by TOPGEN_4:30;
end;

definition
let U be non empty set ;
let A be non empty IntervalSet of U;
func A ``1 -> Subset of U means :Def5: :: INTERVA1:def 5
ex B being Subset of U st A = Inter (it,B);
existence
ex b1, B being Subset of U st A = Inter (b1,B)
proof end;
uniqueness
for b1, b2 being Subset of U st ex B being Subset of U st A = Inter (b1,B) & ex B being Subset of U st A = Inter (b2,B) holds
b1 = b2
by Th6;
func A ``2 -> Subset of U means :Def6: :: INTERVA1:def 6
ex B being Subset of U st A = Inter (B,it);
existence
ex b1, B being Subset of U st A = Inter (B,b1)
proof end;
uniqueness
for b1, b2 being Subset of U st ex B being Subset of U st A = Inter (B,b1) & ex B being Subset of U st A = Inter (B,b2) holds
b1 = b2
by Th6;
end;

:: deftheorem Def5 defines ``1 INTERVA1:def 5 :
for U being non empty set
for A being non empty IntervalSet of U
for b3 being Subset of U holds
( b3 = A ``1 iff ex B being Subset of U st A = Inter (b3,B) );

:: deftheorem Def6 defines ``2 INTERVA1:def 6 :
for U being non empty set
for A being non empty IntervalSet of U
for b3 being Subset of U holds
( b3 = A ``2 iff ex B being Subset of U st A = Inter (B,b3) );

theorem Th14: :: INTERVA1:14
for U being non empty set
for A being non empty IntervalSet of U
for X being set holds
( X in A iff ( A ``1 c= X & X c= A ``2 ) )
proof end;

theorem Th15: :: INTERVA1:15
for U being non empty set
for A being non empty IntervalSet of U holds A = Inter ((A ``1),(A ``2))
proof end;

theorem Th16: :: INTERVA1:16
for U being non empty set
for A being non empty IntervalSet of U holds A ``1 c= A ``2
proof end;

theorem Th17: :: INTERVA1:17
for U being non empty set
for A, B being non empty IntervalSet of U holds A _\/_ B = Inter (((A ``1) \/ (B ``1)),((A ``2) \/ (B ``2)))
proof end;

theorem Th18: :: INTERVA1:18
for U being non empty set
for A, B being non empty IntervalSet of U holds A _/\_ B = Inter (((A ``1) /\ (B ``1)),((A ``2) /\ (B ``2)))
proof end;

definition
let U be non empty set ;
let A, B be non empty IntervalSet of U;
:: original: =
redefine pred A = B means :: INTERVA1:def 7
( A ``1 = B ``1 & A ``2 = B ``2 );
compatibility
( A = B iff ( A ``1 = B ``1 & A ``2 = B ``2 ) )
proof end;
end;

:: deftheorem defines = INTERVA1:def 7 :
for U being non empty set
for A, B being non empty IntervalSet of U holds
( A = B iff ( A ``1 = B ``1 & A ``2 = B ``2 ) );

theorem :: INTERVA1:19
for U being non empty set
for A being non empty IntervalSet of U holds A _\/_ A = A
proof end;

theorem :: INTERVA1:20
for U being non empty set
for A being non empty IntervalSet of U holds A _/\_ A = A
proof end;

theorem :: INTERVA1:21
for U being non empty set
for A, B being non empty IntervalSet of U holds A _\/_ B = B _\/_ A ;

theorem :: INTERVA1:22
for U being non empty set
for A, B being non empty IntervalSet of U holds A _/\_ B = B _/\_ A ;

theorem Th23: :: INTERVA1:23
for U being non empty set
for A, B, C being non empty IntervalSet of U holds (A _\/_ B) _\/_ C = A _\/_ (B _\/_ C)
proof end;

theorem Th24: :: INTERVA1:24
for U being non empty set
for A, B, C being non empty IntervalSet of U holds (A _/\_ B) _/\_ C = A _/\_ (B _/\_ C)
proof end;

Lm1: for X being set
for A, B, C being Subset-Family of X holds UNION (A,(INTERSECTION (B,C))) c= INTERSECTION ((UNION (A,B)),(UNION (A,C)))
proof end;

definition
let X be set ;
let F be Subset-Family of X;
attr F is ordered means :Def8: :: INTERVA1:def 8
ex A, B being set st
( A in F & B in F & ( for Y being set holds
( Y in F iff ( A c= Y & Y c= B ) ) ) );
end;

:: deftheorem Def8 defines ordered INTERVA1:def 8 :
for X being set
for F being Subset-Family of X holds
( F is ordered iff ex A, B being set st
( A in F & B in F & ( for Y being set holds
( Y in F iff ( A c= Y & Y c= B ) ) ) ) );

registration
let X be set ;
cluster non empty ordered Element of bool (bool X);
existence
ex b1 being Subset-Family of X st
( not b1 is empty & b1 is ordered )
proof end;
end;

theorem Th25: :: INTERVA1:25
for U being non empty set
for A, B being Subset of U st A c= B holds
Inter (A,B) is non empty ordered Subset-Family of U
proof end;

theorem Th26: :: INTERVA1:26
for U being non empty set
for A being non empty IntervalSet of U holds A is non empty ordered Subset-Family of U
proof end;

notation
let X be set ;
synonym min X for meet X;
synonym max X for union X;
end;

definition
let X be set ;
let F be non empty ordered Subset-Family of X;
:: original: min
redefine func min F -> Element of F;
correctness
coherence
min F is Element of F
;
proof end;
:: original: max
redefine func max F -> Element of F;
correctness
coherence
max F is Element of F
;
proof end;
end;

Lm2: for X being set
for F being non empty ordered Subset-Family of X
for G being set st G in F holds
( G = min F iff for Y being set st Y in F holds
G c= Y )
proof end;

Lm3: for X being set
for F being non empty ordered Subset-Family of X
for G being set st G in F holds
( G = max F iff for Y being set st Y in F holds
Y c= G )
proof end;

theorem Th27: :: INTERVA1:27
for U being non empty set
for A, B being Subset of U
for F being non empty ordered Subset-Family of U st F = Inter (A,B) holds
( min F = A & max F = B )
proof end;

theorem Th28: :: INTERVA1:28
for X, Y being set
for A being non empty ordered Subset-Family of X holds
( Y in A iff ( min A c= Y & Y c= max A ) )
proof end;

Lm4: for U being non empty set
for A being non empty IntervalSet of U holds A is non empty ordered Subset-Family of U
by Th26;

theorem Th29: :: INTERVA1:29
for X being set
for A, B, C being non empty ordered Subset-Family of X holds UNION (A,(INTERSECTION (B,C))) = INTERSECTION ((UNION (A,B)),(UNION (A,C)))
proof end;

Lm5: for X being set
for A, B, C being Subset-Family of X holds INTERSECTION (A,(UNION (B,C))) c= UNION ((INTERSECTION (A,B)),(INTERSECTION (A,C)))
proof end;

theorem Th30: :: INTERVA1:30
for X being set
for A, B, C being non empty ordered Subset-Family of X holds INTERSECTION (A,(UNION (B,C))) = UNION ((INTERSECTION (A,B)),(INTERSECTION (A,C)))
proof end;

theorem :: INTERVA1:31
for U being non empty set
for A, B, C being non empty IntervalSet of U holds A _\/_ (B _/\_ C) = (A _\/_ B) _/\_ (A _\/_ C)
proof end;

theorem :: INTERVA1:32
for U being non empty set
for A, B, C being non empty IntervalSet of U holds A _/\_ (B _\/_ C) = (A _/\_ B) _\/_ (A _/\_ C)
proof end;

theorem Th33: :: INTERVA1:33
for X being set
for A, B being non empty ordered Subset-Family of X holds INTERSECTION (A,(UNION (A,B))) = A
proof end;

theorem Th34: :: INTERVA1:34
for X being set
for A, B being non empty ordered Subset-Family of X holds UNION ((INTERSECTION (A,B)),B) = B
proof end;

theorem Th35: :: INTERVA1:35
for U being non empty set
for A, B being non empty IntervalSet of U holds A _/\_ (A _\/_ B) = A
proof end;

theorem Th36: :: INTERVA1:36
for U being non empty set
for A, B being non empty IntervalSet of U holds (A _/\_ B) _\/_ B = B
proof end;

begin

theorem Th37: :: INTERVA1:37
for U being non empty set
for A, B being Subset-Family of U holds DIFFERENCE (A,B) is Subset-Family of U
proof end;

theorem Th38: :: INTERVA1:38
for U being non empty set
for A, B being non empty ordered Subset-Family of U holds DIFFERENCE (A,B) = { C where C is Subset of U : ( (min A) \ (max B) c= C & C c= (max A) \ (min B) ) }
proof end;

theorem Th39: :: INTERVA1:39
for U being non empty set
for A1, A2, B1, B2 being Subset of U st A1 c= A2 & B1 c= B2 holds
DIFFERENCE ((Inter (A1,A2)),(Inter (B1,B2))) = { C where C is Subset of U : ( A1 \ B2 c= C & C c= A2 \ B1 ) }
proof end;

definition
let U be non empty set ;
let A, B be non empty IntervalSet of U;
func A _\_ B -> IntervalSet of U equals :: INTERVA1:def 9
DIFFERENCE (A,B);
coherence
DIFFERENCE (A,B) is IntervalSet of U
proof end;
end;

:: deftheorem defines _\_ INTERVA1:def 9 :
for U being non empty set
for A, B being non empty IntervalSet of U holds A _\_ B = DIFFERENCE (A,B);

registration
let U be non empty set ;
let A, B be non empty IntervalSet of U;
cluster A _\_ B -> non empty ;
coherence
not A _\_ B is empty
proof end;
end;

theorem Th40: :: INTERVA1:40
for U being non empty set
for A, B being non empty IntervalSet of U holds A _\_ B = Inter (((A ``1) \ (B ``2)),((A ``2) \ (B ``1)))
proof end;

theorem Th41: :: INTERVA1:41
for U being non empty set
for A, C being non empty IntervalSet of U
for X, Y being Subset of U st A = Inter (X,Y) holds
A _\_ C = Inter ((X \ (C ``2)),(Y \ (C ``1)))
proof end;

theorem Th42: :: INTERVA1:42
for U being non empty set
for A, C being non empty IntervalSet of U
for X, Y, W, Z being Subset of U st A = Inter (X,Y) & C = Inter (W,Z) holds
A _\_ C = Inter ((X \ Z),(Y \ W))
proof end;

theorem Th43: :: INTERVA1:43
for U being non empty set holds Inter (([#] U),([#] U)) is non empty IntervalSet of U
proof end;

theorem Th44: :: INTERVA1:44
for U being non empty set holds Inter (({} U),({} U)) is non empty IntervalSet of U
proof end;

registration
let U be non empty set ;
cluster Inter (([#] U),([#] U)) -> non empty ;
coherence
not Inter (([#] U),([#] U)) is empty
by Th43;
cluster Inter (({} U),({} U)) -> non empty ;
coherence
not Inter (({} U),({} U)) is empty
by Th44;
end;

definition
let U be non empty set ;
let A be non empty IntervalSet of U;
func A ^ -> non empty IntervalSet of U equals :: INTERVA1:def 10
(Inter (([#] U),([#] U))) _\_ A;
coherence
(Inter (([#] U),([#] U))) _\_ A is non empty IntervalSet of U
;
end;

:: deftheorem defines ^ INTERVA1:def 10 :
for U being non empty set
for A being non empty IntervalSet of U holds A ^ = (Inter (([#] U),([#] U))) _\_ A;

theorem Th45: :: INTERVA1:45
for U being non empty set
for A being non empty IntervalSet of U holds A ^ = Inter (((A ``2) `),((A ``1) `)) by Th41;

theorem Th46: :: INTERVA1:46
for U being non empty set
for A being non empty IntervalSet of U
for X, Y being Subset of U st A = Inter (X,Y) & X c= Y holds
A ^ = Inter ((Y `),(X `))
proof end;

theorem :: INTERVA1:47
for U being non empty set holds (Inter (({} U),({} U))) ^ = Inter (([#] U),([#] U))
proof end;

theorem :: INTERVA1:48
for U being non empty set holds (Inter (([#] U),([#] U))) ^ = Inter (({} U),({} U))
proof end;

begin

theorem :: INTERVA1:49
for U being non empty set ex A being non empty IntervalSet of U st (A _/\_ A) ^ <> Inter (({} U),({} U))
proof end;

theorem :: INTERVA1:50
for U being non empty set ex A being non empty IntervalSet of U st (A _\/_ A) ^ <> Inter (([#] U),([#] U))
proof end;

theorem :: INTERVA1:51
for U being non empty set ex A being non empty IntervalSet of U st A _\_ A <> Inter (({} U),({} U))
proof end;

theorem :: INTERVA1:52
for U being non empty set
for A being non empty IntervalSet of U holds U in A _\/_ (A ^)
proof end;

theorem :: INTERVA1:53
for U being non empty set
for A being non empty IntervalSet of U holds {} in A _/\_ (A ^)
proof end;

theorem :: INTERVA1:54
for U being non empty set
for A being non empty IntervalSet of U holds {} in A _\_ A
proof end;

begin

definition
let U be non empty set ;
func IntervalSets U -> non empty set means :Def11: :: INTERVA1:def 11
for x being set holds
( x in it iff x is non empty IntervalSet of U );
existence
ex b1 being non empty set st
for x being set holds
( x in b1 iff x is non empty IntervalSet of U )
proof end;
uniqueness
for b1, b2 being non empty set st ( for x being set holds
( x in b1 iff x is non empty IntervalSet of U ) ) & ( for x being set holds
( x in b2 iff x is non empty IntervalSet of U ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines IntervalSets INTERVA1:def 11 :
for U, b2 being non empty set holds
( b2 = IntervalSets U iff for x being set holds
( x in b2 iff x is non empty IntervalSet of U ) );

definition
let U be non empty set ;
func InterLatt U -> non empty strict LattStr means :Def12: :: INTERVA1:def 12
( the carrier of it = IntervalSets U & ( for a, b being Element of the carrier of it
for a9, b9 being non empty IntervalSet of U st a9 = a & b9 = b holds
( the L_join of it . (a,b) = a9 _\/_ b9 & the L_meet of it . (a,b) = a9 _/\_ b9 ) ) );
existence
ex b1 being non empty strict LattStr st
( the carrier of b1 = IntervalSets U & ( for a, b being Element of the carrier of b1
for a9, b9 being non empty IntervalSet of U st a9 = a & b9 = b holds
( the L_join of b1 . (a,b) = a9 _\/_ b9 & the L_meet of b1 . (a,b) = a9 _/\_ b9 ) ) )
proof end;
uniqueness
for b1, b2 being non empty strict LattStr st the carrier of b1 = IntervalSets U & ( for a, b being Element of the carrier of b1
for a9, b9 being non empty IntervalSet of U st a9 = a & b9 = b holds
( the L_join of b1 . (a,b) = a9 _\/_ b9 & the L_meet of b1 . (a,b) = a9 _/\_ b9 ) ) & the carrier of b2 = IntervalSets U & ( for a, b being Element of the carrier of b2
for a9, b9 being non empty IntervalSet of U st a9 = a & b9 = b holds
( the L_join of b2 . (a,b) = a9 _\/_ b9 & the L_meet of b2 . (a,b) = a9 _/\_ b9 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines InterLatt INTERVA1:def 12 :
for U being non empty set
for b2 being non empty strict LattStr holds
( b2 = InterLatt U iff ( the carrier of b2 = IntervalSets U & ( for a, b being Element of the carrier of b2
for a9, b9 being non empty IntervalSet of U st a9 = a & b9 = b holds
( the L_join of b2 . (a,b) = a9 _\/_ b9 & the L_meet of b2 . (a,b) = a9 _/\_ b9 ) ) ) );

registration
let U be non empty set ;
cluster InterLatt U -> non empty strict Lattice-like ;
correctness
coherence
InterLatt U is Lattice-like
;
proof end;
end;

definition
let X be Tolerance_Space;
mode RoughSet of X -> Element of [:(bool the carrier of X),(bool the carrier of X):] means :Def13: :: INTERVA1:def 13
verum;
existence
ex b1 being Element of [:(bool the carrier of X),(bool the carrier of X):] st verum
;
end;

:: deftheorem Def13 defines RoughSet INTERVA1:def 13 :
for X being Tolerance_Space
for b2 being Element of [:(bool the carrier of X),(bool the carrier of X):] holds
( b2 is RoughSet of X iff verum );

theorem Th55: :: INTERVA1:55
for X being Tolerance_Space
for A being RoughSet of X ex B, C being Subset of X st A = [B,C]
proof end;

definition
let X be Tolerance_Space;
let A be Subset of X;
func RS A -> RoughSet of X equals :: INTERVA1:def 14
[(LAp A),(UAp A)];
coherence
[(LAp A),(UAp A)] is RoughSet of X
proof end;
end;

:: deftheorem defines RS INTERVA1:def 14 :
for X being Tolerance_Space
for A being Subset of X holds RS A = [(LAp A),(UAp A)];

definition
let X be Tolerance_Space;
let A be RoughSet of X;
func LAp A -> Subset of X equals :: INTERVA1:def 15
A `1 ;
coherence
A `1 is Subset of X
proof end;
func UAp A -> Subset of X equals :: INTERVA1:def 16
A `2 ;
coherence
A `2 is Subset of X
proof end;
end;

:: deftheorem defines LAp INTERVA1:def 15 :
for X being Tolerance_Space
for A being RoughSet of X holds LAp A = A `1 ;

:: deftheorem defines UAp INTERVA1:def 16 :
for X being Tolerance_Space
for A being RoughSet of X holds UAp A = A `2 ;

definition
let X be Tolerance_Space;
let A, B be RoughSet of X;
:: original: =
redefine pred A = B means :Def17: :: INTERVA1:def 17
( LAp A = LAp B & UAp A = UAp B );
compatibility
( A = B iff ( LAp A = LAp B & UAp A = UAp B ) )
proof end;
end;

:: deftheorem Def17 defines = INTERVA1:def 17 :
for X being Tolerance_Space
for A, B being RoughSet of X holds
( A = B iff ( LAp A = LAp B & UAp A = UAp B ) );

definition
let X be Tolerance_Space;
let A, B be RoughSet of X;
func A _\/_ B -> RoughSet of X equals :: INTERVA1:def 18
[((LAp A) \/ (LAp B)),((UAp A) \/ (UAp B))];
coherence
[((LAp A) \/ (LAp B)),((UAp A) \/ (UAp B))] is RoughSet of X
proof end;
func A _/\_ B -> RoughSet of X equals :: INTERVA1:def 19
[((LAp A) /\ (LAp B)),((UAp A) /\ (UAp B))];
coherence
[((LAp A) /\ (LAp B)),((UAp A) /\ (UAp B))] is RoughSet of X
proof end;
end;

:: deftheorem defines _\/_ INTERVA1:def 18 :
for X being Tolerance_Space
for A, B being RoughSet of X holds A _\/_ B = [((LAp A) \/ (LAp B)),((UAp A) \/ (UAp B))];

:: deftheorem defines _/\_ INTERVA1:def 19 :
for X being Tolerance_Space
for A, B being RoughSet of X holds A _/\_ B = [((LAp A) /\ (LAp B)),((UAp A) /\ (UAp B))];

theorem Th56: :: INTERVA1:56
for X being Tolerance_Space
for A, B being RoughSet of X holds LAp (A _\/_ B) = (LAp A) \/ (LAp B) by MCART_1:7;

theorem Th57: :: INTERVA1:57
for X being Tolerance_Space
for A, B being RoughSet of X holds UAp (A _\/_ B) = (UAp A) \/ (UAp B) by MCART_1:7;

theorem Th58: :: INTERVA1:58
for X being Tolerance_Space
for A, B being RoughSet of X holds LAp (A _/\_ B) = (LAp A) /\ (LAp B) by MCART_1:7;

theorem Th59: :: INTERVA1:59
for X being Tolerance_Space
for A, B being RoughSet of X holds UAp (A _/\_ B) = (UAp A) /\ (UAp B) by MCART_1:7;

theorem :: INTERVA1:60
for X being Tolerance_Space
for A being RoughSet of X holds A _\/_ A = A
proof end;

theorem Th61: :: INTERVA1:61
for X being Tolerance_Space
for A being RoughSet of X holds A _/\_ A = A
proof end;

theorem :: INTERVA1:62
for X being Tolerance_Space
for A, B being RoughSet of X holds A _\/_ B = B _\/_ A ;

theorem :: INTERVA1:63
for X being Tolerance_Space
for A, B being RoughSet of X holds A _/\_ B = B _/\_ A ;

theorem Th64: :: INTERVA1:64
for X being Tolerance_Space
for A, B, C being RoughSet of X holds (A _\/_ B) _\/_ C = A _\/_ (B _\/_ C)
proof end;

theorem Th65: :: INTERVA1:65
for X being Tolerance_Space
for A, B, C being RoughSet of X holds (A _/\_ B) _/\_ C = A _/\_ (B _/\_ C)
proof end;

theorem Th66: :: INTERVA1:66
for X being Tolerance_Space
for A, B, C being RoughSet of X holds A _/\_ (B _\/_ C) = (A _/\_ B) _\/_ (A _/\_ C)
proof end;

theorem Th67: :: INTERVA1:67
for X being Tolerance_Space
for A, B being RoughSet of X holds A _\/_ (A _/\_ B) = A
proof end;

theorem :: INTERVA1:68
for X being Tolerance_Space
for A, B being RoughSet of X holds A _/\_ (A _\/_ B) = A
proof end;

begin

definition
let X be Tolerance_Space;
func RoughSets X -> set means :Def20: :: INTERVA1:def 20
for x being set holds
( x in it iff x is RoughSet of X );
existence
ex b1 being set st
for x being set holds
( x in b1 iff x is RoughSet of X )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff x is RoughSet of X ) ) & ( for x being set holds
( x in b2 iff x is RoughSet of X ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def20 defines RoughSets INTERVA1:def 20 :
for X being Tolerance_Space
for b2 being set holds
( b2 = RoughSets X iff for x being set holds
( x in b2 iff x is RoughSet of X ) );

registration
let X be Tolerance_Space;
cluster RoughSets X -> non empty ;
coherence
not RoughSets X is empty
proof end;
end;

definition
let X be Tolerance_Space;
let R be Element of RoughSets X;
func @ R -> RoughSet of X equals :: INTERVA1:def 21
R;
coherence
R is RoughSet of X
by Def20;
end;

:: deftheorem defines @ INTERVA1:def 21 :
for X being Tolerance_Space
for R being Element of RoughSets X holds @ R = R;

definition
let X be Tolerance_Space;
let R be RoughSet of X;
func R @ -> Element of RoughSets X equals :: INTERVA1:def 22
R;
coherence
R is Element of RoughSets X
by Def20;
end;

:: deftheorem defines @ INTERVA1:def 22 :
for X being Tolerance_Space
for R being RoughSet of X holds R @ = R;

definition
let X be Tolerance_Space;
func RSLattice X -> strict LattStr means :Def23: :: INTERVA1:def 23
( the carrier of it = RoughSets X & ( for A, B being Element of RoughSets X
for A9, B9 being RoughSet of X st A = A9 & B = B9 holds
( the L_join of it . (A,B) = A9 _\/_ B9 & the L_meet of it . (A,B) = A9 _/\_ B9 ) ) );
existence
ex b1 being strict LattStr st
( the carrier of b1 = RoughSets X & ( for A, B being Element of RoughSets X
for A9, B9 being RoughSet of X st A = A9 & B = B9 holds
( the L_join of b1 . (A,B) = A9 _\/_ B9 & the L_meet of b1 . (A,B) = A9 _/\_ B9 ) ) )
proof end;
uniqueness
for b1, b2 being strict LattStr st the carrier of b1 = RoughSets X & ( for A, B being Element of RoughSets X
for A9, B9 being RoughSet of X st A = A9 & B = B9 holds
( the L_join of b1 . (A,B) = A9 _\/_ B9 & the L_meet of b1 . (A,B) = A9 _/\_ B9 ) ) & the carrier of b2 = RoughSets X & ( for A, B being Element of RoughSets X
for A9, B9 being RoughSet of X st A = A9 & B = B9 holds
( the L_join of b2 . (A,B) = A9 _\/_ B9 & the L_meet of b2 . (A,B) = A9 _/\_ B9 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def23 defines RSLattice INTERVA1:def 23 :
for X being Tolerance_Space
for b2 being strict LattStr holds
( b2 = RSLattice X iff ( the carrier of b2 = RoughSets X & ( for A, B being Element of RoughSets X
for A9, B9 being RoughSet of X st A = A9 & B = B9 holds
( the L_join of b2 . (A,B) = A9 _\/_ B9 & the L_meet of b2 . (A,B) = A9 _/\_ B9 ) ) ) );

registration
let X be Tolerance_Space;
cluster RSLattice X -> non empty strict ;
coherence
not RSLattice X is empty
proof end;
end;

Lm6: for X being Tolerance_Space
for a, b being Element of (RSLattice X) holds a "\/" b = b "\/" a
proof end;

Lm7: for X being Tolerance_Space
for a, b, c being Element of (RSLattice X) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c
proof end;

Lm8: for X being Tolerance_Space
for K, L being Element of RoughSets X holds the L_join of (RSLattice X) . (( the L_meet of (RSLattice X) . (K,L)),L) = L
proof end;

Lm9: for X being Tolerance_Space
for a, b being Element of (RSLattice X) holds (a "/\" b) "\/" b = b
proof end;

Lm10: for X being Tolerance_Space
for a, b being Element of (RSLattice X) holds a "/\" b = b "/\" a
proof end;

Lm11: for X being Tolerance_Space
for a, b, c being Element of (RSLattice X) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c
proof end;

Lm12: for X being Tolerance_Space
for K, L, M being Element of RoughSets X holds the L_meet of (RSLattice X) . (K,( the L_join of (RSLattice X) . (L,M))) = the L_join of (RSLattice X) . (( the L_meet of (RSLattice X) . (K,L)),( the L_meet of (RSLattice X) . (K,M)))
proof end;

Lm13: for X being Tolerance_Space
for a, b being Element of (RSLattice X) holds a "/\" (a "\/" b) = a
proof end;

registration
let X be Tolerance_Space;
cluster RSLattice X -> strict Lattice-like ;
coherence
RSLattice X is Lattice-like
proof end;
end;

registration
let X be Tolerance_Space;
cluster RSLattice X -> strict distributive ;
coherence
RSLattice X is distributive
proof end;
end;

definition
let X be Tolerance_Space;
func ERS X -> RoughSet of X equals :: INTERVA1:def 24
[{},{}];
coherence
[{},{}] is RoughSet of X
proof end;
end;

:: deftheorem defines ERS INTERVA1:def 24 :
for X being Tolerance_Space holds ERS X = [{},{}];

Lm14: for X being Tolerance_Space holds ERS X in RoughSets X
by Def20;

theorem Th69: :: INTERVA1:69
for X being Tolerance_Space
for A being RoughSet of X holds (ERS X) _\/_ A = A
proof end;

definition
let X be Tolerance_Space;
func TRS X -> RoughSet of X equals :: INTERVA1:def 25
[([#] X),([#] X)];
coherence
[([#] X),([#] X)] is RoughSet of X
proof end;
end;

:: deftheorem defines TRS INTERVA1:def 25 :
for X being Tolerance_Space holds TRS X = [([#] X),([#] X)];

Lm15: for X being Tolerance_Space holds TRS X in RoughSets X
by Def20;

theorem Th70: :: INTERVA1:70
for X being Tolerance_Space
for A being RoughSet of X holds (TRS X) _/\_ A = A
proof end;

registration
let X be Tolerance_Space;
cluster RSLattice X -> strict bounded ;
coherence
RSLattice X is bounded
proof end;
end;

theorem Th71: :: INTERVA1:71
for X being Tolerance_Space
for A, B being Element of (RSLattice X)
for A9, B9 being RoughSet of X st A = A9 & B = B9 holds
( A [= B iff ( LAp A9 c= LAp B9 & UAp A9 c= UAp B9 ) )
proof end;

Lm16: for X being Tolerance_Space holds RSLattice X is complete
proof end;

registration
let X be Tolerance_Space;
cluster RSLattice X -> strict complete ;
coherence
RSLattice X is complete
by Lm16;
end;