:: INTERVA1 semantic presentation

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
set IT =  {  A where A is Subset of U : ( X c= A & A c= Y )  }  ;
  {  A where A is Subset of U : ( X c= A & A c= Y )  }  c= bool U
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  A where A is Subset of U : ( X c= A & A c= Y )  }  or x in bool U )
assume  x in  {  A where A is Subset of U : ( X c= A & A c= Y )  }  ; ::_thesis: x in bool U
then  x in  {  A where A is Subset of U : ( X c= A & A c= Y )  }  ;
then consider B being Subset of U such that
A1: ( x = B & X c= B & B c= Y ) ;
thus  x in bool U by A1; ::_thesis: verum
end;
then   {  A where A is Subset of U : ( X c= A & A c= Y )  }  is Subset-Family of U ;
hence   {  A where A is Subset of U : ( X c= A & A c= Y )  }  is Subset-Family of U ; ::_thesis: verum
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
let U be set ; ::_thesis: for X, Y being Subset of U
for x being set holds
( x in Inter (X,Y) iff ( X c= x & x c= Y ) )
let X, Y be Subset of U; ::_thesis: for x being set holds
( x in Inter (X,Y) iff ( X c= x & x c= Y ) )
let x be set ; ::_thesis: ( x in Inter (X,Y) iff ( X c= x & x c= Y ) )
hereby  ::_thesis: ( X c= x & x c= Y implies x in Inter (X,Y) )
assume  x in Inter (X,Y) ; ::_thesis: ( X c= x & x c= Y )
then consider A9 being Element of bool U such that
A1: ( x = A9 & X c= A9 & A9 c= Y ) ;
thus  ( X c= x & x c= Y ) by A1; ::_thesis: verum
end;
assume A2: ( X c= x & x c= Y ) ; ::_thesis: x in Inter (X,Y)
then  x is Subset of U by XBOOLE_1:1;
hence  x in Inter (X,Y) by A2; ::_thesis: verum
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
let U be set ; ::_thesis: for X, Y being Subset of U st Inter (X,Y) <> {} holds
( X in Inter (X,Y) & Y in Inter (X,Y) )
let X, Y be Subset of U; ::_thesis: ( Inter (X,Y) <> {} implies ( X in Inter (X,Y) & Y in Inter (X,Y) ) )
assume  Inter (X,Y) <> {} ; ::_thesis: ( X in Inter (X,Y) & Y in Inter (X,Y) )
then consider x being set  such that
A1: x in Inter (X,Y) by XBOOLE_0:def_1;
 ( X c= x & x c= Y ) by A1, Th1;
then  X c= Y by XBOOLE_1:1;
hence  ( X in Inter (X,Y) & Y in Inter (X,Y) ) ; ::_thesis: verum
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
let U be set ; ::_thesis: for A, B being Subset of U st not A c= B holds
Inter (A,B) = {}
let A, B be Subset of U; ::_thesis: ( not A c= B implies Inter (A,B) = {} )
assume A1: not A c= B ; ::_thesis: Inter (A,B) = {}
assume  Inter (A,B) <> {} ; ::_thesis: contradiction
then consider x being set  such that
A2: x in Inter (A,B) by XBOOLE_0:def_1;
 ( A c= x & x c= B ) by A2, Th1;
hence  contradiction by A1, XBOOLE_1:1; ::_thesis: verum
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
let U be set ; ::_thesis: for A, B being Subset of U st Inter (A,B) <> {} holds
A c= B
let A, B be Subset of U; ::_thesis: ( Inter (A,B) <> {} implies A c= B )
assume  Inter (A,B) <> {} ; ::_thesis: A c= B
then consider x being set  such that
A1: x in Inter (A,B) by XBOOLE_0:def_1;
 ( A c= x & x c= B ) by A1, Th1;
hence  A c= B by XBOOLE_1:1; ::_thesis: verum
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
let U be set ; ::_thesis: for A, B, C, D being Subset of U st Inter (A,B) <> {} & Inter (A,B) = Inter (C,D) holds
( A = C & B = D )
let A, B, C, D be Subset of U; ::_thesis: ( Inter (A,B) <> {} & Inter (A,B) = Inter (C,D) implies ( A = C & B = D ) )
assume A1: ( Inter (A,B) <> {} & Inter (A,B) = Inter (C,D) ) ; ::_thesis: ( A = C & B = D )
then  A in Inter (A,B) by Th2;
then A2: ( C c= A & A c= D ) by Th1, A1;
 C in Inter (C,D) by A1, Th2;
then A3: ( A c= C & C c= B ) by A1, Th1;
 B in Inter (A,B) by A1, Th2;
then A4: B c= D by Th1, A1;
 D in Inter (C,D) by A1, Th2;
then  D c= B by A1, Th1;
hence  ( A = C & B = D ) by A3, A4, A2, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th7: :: INTERVA1:7
for U being non empty set
for A being non empty Subset of U holds Inter (A,({} U)) = {}
proof
let U be non empty set ; ::_thesis: for A being non empty Subset of U holds Inter (A,({} U)) = {}
let A be non empty Subset of U; ::_thesis: Inter (A,({} U)) = {}
thus  Inter (A,({} U)) c= {} :: according to XBOOLE_0:def_10 ::_thesis: {} c= Inter (A,({} U))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Inter (A,({} U)) or x in {} )
assume  x in Inter (A,({} U)) ; ::_thesis: x in {}
then  ( A c= x & x c= {} U ) by Th1;
hence  x in {} ; ::_thesis: verum
end;
thus  {} c= Inter (A,({} U)) by XBOOLE_1:2; ::_thesis: verum
end;

theorem Th8: :: INTERVA1:8
for U being set
for A being Subset of U holds Inter (A,A) = {A}
proof
let U be set ; ::_thesis: for A being Subset of U holds Inter (A,A) = {A}
let A be Subset of U; ::_thesis: Inter (A,A) = {A}
thus  Inter (A,A) c= {A} :: according to XBOOLE_0:def_10 ::_thesis: {A} c= Inter (A,A)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Inter (A,A) or x in {A} )
assume  x in Inter (A,A) ; ::_thesis: x in {A}
then  ( A c= x & x c= A ) by Th1;
then  A = x by XBOOLE_0:def_10;
hence  x in {A} by TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {A} or x in Inter (A,A) )
assume  x in {A} ; ::_thesis: x in Inter (A,A)
then  x = A by TARSKI:def_1;
hence  x in Inter (A,A) ; ::_thesis: verum
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
set A = the Subset of U;
set IT = { the Subset of U};
 { the Subset of U} = Inter ( the Subset of U, the Subset of U) by Th8;
hence  ex b1 being Subset-Family of U ex A, B being Subset of U st b1 = Inter (A,B) ; ::_thesis: verum
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
let U be non empty set ; ::_thesis: {} is IntervalSet of U
set A = the non empty Subset of U;
 Inter ( the non empty Subset of U,({} U)) = {} by Th7;
hence  {} is IntervalSet of U by Def2; ::_thesis: verum
end;

theorem Th10: :: INTERVA1:10
for U being non empty set
for A being Subset of U holds {A} is IntervalSet of U
proof
let U be non empty set ; ::_thesis: for A being Subset of U holds {A} is IntervalSet of U
let A be Subset of U; ::_thesis: {A} is IntervalSet of U
 Inter (A,A) = {A} by Th8;
hence  {A} is IntervalSet of U by Def2; ::_thesis: verum
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 for IntervalSet of U;
existence
 not for b1 being IntervalSet of U holds b1 is empty
proof
set A = the Subset of U;
 { the Subset of U} is IntervalSet of U by Th10;
hence  not for b1 being IntervalSet of U holds b1 is empty ; ::_thesis: verum
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
let U be non empty set ; ::_thesis: 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) ) )
let A be set ; ::_thesis: ( A is non empty IntervalSet of U iff ex A1, A2 being Subset of U st
( A1 c= A2 & A = Inter (A1,A2) ) )
hereby  ::_thesis: ( ex A1, A2 being Subset of U st
( A1 c= A2 & A = Inter (A1,A2) ) implies A is non empty IntervalSet of U )
assume A1: A is non empty IntervalSet of U ; ::_thesis: ex A1, A2 being Subset of U st
( A1 c= A2 & A = Inter (A1,A2) )
then consider A1, A2 being Subset of U such that
A2: A = Inter (A1,A2) by Def2;
take A1 = A1; ::_thesis: ex A2 being Subset of U st
( A1 c= A2 & A = Inter (A1,A2) )
take A2 = A2; ::_thesis: ( A1 c= A2 & A = Inter (A1,A2) )
thus  A1 c= A2 by A1, A2, Th3; ::_thesis: A = Inter (A1,A2)
thus  A = Inter (A1,A2) by A2; ::_thesis: verum
end;
given A1, A2 being Subset of U such that A3: ( A1 c= A2 & A = Inter (A1,A2) ) ; ::_thesis: A is non empty IntervalSet of U
 A1 in Inter (A1,A2) by A3;
hence  A is non empty IntervalSet of U by A3; ::_thesis: verum
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
let U be non empty set ; ::_thesis: 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 )  }
let A1, A2, B1, B2 be Subset of U; ::_thesis: ( A1 c= A2 & B1 c= B2 implies INTERSECTION ((Inter (A1,A2)),(Inter (B1,B2))) =  {  C where C is Subset of U : ( A1 /\ B1 c= C & C c= A2 /\ B2 )  }  )
assume that
A1: A1 c= A2 and
A2: B1 c= B2 ; ::_thesis: INTERSECTION ((Inter (A1,A2)),(Inter (B1,B2))) =  {  C where C is Subset of U : ( A1 /\ B1 c= C & C c= A2 /\ B2 )  }
set A = Inter (A1,A2);
set B = Inter (B1,B2);
set LAB = A1 /\ B1;
set UAB = A2 /\ B2;
set IT = INTERSECTION ((Inter (A1,A2)),(Inter (B1,B2)));
thus  INTERSECTION ((Inter (A1,A2)),(Inter (B1,B2))) c=  {  C where C is Subset of U : ( A1 /\ B1 c= C & C c= A2 /\ B2 )  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  C where C is Subset of U : ( A1 /\ B1 c= C & C c= A2 /\ B2 )  }  c= INTERSECTION ((Inter (A1,A2)),(Inter (B1,B2)))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in INTERSECTION ((Inter (A1,A2)),(Inter (B1,B2))) or x in  {  C where C is Subset of U : ( A1 /\ B1 c= C & C c= A2 /\ B2 )  }  )
assume  x in INTERSECTION ((Inter (A1,A2)),(Inter (B1,B2))) ; ::_thesis: x in  {  C where C is Subset of U : ( A1 /\ B1 c= C & C c= A2 /\ B2 )  }
then consider X, Y being set  such that
A3: ( X in Inter (A1,A2) & Y in Inter (B1,B2) & x = X /\ Y ) by SETFAM_1:def_5;
 x c= X by A3, XBOOLE_1:17;
then A4: x is Subset of U by A3, XBOOLE_1:1;
A5: A1 c= X by Th1, A3;
 B1 c= Y by Th1, A3;
then A6: A1 /\ B1 c= x by A5, A3, XBOOLE_1:27;
A7: X c= A2 by Th1, A3;
 Y c= B2 by Th1, A3;
then  x c= A2 /\ B2 by A7, A3, XBOOLE_1:27;
hence  x in  {  C where C is Subset of U : ( A1 /\ B1 c= C & C c= A2 /\ B2 )  }  by A6, A4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  C where C is Subset of U : ( A1 /\ B1 c= C & C c= A2 /\ B2 )  }  or x in INTERSECTION ((Inter (A1,A2)),(Inter (B1,B2))) )
assume  x in  {  C where C is Subset of U : ( A1 /\ B1 c= C & C c= A2 /\ B2 )  }  ; ::_thesis: x in INTERSECTION ((Inter (A1,A2)),(Inter (B1,B2)))
then consider C9 being Subset of U such that
A8: ( C9 = x & A1 /\ B1 c= C9 & C9 c= A2 /\ B2 ) ;
set x1 = (x \/ A1) /\ A2;
set x2 = (x \/ B1) /\ B2;
A9: (A1 /\ B1) \/ x = x by A8, XBOOLE_1:12;
A10: (A2 /\ B2) /\ x = x by A8, XBOOLE_1:28;
A11: ((x \/ A1) /\ A2) /\ ((x \/ B1) /\ B2) = (x \/ A1) /\ (A2 /\ ((x \/ B1) /\ B2)) by XBOOLE_1:16
.= (x \/ A1) /\ ((x \/ B1) /\ (B2 /\ A2)) by XBOOLE_1:16
.= ((x \/ A1) /\ (x \/ B1)) /\ (A2 /\ B2) by XBOOLE_1:16
.= x by A9, A10, XBOOLE_1:24 ;
 A1 /\ A2 = A1 by A1, XBOOLE_1:28;
then  (x \/ A1) /\ A2 = (x /\ A2) \/ A1 by XBOOLE_1:23;
then A12: A1 c= (x \/ A1) /\ A2 by XBOOLE_1:7;
 (x \/ A1) /\ A2 c= A2 by XBOOLE_1:17;
then A13: (x \/ A1) /\ A2 in Inter (A1,A2) by A12;
 B1 /\ B2 = B1 by A2, XBOOLE_1:28;
then  (x \/ B1) /\ B2 = (x /\ B2) \/ B1 by XBOOLE_1:23;
then A14: B1 c= (x \/ B1) /\ B2 by XBOOLE_1:7;
 (x \/ B1) /\ B2 c= B2 by XBOOLE_1:17;
then  (x \/ B1) /\ B2 in Inter (B1,B2) by A14;
hence  x in INTERSECTION ((Inter (A1,A2)),(Inter (B1,B2))) by A11, A13, SETFAM_1:def_5; ::_thesis: verum
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
let U be non empty set ; ::_thesis: 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 )  }
let A1, A2, B1, B2 be Subset of U; ::_thesis: ( A1 c= A2 & B1 c= B2 implies UNION ((Inter (A1,A2)),(Inter (B1,B2))) =  {  C where C is Subset of U : ( A1 \/ B1 c= C & C c= A2 \/ B2 )  }  )
assume that
A1: A1 c= A2 and
A2: B1 c= B2 ; ::_thesis: UNION ((Inter (A1,A2)),(Inter (B1,B2))) =  {  C where C is Subset of U : ( A1 \/ B1 c= C & C c= A2 \/ B2 )  }
set A = Inter (A1,A2);
set B = Inter (B1,B2);
set LAB = A1 \/ B1;
set UAB = A2 \/ B2;
set IT = UNION ((Inter (A1,A2)),(Inter (B1,B2)));
thus  UNION ((Inter (A1,A2)),(Inter (B1,B2))) c=  {  C where C is Subset of U : ( A1 \/ B1 c= C & C c= A2 \/ B2 )  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  C where C is Subset of U : ( A1 \/ B1 c= C & C c= A2 \/ B2 )  }  c= UNION ((Inter (A1,A2)),(Inter (B1,B2)))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in UNION ((Inter (A1,A2)),(Inter (B1,B2))) or x in  {  C where C is Subset of U : ( A1 \/ B1 c= C & C c= A2 \/ B2 )  }  )
assume  x in UNION ((Inter (A1,A2)),(Inter (B1,B2))) ; ::_thesis: x in  {  C where C is Subset of U : ( A1 \/ B1 c= C & C c= A2 \/ B2 )  }
then consider X, Y being set  such that
A3: ( X in Inter (A1,A2) & Y in Inter (B1,B2) & x = X \/ Y ) by SETFAM_1:def_4;
A4: x is Subset of U by A3, XBOOLE_1:8;
A5: A1 c= X by Th1, A3;
 B1 c= Y by Th1, A3;
then A6: A1 \/ B1 c= x by A5, A3, XBOOLE_1:13;
A7: X c= A2 by Th1, A3;
 Y c= B2 by Th1, A3;
then  x c= A2 \/ B2 by A7, A3, XBOOLE_1:13;
hence  x in  {  C where C is Subset of U : ( A1 \/ B1 c= C & C c= A2 \/ B2 )  }  by A4, A6; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  C where C is Subset of U : ( A1 \/ B1 c= C & C c= A2 \/ B2 )  }  or x in UNION ((Inter (A1,A2)),(Inter (B1,B2))) )
assume  x in  {  C where C is Subset of U : ( A1 \/ B1 c= C & C c= A2 \/ B2 )  }  ; ::_thesis: x in UNION ((Inter (A1,A2)),(Inter (B1,B2)))
then consider C9 being Subset of U such that
A8: ( C9 = x & A1 \/ B1 c= C9 & C9 c= A2 \/ B2 ) ;
set x1 = (x \/ A1) /\ A2;
set x2 = (x \/ B1) /\ B2;
A9: (A1 \/ B1) \/ x = x by A8, XBOOLE_1:12;
A10: (A2 \/ B2) /\ x = x by A8, XBOOLE_1:28;
A11: A1 /\ A2 = A1 by A1, XBOOLE_1:28;
A12: B1 /\ B2 = B1 by A2, XBOOLE_1:28;
A13: ((x \/ A1) /\ A2) \/ ((x \/ B1) /\ B2) = ((x /\ A2) \/ (A1 /\ A2)) \/ ((x \/ B1) /\ B2) by XBOOLE_1:23
.= ((x /\ A2) \/ A1) \/ ((x /\ B2) \/ (B1 /\ B2)) by A11, XBOOLE_1:23
.= (x /\ A2) \/ (A1 \/ ((x /\ B2) \/ B1)) by A12, XBOOLE_1:4
.= (x /\ A2) \/ ((x /\ B2) \/ (A1 \/ B1)) by XBOOLE_1:4
.= ((x /\ A2) \/ (x /\ B2)) \/ (A1 \/ B1) by XBOOLE_1:4
.= x by A9, A10, XBOOLE_1:23 ;
 A1 /\ A2 = A1 by A1, XBOOLE_1:28;
then  (x \/ A1) /\ A2 = (x /\ A2) \/ A1 by XBOOLE_1:23;
then A14: A1 c= (x \/ A1) /\ A2 by XBOOLE_1:7;
 (x \/ A1) /\ A2 c= A2 by XBOOLE_1:17;
then A15: (x \/ A1) /\ A2 in Inter (A1,A2) by A14;
 B1 /\ B2 = B1 by A2, XBOOLE_1:28;
then  (x \/ B1) /\ B2 = (x /\ B2) \/ B1 by XBOOLE_1:23;
then A16: B1 c= (x \/ B1) /\ B2 by XBOOLE_1:7;
 (x \/ B1) /\ B2 c= B2 by XBOOLE_1:17;
then  (x \/ B1) /\ B2 in Inter (B1,B2) by A16;
hence  x in UNION ((Inter (A1,A2)),(Inter (B1,B2))) by A13, A15, SETFAM_1:def_4; ::_thesis: verum
end;

definition
let U be non empty set ;
let A, B be non empty IntervalSet of U;
funcA _/\_ B ->  IntervalSet of U equals :: INTERVA1:def 3
 INTERSECTION (A,B);
coherence
 INTERSECTION (A,B) is IntervalSet of U
proof
set IT = INTERSECTION (A,B);
consider A1, A2 being Subset of U such that
A1: ( A1 c= A2 & A = Inter (A1,A2) ) by Th11;
consider B1, B2 being Subset of U such that
A2: ( B1 c= B2 & B = Inter (B1,B2) ) by Th11;
set LAB = A1 /\ B1;
set UAB = A2 /\ B2;
 INTERSECTION (A,B) = Inter ((A1 /\ B1),(A2 /\ B2)) by Th12, A1, A2;
hence  INTERSECTION (A,B) is IntervalSet of U ; ::_thesis: verum
end;
funcA _\/_ B ->  IntervalSet of U equals :: INTERVA1:def 4
 UNION (A,B);
coherence
 UNION (A,B) is IntervalSet of U
proof
set IT = UNION (A,B);
consider A1, A2 being Subset of U such that
A3: ( A1 c= A2 & A = Inter (A1,A2) ) by Th11;
consider B1, B2 being Subset of U such that
A4: ( B1 c= B2 & B = Inter (B1,B2) ) by Th11;
set LAB = A1 \/ B1;
set UAB = A2 \/ B2;
 UNION (A,B) = Inter ((A1 \/ B1),(A2 \/ B2)) by Th13, A3, A4;
hence  UNION (A,B) is IntervalSet of U ; ::_thesis: verum
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;
clusterA _/\_ B ->  non empty ;
coherence
 not A _/\_ B is empty by TOPGEN_4:31;
clusterA _\/_ 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;
funcA ``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
consider A1, A2 being Subset of U such that
A1: ( A1 c= A2 & A = Inter (A1,A2) ) by Th11;
thus  ex b1, B being Subset of U st A = Inter (b1,B) by A1; ::_thesis: verum
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;
funcA ``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
consider A1, A2 being Subset of U such that
A2: ( A1 c= A2 & A = Inter (A1,A2) ) by Th11;
thus  ex b1, B being Subset of U st A = Inter (B,b1) by A2; ::_thesis: verum
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
let U be non empty set ; ::_thesis: 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 ) )
let A be non empty IntervalSet of U; ::_thesis: for X being set holds
( X in A iff ( A ``1 c= X & X c= A ``2 ) )
let X be set ; ::_thesis: ( X in A iff ( A ``1 c= X & X c= A ``2 ) )
A1: ( X in A implies ( A ``1 c= X & X c= A ``2 ) )
proof
assume A2: X in A ; ::_thesis: ( A ``1 c= X & X c= A ``2 )
A3: A ``1 c= X
proof
consider B being Subset of U such that
A4: A = Inter ((A ``1),B) by Def5;
thus  A ``1 c= X by Th1, A2, A4; ::_thesis: verum
end;
 X c= A ``2
proof
consider B being Subset of U such that
A5: A = Inter (B,(A ``2)) by Def6;
thus  X c= A ``2 by Th1, A2, A5; ::_thesis: verum
end;
hence  ( A ``1 c= X & X c= A ``2 ) by A3; ::_thesis: verum
end;
 ( A ``1 c= X & X c= A ``2 implies X in A )
proof
assume  ( A ``1 c= X & X c= A ``2 ) ; ::_thesis: X in A
then A6: X in Inter ((A ``1),(A ``2)) by Th1;
consider B being Subset of U such that
A7: A = Inter ((A ``1),B) by Def5;
consider C being Subset of U such that
A8: A = Inter (C,(A ``2)) by Def6;
thus  X in A by A7, A6, Th6, A8; ::_thesis: verum
end;
hence  ( X in A iff ( A ``1 c= X & X c= A ``2 ) ) by A1; ::_thesis: verum
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
let U be non empty set ; ::_thesis: for A being non empty IntervalSet of U holds A = Inter ((A ``1),(A ``2))
let A be non empty IntervalSet of U; ::_thesis: A = Inter ((A ``1),(A ``2))
A1: Inter ((A ``1),(A ``2)) c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Inter ((A ``1),(A ``2)) or x in A )
assume  x in Inter ((A ``1),(A ``2)) ; ::_thesis: x in A
then  ( A ``1 c= x & x c= A ``2 ) by Th1;
hence  x in A by Th14; ::_thesis: verum
end;
 A c= Inter ((A ``1),(A ``2))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in Inter ((A ``1),(A ``2)) )
assume  x in A ; ::_thesis: x in Inter ((A ``1),(A ``2))
then  ( A ``1 c= x & x c= A ``2 ) by Th14;
hence  x in Inter ((A ``1),(A ``2)) by Th1; ::_thesis: verum
end;
hence  A = Inter ((A ``1),(A ``2)) by A1, XBOOLE_0:def_10; ::_thesis: verum
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
let U be non empty set ; ::_thesis: for A being non empty IntervalSet of U holds A ``1 c= A ``2
let A be non empty IntervalSet of U; ::_thesis: A ``1 c= A ``2
consider B being Subset of U such that
A1: A = Inter ((A ``1),B) by Def5;
consider C being Subset of U such that
A2: A = Inter (C,(A ``2)) by Def6;
 A ``1 = C by Th6, A2, A1;
hence  A ``1 c= A ``2 by Th5, A2; ::_thesis: verum
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
let U be non empty set ; ::_thesis: for A, B being non empty IntervalSet of U holds A _\/_ B = Inter (((A ``1) \/ (B ``1)),((A ``2) \/ (B ``2)))
let A, B be non empty IntervalSet of U; ::_thesis: A _\/_ B = Inter (((A ``1) \/ (B ``1)),((A ``2) \/ (B ``2)))
thus  A _\/_ B c= Inter (((A ``1) \/ (B ``1)),((A ``2) \/ (B ``2))) :: according to XBOOLE_0:def_10 ::_thesis: Inter (((A ``1) \/ (B ``1)),((A ``2) \/ (B ``2))) c= A _\/_ B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A _\/_ B or x in Inter (((A ``1) \/ (B ``1)),((A ``2) \/ (B ``2))) )
assume A1: x in A _\/_ B ; ::_thesis: x in Inter (((A ``1) \/ (B ``1)),((A ``2) \/ (B ``2)))
then consider X, Y being set  such that
A2: ( X in A & Y in B & x = X \/ Y ) by SETFAM_1:def_4;
A3: ( A ``1 c= X & X c= A ``2 ) by A2, Th14;
A4: ( B ``1 c= Y & Y c= B ``2 ) by A2, Th14;
then A5: x c= (A ``2) \/ (B ``2) by A3, A2, XBOOLE_1:13;
 (A ``1) \/ (B ``1) c= x by A3, A2, A4, XBOOLE_1:13;
hence  x in Inter (((A ``1) \/ (B ``1)),((A ``2) \/ (B ``2))) by A1, A5; ::_thesis: verum
end;
thus  Inter (((A ``1) \/ (B ``1)),((A ``2) \/ (B ``2))) c= A _\/_ B ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Inter (((A ``1) \/ (B ``1)),((A ``2) \/ (B ``2))) or x in A _\/_ B )
assume  x in Inter (((A ``1) \/ (B ``1)),((A ``2) \/ (B ``2))) ; ::_thesis: x in A _\/_ B
then consider Z being Element of bool U such that
A6: ( x = Z & (A ``1) \/ (B ``1) c= Z & Z c= (A ``2) \/ (B ``2) ) ;
 A ``1 c= (Z \/ (A ``1)) /\ (A ``2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A ``1 or x in (Z \/ (A ``1)) /\ (A ``2) )
assume A7: x in A ``1 ; ::_thesis: x in (Z \/ (A ``1)) /\ (A ``2)
assume A8: not x in (Z \/ (A ``1)) /\ (A ``2) ; ::_thesis: contradiction
percases ( not x in Z \/ (A ``1) or not x in A ``2 ) by A8, XBOOLE_0:def_4;
suppose not x in Z \/ (A ``1) ; ::_thesis: contradiction
hence  contradiction by A7, XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA9: not x in A ``2 ; ::_thesis: contradiction
 ( A ``1 c= A ``2 & x in A ``1 ) by A7, Th16;
hence  contradiction by A9; ::_thesis: verum
end;
end;
end;
then  ( A ``1 c= (Z \/ (A ``1)) /\ (A ``2) & (Z \/ (A ``1)) /\ (A ``2) c= A ``2 ) by XBOOLE_1:17;
then A10: (Z \/ (A ``1)) /\ (A ``2) in A by Th14;
 B ``1 c= (Z \/ (B ``1)) /\ (B ``2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B ``1 or x in (Z \/ (B ``1)) /\ (B ``2) )
assume A11: x in B ``1 ; ::_thesis: x in (Z \/ (B ``1)) /\ (B ``2)
then A12: x in Z \/ (B ``1) by XBOOLE_0:def_3;
 B ``1 c= B ``2 by Th16;
hence  x in (Z \/ (B ``1)) /\ (B ``2) by A11, A12, XBOOLE_0:def_4; ::_thesis: verum
end;
then  ( B ``1 c= (Z \/ (B ``1)) /\ (B ``2) & (Z \/ (B ``1)) /\ (B ``2) c= B ``2 ) by XBOOLE_1:17;
then A13: (Z \/ (B ``1)) /\ (B ``2) in B by Th14;
((Z \/ (A ``1)) /\ (A ``2)) \/ ((Z \/ (B ``1)) /\ (B ``2)) = (((Z \/ (A ``1)) /\ (A ``2)) \/ (Z \/ (B ``1))) /\ (((Z \/ (A ``1)) /\ (A ``2)) \/ (B ``2)) by XBOOLE_1:24
.= (((Z \/ (A ``1)) \/ (Z \/ (B ``1))) /\ ((A ``2) \/ (Z \/ (B ``1)))) /\ (((Z \/ (A ``1)) /\ (A ``2)) \/ (B ``2)) by XBOOLE_1:24
.= ((Z \/ ((A ``1) \/ (B ``1))) /\ ((A ``2) \/ (Z \/ (B ``1)))) /\ (((Z \/ (A ``1)) /\ (A ``2)) \/ (B ``2)) by XBOOLE_1:5
.= (Z /\ ((A ``2) \/ (Z \/ (B ``1)))) /\ (((Z \/ (A ``1)) /\ (A ``2)) \/ (B ``2)) by A6, XBOOLE_1:12
.= ((Z /\ (A ``2)) \/ (Z /\ (Z \/ (B ``1)))) /\ (((Z \/ (A ``1)) /\ (A ``2)) \/ (B ``2)) by XBOOLE_1:23
.= ((Z /\ (A ``2)) \/ Z) /\ (((Z \/ (A ``1)) /\ (A ``2)) \/ (B ``2)) by XBOOLE_1:7, XBOOLE_1:28
.= Z /\ ((B ``2) \/ ((Z \/ (A ``1)) /\ (A ``2))) by XBOOLE_1:12, XBOOLE_1:17
.= Z /\ (((Z \/ (A ``1)) \/ (B ``2)) /\ ((A ``2) \/ (B ``2))) by XBOOLE_1:24
.= Z /\ ((Z \/ ((A ``1) \/ (B ``2))) /\ ((A ``2) \/ (B ``2))) by XBOOLE_1:4
.= Z /\ ((Z /\ ((A ``2) \/ (B ``2))) \/ (((A ``1) \/ (B ``2)) /\ ((A ``2) \/ (B ``2)))) by XBOOLE_1:23
.= Z /\ (Z \/ (((A ``1) \/ (B ``2)) /\ ((A ``2) \/ (B ``2)))) by A6, XBOOLE_1:28
.= Z /\ ((Z \/ ((A ``1) \/ (B ``2))) /\ (Z \/ ((A ``2) \/ (B ``2)))) by XBOOLE_1:24
.= (Z /\ (Z \/ ((A ``1) \/ (B ``2)))) /\ (Z \/ ((A ``2) \/ (B ``2))) by XBOOLE_1:16
.= Z /\ (Z \/ ((A ``2) \/ (B ``2))) by XBOOLE_1:7, XBOOLE_1:28
.= Z by XBOOLE_1:7, XBOOLE_1:28 ;
then consider X, Y being Subset of U such that
A14: ( X in A & Y in B & Z = X \/ Y ) by A10, A13;
thus  x in A _\/_ B by A14, A6, SETFAM_1:def_4; ::_thesis: verum
end;
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
let U be non empty set ; ::_thesis: for A, B being non empty IntervalSet of U holds A _/\_ B = Inter (((A ``1) /\ (B ``1)),((A ``2) /\ (B ``2)))
let A, B be non empty IntervalSet of U; ::_thesis: A _/\_ B = Inter (((A ``1) /\ (B ``1)),((A ``2) /\ (B ``2)))
A1: A _/\_ B c= Inter (((A ``1) /\ (B ``1)),((A ``2) /\ (B ``2)))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A _/\_ B or x in Inter (((A ``1) /\ (B ``1)),((A ``2) /\ (B ``2))) )
assume  x in A _/\_ B ; ::_thesis: x in Inter (((A ``1) /\ (B ``1)),((A ``2) /\ (B ``2)))
then consider X, Y being set  such that
A2: ( X in A & Y in B & x = X /\ Y ) by SETFAM_1:def_5;
 ( A ``1 c= X & B ``1 c= Y & X c= A ``2 & Y c= B ``2 ) by A2, Th14;
then  ( (A ``1) /\ (B ``1) c= x & x c= (A ``2) /\ (B ``2) ) by A2, XBOOLE_1:27;
hence  x in Inter (((A ``1) /\ (B ``1)),((A ``2) /\ (B ``2))) by Th1; ::_thesis: verum
end;
 Inter (((A ``1) /\ (B ``1)),((A ``2) /\ (B ``2))) c= A _/\_ B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Inter (((A ``1) /\ (B ``1)),((A ``2) /\ (B ``2))) or x in A _/\_ B )
assume  x in Inter (((A ``1) /\ (B ``1)),((A ``2) /\ (B ``2))) ; ::_thesis: x in A _/\_ B
then consider Z being Element of bool U such that
A3: ( x = Z & (A ``1) /\ (B ``1) c= Z & Z c= (A ``2) /\ (B ``2) ) ;
 A ``1 c= (Z \/ (A ``1)) /\ (A ``2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A ``1 or x in (Z \/ (A ``1)) /\ (A ``2) )
assume A4: x in A ``1 ; ::_thesis: x in (Z \/ (A ``1)) /\ (A ``2)
assume A5: not x in (Z \/ (A ``1)) /\ (A ``2) ; ::_thesis: contradiction
percases ( not x in Z \/ (A ``1) or not x in A ``2 ) by A5, XBOOLE_0:def_4;
suppose not x in Z \/ (A ``1) ; ::_thesis: contradiction
hence  contradiction by A4, XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA6: not x in A ``2 ; ::_thesis: contradiction
 ( A ``1 c= A ``2 & x in A ``1 ) by A4, Th16;
hence  contradiction by A6; ::_thesis: verum
end;
end;
end;
then  ( A ``1 c= (Z \/ (A ``1)) /\ (A ``2) & (Z \/ (A ``1)) /\ (A ``2) c= A ``2 ) by XBOOLE_1:17;
then A7: (Z \/ (A ``1)) /\ (A ``2) in A by Th14;
 B ``1 c= (Z \/ (B ``1)) /\ (B ``2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B ``1 or x in (Z \/ (B ``1)) /\ (B ``2) )
assume A8: x in B ``1 ; ::_thesis: x in (Z \/ (B ``1)) /\ (B ``2)
then A9: x in Z \/ (B ``1) by XBOOLE_0:def_3;
 B ``1 c= B ``2 by Th16;
hence  x in (Z \/ (B ``1)) /\ (B ``2) by A8, A9, XBOOLE_0:def_4; ::_thesis: verum
end;
then  ( B ``1 c= (Z \/ (B ``1)) /\ (B ``2) & (Z \/ (B ``1)) /\ (B ``2) c= B ``2 ) by XBOOLE_1:17;
then A10: (Z \/ (B ``1)) /\ (B ``2) in B by Th14;
((Z \/ (A ``1)) /\ (A ``2)) /\ ((Z \/ (B ``1)) /\ (B ``2)) = (((A ``2) /\ (Z \/ (A ``1))) /\ (Z \/ (B ``1))) /\ (B ``2) by XBOOLE_1:16
.= ((A ``2) /\ ((Z \/ (A ``1)) /\ (Z \/ (B ``1)))) /\ (B ``2) by XBOOLE_1:16
.= ((A ``2) /\ (Z \/ ((A ``1) /\ (B ``1)))) /\ (B ``2) by XBOOLE_1:24
.= ((A ``2) /\ Z) /\ (B ``2) by A3, XBOOLE_1:12
.= Z /\ ((A ``2) /\ (B ``2)) by XBOOLE_1:16
.= Z by A3, XBOOLE_1:28 ;
hence  x in A _/\_ B by A3, A7, A10, SETFAM_1:def_5; ::_thesis: verum
end;
hence  A _/\_ B = Inter (((A ``1) /\ (B ``1)),((A ``2) /\ (B ``2))) by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

definition
let U be non empty set ;
let A, B be non empty IntervalSet of U;
:: original: =
redefine predA = 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
thus  ( A = B implies ( A ``1 = B ``1 & A ``2 = B ``2 ) ) ; ::_thesis: ( A ``1 = B ``1 & A ``2 = B ``2 implies A = B )
assume that
A1: A ``1 = B ``1 and
A2: A ``2 = B ``2 ; ::_thesis: A = B
A3: A c= B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in B )
assume A4: x in A ; ::_thesis: x in B
consider A1, B1 being Subset of U such that
A5: A = Inter (A1,B1) by Def2;
consider C1 being Subset of U such that
A6: A = Inter ((A ``1),C1) by Def5;
A7: A1 = B ``1 by A1, A5, Th6, A6;
consider C2 being Subset of U such that
A8: B = Inter ((B ``1),C2) by Def5;
consider D1 being Subset of U such that
A9: A = Inter (D1,(A ``2)) by Def6;
A10: B ``2 = B1 by A2, A9, A5, Th6;
consider D2 being Subset of U such that
A11: B = Inter (D2,(B ``2)) by Def6;
thus  x in B by A4, A5, A7, A8, A10, A11, Th6; ::_thesis: verum
end;
 B c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in A )
assume A12: x in B ; ::_thesis: x in A
consider A1, B1 being Subset of U such that
A13: B = Inter (A1,B1) by Def2;
consider C1 being Subset of U such that
A14: B = Inter ((B ``1),C1) by Def5;
A15: A ``1 = A1 by A1, A14, Th6, A13;
consider C2 being Subset of U such that
A16: A = Inter ((A ``1),C2) by Def5;
consider D1 being Subset of U such that
A17: B = Inter (D1,(B ``2)) by Def6;
A18: A ``2 = B1 by A2, A17, A13, Th6;
consider D2 being Subset of U such that
A19: A = Inter (D2,(A ``2)) by Def6;
thus  x in A by A12, A13, A15, A16, A18, A19, Th6; ::_thesis: verum
end;
hence  A = B by A3, XBOOLE_0:def_10; ::_thesis: verum
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
let U be non empty set ; ::_thesis: for A being non empty IntervalSet of U holds A _\/_ A = A
let A be non empty IntervalSet of U; ::_thesis: A _\/_ A = A
A1: A _\/_ A c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A _\/_ A or x in A )
assume  x in A _\/_ A ; ::_thesis: x in A
then consider X, Y being set  such that
A2: ( X in A & Y in A & x = X \/ Y ) by SETFAM_1:def_4;
A3: ( A ``1 c= X & X c= A ``2 ) by A2, Th14;
 ( A ``1 c= Y & Y c= A ``2 ) by A2, Th14;
then A4: X \/ Y c= A ``2 by A3, XBOOLE_1:8;
 X c= X \/ Y by XBOOLE_1:7;
then  A ``1 c= X \/ Y by A3, XBOOLE_1:1;
hence  x in A by Th14, A4, A2; ::_thesis: verum
end;
 A c= A _\/_ A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in A _\/_ A )
assume A5: x in A ; ::_thesis: x in A _\/_ A
 x = x \/ x ;
hence  x in A _\/_ A by A5, SETFAM_1:def_4; ::_thesis: verum
end;
hence  A _\/_ A = A by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: INTERVA1:20
for U being non empty set
for A being non empty IntervalSet of U holds A _/\_ A = A
proof
let U be non empty set ; ::_thesis: for A being non empty IntervalSet of U holds A _/\_ A = A
let A be non empty IntervalSet of U; ::_thesis: A _/\_ A = A
A1: A _/\_ A c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A _/\_ A or x in A )
assume  x in A _/\_ A ; ::_thesis: x in A
then consider X, Y being set  such that
A2: ( X in A & Y in A & x = X /\ Y ) by SETFAM_1:def_5;
A3: ( A ``1 c= X & X c= A ``2 ) by A2, Th14;
 ( A ``1 c= Y & Y c= A ``2 ) by A2, Th14;
then A4: A ``1 c= X /\ Y by A3, XBOOLE_1:19;
 X /\ Y c= X by XBOOLE_1:17;
then  X /\ Y c= A ``2 by A3, XBOOLE_1:1;
hence  x in A by A4, A2, Th14; ::_thesis: verum
end;
 A c= A _/\_ A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in A _/\_ A )
assume A5: x in A ; ::_thesis: x in A _/\_ A
 x = x /\ x ;
hence  x in A _/\_ A by A5, SETFAM_1:def_5; ::_thesis: verum
end;
hence  A _/\_ A = A by A1, XBOOLE_0:def_10; ::_thesis: verum
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
let U be non empty set ; ::_thesis: for A, B, C being non empty IntervalSet of U holds (A _\/_ B) _\/_ C = A _\/_ (B _\/_ C)
let A, B, C be non empty IntervalSet of U; ::_thesis: (A _\/_ B) _\/_ C = A _\/_ (B _\/_ C)
A1: (A _\/_ B) _\/_ C c= A _\/_ (B _\/_ C)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A _\/_ B) _\/_ C or x in A _\/_ (B _\/_ C) )
assume  x in (A _\/_ B) _\/_ C ; ::_thesis: x in A _\/_ (B _\/_ C)
then consider X, Y being set  such that
A2: ( X in UNION (A,B) & Y in C & x = X \/ Y ) by SETFAM_1:def_4;
consider Z, W being set  such that
A3: ( Z in A & W in B & X = Z \/ W ) by A2, SETFAM_1:def_4;
 W \/ Y in UNION (B,C) by A2, A3, SETFAM_1:def_4;
then  Z \/ (W \/ Y) in UNION (A,(UNION (B,C))) by A3, SETFAM_1:def_4;
hence  x in A _\/_ (B _\/_ C) by A2, A3, XBOOLE_1:4; ::_thesis: verum
end;
 A _\/_ (B _\/_ C) c= (A _\/_ B) _\/_ C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A _\/_ (B _\/_ C) or x in (A _\/_ B) _\/_ C )
assume  x in A _\/_ (B _\/_ C) ; ::_thesis: x in (A _\/_ B) _\/_ C
then consider X, Y being set  such that
A4: ( X in A & Y in UNION (B,C) & x = X \/ Y ) by SETFAM_1:def_4;
consider Z, W being set  such that
A5: ( Z in B & W in C & Y = Z \/ W ) by A4, SETFAM_1:def_4;
 X \/ Z in UNION (A,B) by A4, A5, SETFAM_1:def_4;
then  (X \/ Z) \/ W in UNION ((UNION (A,B)),C) by A5, SETFAM_1:def_4;
hence  x in (A _\/_ B) _\/_ C by A4, A5, XBOOLE_1:4; ::_thesis: verum
end;
hence  (A _\/_ B) _\/_ C = A _\/_ (B _\/_ C) by A1, XBOOLE_0:def_10; ::_thesis: verum
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
let U be non empty set ; ::_thesis: for A, B, C being non empty IntervalSet of U holds (A _/\_ B) _/\_ C = A _/\_ (B _/\_ C)
let A, B, C be non empty IntervalSet of U; ::_thesis: (A _/\_ B) _/\_ C = A _/\_ (B _/\_ C)
A1: (A _/\_ B) _/\_ C c= A _/\_ (B _/\_ C)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A _/\_ B) _/\_ C or x in A _/\_ (B _/\_ C) )
assume  x in (A _/\_ B) _/\_ C ; ::_thesis: x in A _/\_ (B _/\_ C)
then consider X, Y being set  such that
A2: ( X in INTERSECTION (A,B) & Y in C & x = X /\ Y ) by SETFAM_1:def_5;
consider Z, W being set  such that
A3: ( Z in A & W in B & X = Z /\ W ) by A2, SETFAM_1:def_5;
 W /\ Y in INTERSECTION (B,C) by A2, A3, SETFAM_1:def_5;
then  Z /\ (W /\ Y) in INTERSECTION (A,(INTERSECTION (B,C))) by A3, SETFAM_1:def_5;
hence  x in A _/\_ (B _/\_ C) by A2, A3, XBOOLE_1:16; ::_thesis: verum
end;
 A _/\_ (B _/\_ C) c= (A _/\_ B) _/\_ C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A _/\_ (B _/\_ C) or x in (A _/\_ B) _/\_ C )
assume  x in A _/\_ (B _/\_ C) ; ::_thesis: x in (A _/\_ B) _/\_ C
then consider X, Y being set  such that
A4: ( X in A & Y in INTERSECTION (B,C) & x = X /\ Y ) by SETFAM_1:def_5;
consider Z, W being set  such that
A5: ( Z in B & W in C & Y = Z /\ W ) by A4, SETFAM_1:def_5;
 X /\ Z in INTERSECTION (A,B) by A4, A5, SETFAM_1:def_5;
then  (X /\ Z) /\ W in INTERSECTION ((INTERSECTION (A,B)),C) by A5, SETFAM_1:def_5;
hence  x in (A _/\_ B) _/\_ C by A4, A5, XBOOLE_1:16; ::_thesis: verum
end;
hence  (A _/\_ B) _/\_ C = A _/\_ (B _/\_ C) by A1, XBOOLE_0:def_10; ::_thesis: verum
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
let X be set ; ::_thesis: for A, B, C being Subset-Family of X holds UNION (A,(INTERSECTION (B,C))) c= INTERSECTION ((UNION (A,B)),(UNION (A,C)))
let A, B, C be Subset-Family of X; ::_thesis: UNION (A,(INTERSECTION (B,C))) c= INTERSECTION ((UNION (A,B)),(UNION (A,C)))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in UNION (A,(INTERSECTION (B,C))) or x in INTERSECTION ((UNION (A,B)),(UNION (A,C))) )
assume  x in UNION (A,(INTERSECTION (B,C))) ; ::_thesis: x in INTERSECTION ((UNION (A,B)),(UNION (A,C)))
then consider X, Y being set  such that
A1: ( X in A & Y in INTERSECTION (B,C) & x = X \/ Y ) by SETFAM_1:def_4;
consider W, Z being set  such that
A2: ( W in B & Z in C & Y = W /\ Z ) by A1, SETFAM_1:def_5;
A3: x = (X \/ W) /\ (X \/ Z) by A1, A2, XBOOLE_1:24;
A4: X \/ W in UNION (A,B) by A1, A2, SETFAM_1:def_4;
 X \/ Z in UNION (A,C) by A1, A2, SETFAM_1:def_4;
hence  x in INTERSECTION ((UNION (A,B)),(UNION (A,C))) by A3, A4, SETFAM_1:def_5; ::_thesis: verum
end;

definition
let X be set ;
let F be Subset-Family of X;
attrF 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 for Element of K19(K19(X));
existence
 ex b1 being Subset-Family of X st
( not b1 is empty & b1 is ordered )
proof
reconsider F = {X} as Subset-Family of X by ZFMISC_1:68;
take  F ; ::_thesis: ( not F is empty & F is ordered )
 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 ) ) ) )
proof
take  X ; ::_thesis: ex B being set st
( X in F & B in F & ( for Y being set holds
( Y in F iff ( X c= Y & Y c= B ) ) ) )
take  X ; ::_thesis: ( X in F & X in F & ( for Y being set holds
( Y in F iff ( X c= Y & Y c= X ) ) ) )
thus  ( X in F & X in F ) by TARSKI:def_1; ::_thesis: for Y being set holds
( Y in F iff ( X c= Y & Y c= X ) )
let Y be set ; ::_thesis: ( Y in F iff ( X c= Y & Y c= X ) )
thus  ( Y in F implies ( X c= Y & Y c= X ) ) by TARSKI:def_1; ::_thesis: ( X c= Y & Y c= X implies Y in F )
assume  ( X c= Y & Y c= X ) ; ::_thesis: Y in F
then  X = Y by XBOOLE_0:def_10;
hence  Y in F by TARSKI:def_1; ::_thesis: verum
end;
hence  ( not F is empty & F is ordered ) by Def8; ::_thesis: verum
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
let U be non empty set ; ::_thesis: for A, B being Subset of U st A c= B holds
Inter (A,B) is non empty ordered Subset-Family of U
let A, B be Subset of U; ::_thesis: ( A c= B implies Inter (A,B) is non empty ordered Subset-Family of U )
assume A1: A c= B ; ::_thesis: Inter (A,B) is non empty ordered Subset-Family of U
consider C, D being set  such that
A2: ( C = A & D = B ) ;
 ( C in Inter (A,B) & D in Inter (A,B) & ( for Y being set holds
( Y in Inter (A,B) iff ( C c= Y & Y c= D ) ) ) ) by A2, Th1, A1;
hence  Inter (A,B) is non empty ordered Subset-Family of U by Def8; ::_thesis: verum
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
let U be non empty set ; ::_thesis: for A being non empty IntervalSet of U holds A is non empty ordered Subset-Family of U
let A be non empty IntervalSet of U; ::_thesis: A is non empty ordered Subset-Family of U
 ( A = Inter ((A ``1),(A ``2)) & A ``1 c= A ``2 ) by Th15, Th16;
hence  A is non empty ordered Subset-Family of U by Th25; ::_thesis: verum
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
consider A, B being set  such that
A1: ( A in F & B in F & ( for Y being set holds
( Y in F iff ( A c= Y & Y c= B ) ) ) ) by Def8;
 for Z1 being set st Z1 in F holds
A c= Z1 by A1;
then A2: A c= meet F by SETFAM_1:5;
 meet F c= B by A1, SETFAM_1:3;
hence  min F is Element of F by A1, A2; ::_thesis: verum
end;
:: original: max
redefine func max F ->  Element of F;
correctness
coherence
max F is Element of F;
proof
consider A, B being set  such that
A3: ( A in F & B in F & ( for Y being set holds
( Y in F iff ( A c= Y & Y c= B ) ) ) ) by Def8;
A4: for Z1 being set st Z1 in F holds
Z1 c= B by A3;
A5: A c= union F by A3, ZFMISC_1:74;
 union F c= B by A4, ZFMISC_1:76;
hence  max F is Element of F by A3, A5; ::_thesis: verum
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
let X be set ; ::_thesis: 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 )
let F be non empty ordered Subset-Family of X; ::_thesis: 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 )
let G be set ; ::_thesis: ( G in F implies ( G = min F iff for Y being set st Y in F holds
G c= Y ) )
assume A1: G in F ; ::_thesis: ( G = min F iff for Y being set st Y in F holds
G c= Y )
thus  ( G = min F implies for Y being set st Y in F holds
G c= Y ) by SETFAM_1:3; ::_thesis: ( ( for Y being set st Y in F holds
G c= Y ) implies G = min F )
assume  for Y being set st Y in F holds
G c= Y ; ::_thesis: G = min F
then A2: G c= min F ;
 min F c= G by A1, SETFAM_1:3;
hence  G = min F by A2, XBOOLE_0:def_10; ::_thesis: verum
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
let X be set ; ::_thesis: 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 )
let F be non empty ordered Subset-Family of X; ::_thesis: 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 )
let G be set ; ::_thesis: ( G in F implies ( G = max F iff for Y being set st Y in F holds
Y c= G ) )
assume A1: G in F ; ::_thesis: ( G = max F iff for Y being set st Y in F holds
Y c= G )
thus  ( G = max F implies for Y being set st Y in F holds
Y c= G ) by ZFMISC_1:74; ::_thesis: ( ( for Y being set st Y in F holds
Y c= G ) implies G = max F )
assume A2: for Y being set st Y in F holds
Y c= G ; ::_thesis: G = max F
A3: G c= max F by A1, ZFMISC_1:74;
 max F c= G by A2;
hence  G = max F by A3, XBOOLE_0:def_10; ::_thesis: verum
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
let U be non empty set ; ::_thesis: 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 )
let A, B be Subset of U; ::_thesis: for F being non empty ordered Subset-Family of U st F = Inter (A,B) holds
( min F = A & max F = B )
let F be non empty ordered Subset-Family of U; ::_thesis: ( F = Inter (A,B) implies ( min F = A & max F = B ) )
assume A1: F = Inter (A,B) ; ::_thesis: ( min F = A & max F = B )
then  ( A is Element of F & ( for Y being set st Y in F holds
A c= Y ) ) by Th2, Th1;
then A2: A = min F by Lm2;
 ( B is Element of F & ( for Y being set st Y in F holds
Y c= B ) ) by Th2, A1, Th1;
hence  ( min F = A & max F = B ) by A2, Lm3; ::_thesis: verum
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
let X, Y be set ; ::_thesis: for A being non empty ordered Subset-Family of X holds
( Y in A iff ( min A c= Y & Y c= max A ) )
let A be non empty ordered Subset-Family of X; ::_thesis: ( Y in A iff ( min A c= Y & Y c= max A ) )
 ( min A c= Y & Y c= max A implies Y in A )
proof
assume A1: ( min A c= Y & Y c= max A ) ; ::_thesis: Y in A
consider C, D being set  such that
A2: ( C in A & D in A & ( for X being set holds
( X in A iff ( C c= X & X c= D ) ) ) ) by Def8;
A3: ( min A c= C & D c= max A ) by Lm2, Lm3, A2;
 ( C c= min A & max A c= D ) by A2;
then  ( min A = C & max A = D ) by A3, XBOOLE_0:def_10;
hence  Y in A by A2, A1; ::_thesis: verum
end;
hence  ( Y in A iff ( min A c= Y & Y c= max A ) ) by Lm2, Lm3; ::_thesis: verum
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
let X be set ; ::_thesis: 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)))
let A, B, C be non empty ordered Subset-Family of X; ::_thesis: UNION (A,(INTERSECTION (B,C))) = INTERSECTION ((UNION (A,B)),(UNION (A,C)))
A1: UNION (A,(INTERSECTION (B,C))) c= INTERSECTION ((UNION (A,B)),(UNION (A,C))) by Lm1;
 INTERSECTION ((UNION (A,B)),(UNION (A,C))) c= UNION (A,(INTERSECTION (B,C)))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in INTERSECTION ((UNION (A,B)),(UNION (A,C))) or x in UNION (A,(INTERSECTION (B,C))) )
assume  x in INTERSECTION ((UNION (A,B)),(UNION (A,C))) ; ::_thesis: x in UNION (A,(INTERSECTION (B,C)))
then consider X, Y being set  such that
A2: ( X in UNION (A,B) & Y in UNION (A,C) & x = X /\ Y ) by SETFAM_1:def_5;
consider X1, X2 being set  such that
A3: ( X1 in A & X2 in B & X = X1 \/ X2 ) by A2, SETFAM_1:def_4;
consider Y1, Y2 being set  such that
A4: ( Y1 in A & Y2 in C & Y = Y1 \/ Y2 ) by A2, SETFAM_1:def_4;
A5: x = (X1 /\ (Y1 \/ Y2)) \/ (X2 /\ (Y1 \/ Y2)) by A2, A3, A4, XBOOLE_1:23
.= ((X1 /\ Y1) \/ (X1 /\ Y2)) \/ (X2 /\ (Y1 \/ Y2)) by XBOOLE_1:23
.= ((X1 /\ Y1) \/ (X1 /\ Y2)) \/ ((X2 /\ Y1) \/ (X2 /\ Y2)) by XBOOLE_1:23
.= (((X1 /\ Y1) \/ (X1 /\ Y2)) \/ (X2 /\ Y1)) \/ (X2 /\ Y2) by XBOOLE_1:4 ;
set A1 = min A;
set A2 = max A;
 ( min A c= X1 & X1 c= max A & min A c= Y1 & Y1 c= max A ) by A3, A4, Th28;
then A6: ( (min A) /\ (min A) c= X1 /\ Y1 & X1 /\ Y1 c= (max A) /\ (max A) ) by XBOOLE_1:27;
 ( Y1 c= max A & X2 /\ Y1 c= Y1 ) by A4, Th28, XBOOLE_1:17;
then  X2 /\ Y1 c= max A by XBOOLE_1:1;
then A7: ( min A c= (X1 /\ Y1) \/ (X2 /\ Y1) & (X1 /\ Y1) \/ (X2 /\ Y1) c= max A ) by A6, XBOOLE_1:8, XBOOLE_1:10;
 ( X1 c= max A & X1 /\ Y2 c= X1 ) by A3, Th28, XBOOLE_1:17;
then  X1 /\ Y2 c= max A by XBOOLE_1:1;
then  ((X1 /\ Y1) \/ (X2 /\ Y1)) \/ (X1 /\ Y2) c= max A by A7, XBOOLE_1:8;
then  ( min A c= ((X1 /\ Y1) \/ (X2 /\ Y1)) \/ (X1 /\ Y2) & ((X1 /\ Y1) \/ (X1 /\ Y2)) \/ (X2 /\ Y1) c= max A ) by A7, XBOOLE_1:4, XBOOLE_1:10;
then  ( min A c= ((X1 /\ Y1) \/ (X1 /\ Y2)) \/ (X2 /\ Y1) & ((X1 /\ Y1) \/ (X1 /\ Y2)) \/ (X2 /\ Y1) c= max A ) by XBOOLE_1:4;
then A8: ((X1 /\ Y1) \/ (X1 /\ Y2)) \/ (X2 /\ Y1) in A by Th28;
 X2 /\ Y2 in INTERSECTION (B,C) by A3, A4, SETFAM_1:def_5;
hence  x in UNION (A,(INTERSECTION (B,C))) by A8, A5, SETFAM_1:def_4; ::_thesis: verum
end;
hence  UNION (A,(INTERSECTION (B,C))) = INTERSECTION ((UNION (A,B)),(UNION (A,C))) by A1, XBOOLE_0:def_10; ::_thesis: verum
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
let X be set ; ::_thesis: for A, B, C being Subset-Family of X holds INTERSECTION (A,(UNION (B,C))) c= UNION ((INTERSECTION (A,B)),(INTERSECTION (A,C)))
let A, B, C be Subset-Family of X; ::_thesis: INTERSECTION (A,(UNION (B,C))) c= UNION ((INTERSECTION (A,B)),(INTERSECTION (A,C)))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in INTERSECTION (A,(UNION (B,C))) or x in UNION ((INTERSECTION (A,B)),(INTERSECTION (A,C))) )
assume  x in INTERSECTION (A,(UNION (B,C))) ; ::_thesis: x in UNION ((INTERSECTION (A,B)),(INTERSECTION (A,C)))
then consider X, Y being set  such that
A1: ( X in A & Y in UNION (B,C) & x = X /\ Y ) by SETFAM_1:def_5;
consider Z, W being set  such that
A2: ( Z in B & W in C & Y = Z \/ W ) by A1, SETFAM_1:def_4;
A3: x = (X /\ Z) \/ (X /\ W) by A1, A2, XBOOLE_1:23;
A4: X /\ Z in INTERSECTION (A,B) by A1, A2, SETFAM_1:def_5;
 X /\ W in INTERSECTION (A,C) by A1, A2, SETFAM_1:def_5;
hence  x in UNION ((INTERSECTION (A,B)),(INTERSECTION (A,C))) by A3, A4, SETFAM_1:def_4; ::_thesis: verum
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
let X be set ; ::_thesis: 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)))
let A, B, C be non empty ordered Subset-Family of X; ::_thesis: INTERSECTION (A,(UNION (B,C))) = UNION ((INTERSECTION (A,B)),(INTERSECTION (A,C)))
A1: INTERSECTION (A,(UNION (B,C))) c= UNION ((INTERSECTION (A,B)),(INTERSECTION (A,C))) by Lm5;
 UNION ((INTERSECTION (A,B)),(INTERSECTION (A,C))) c= INTERSECTION (A,(UNION (B,C)))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in UNION ((INTERSECTION (A,B)),(INTERSECTION (A,C))) or x in INTERSECTION (A,(UNION (B,C))) )
assume  x in UNION ((INTERSECTION (A,B)),(INTERSECTION (A,C))) ; ::_thesis: x in INTERSECTION (A,(UNION (B,C)))
then consider X, Y being set  such that
A2: ( X in INTERSECTION (A,B) & Y in INTERSECTION (A,C) & x = X \/ Y ) by SETFAM_1:def_4;
consider X1, X2 being set  such that
A3: ( X1 in A & X2 in B & X = X1 /\ X2 ) by A2, SETFAM_1:def_5;
consider Y1, Y2 being set  such that
A4: ( Y1 in A & Y2 in C & Y = Y1 /\ Y2 ) by A2, SETFAM_1:def_5;
A5: x = ((X1 /\ X2) \/ Y1) /\ ((X1 /\ X2) \/ Y2) by A2, A3, A4, XBOOLE_1:24
.= (Y1 \/ (X1 /\ X2)) /\ ((Y2 \/ X1) /\ (Y2 \/ X2)) by XBOOLE_1:24
.= ((Y1 \/ X1) /\ (Y1 \/ X2)) /\ ((Y2 \/ X1) /\ (Y2 \/ X2)) by XBOOLE_1:24
.= (((Y1 \/ X1) /\ (Y1 \/ X2)) /\ (Y2 \/ X1)) /\ (Y2 \/ X2) by XBOOLE_1:16 ;
set A1 = min A;
set A2 = max A;
A6: ( min A c= Y1 & min A c= X1 ) by A3, A4, Th28;
then A7: (min A) \/ (min A) c= Y1 \/ X1 by XBOOLE_1:13;
 Y1 c= Y1 \/ X2 by XBOOLE_1:7;
then  min A c= Y1 \/ X2 by A6, XBOOLE_1:1;
then A8: (min A) /\ (min A) c= (Y1 \/ X1) /\ (Y1 \/ X2) by A7, XBOOLE_1:27;
 ( min A c= X1 & X1 c= Y2 \/ X1 ) by Th28, A3, XBOOLE_1:7;
then  min A c= Y2 \/ X1 by XBOOLE_1:1;
then A9: min A c= ((Y1 \/ X1) /\ (Y1 \/ X2)) /\ (Y2 \/ X1) by A8, XBOOLE_1:19;
 ( Y1 c= max A & X1 c= max A ) by A3, A4, Th28;
then  ( (Y1 \/ X1) /\ ((Y1 \/ X2) /\ (Y2 \/ X1)) c= Y1 \/ X1 & Y1 \/ X1 c= max A ) by XBOOLE_1:8, XBOOLE_1:17;
then  ( min A c= ((Y1 \/ X1) /\ (Y1 \/ X2)) /\ (Y2 \/ X1) & (Y1 \/ X1) /\ ((Y1 \/ X2) /\ (Y2 \/ X1)) c= max A ) by A9, XBOOLE_1:1;
then  ( min A c= ((Y1 \/ X1) /\ (Y1 \/ X2)) /\ (Y2 \/ X1) & ((Y1 \/ X1) /\ (Y1 \/ X2)) /\ (Y2 \/ X1) c= max A ) by XBOOLE_1:16;
then A10: ((Y1 \/ X1) /\ (Y1 \/ X2)) /\ (Y2 \/ X1) in A by Th28;
 Y2 \/ X2 in UNION (B,C) by A3, A4, SETFAM_1:def_4;
hence  x in INTERSECTION (A,(UNION (B,C))) by A5, A10, SETFAM_1:def_5; ::_thesis: verum
end;
hence  INTERSECTION (A,(UNION (B,C))) = UNION ((INTERSECTION (A,B)),(INTERSECTION (A,C))) by A1, XBOOLE_0:def_10; ::_thesis: verum
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
let U be non empty set ; ::_thesis: for A, B, C being non empty IntervalSet of U holds A _\/_ (B _/\_ C) = (A _\/_ B) _/\_ (A _\/_ C)
let A, B, C be non empty IntervalSet of U; ::_thesis: A _\/_ (B _/\_ C) = (A _\/_ B) _/\_ (A _\/_ C)
A1: A _\/_ (B _/\_ C) c= (A _\/_ B) _/\_ (A _\/_ C) by Lm1;
 (A _\/_ B) _/\_ (A _\/_ C) c= A _\/_ (B _/\_ C)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A _\/_ B) _/\_ (A _\/_ C) or x in A _\/_ (B _/\_ C) )
assume  x in (A _\/_ B) _/\_ (A _\/_ C) ; ::_thesis: x in A _\/_ (B _/\_ C)
then consider X, Y being set  such that
A2: ( X in UNION (A,B) & Y in UNION (A,C) & x = X /\ Y ) by SETFAM_1:def_5;
A3: ( A is non empty ordered Subset-Family of U & B is non empty ordered Subset-Family of U & C is non empty ordered Subset-Family of U ) by Lm4;
 x in INTERSECTION ((UNION (A,B)),(UNION (A,C))) by A2, SETFAM_1:def_5;
hence  x in A _\/_ (B _/\_ C) by Th29, A3; ::_thesis: verum
end;
hence  A _\/_ (B _/\_ C) = (A _\/_ B) _/\_ (A _\/_ C) by A1, XBOOLE_0:def_10; ::_thesis: verum
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
let U be non empty set ; ::_thesis: for A, B, C being non empty IntervalSet of U holds A _/\_ (B _\/_ C) = (A _/\_ B) _\/_ (A _/\_ C)
let A, B, C be non empty IntervalSet of U; ::_thesis: A _/\_ (B _\/_ C) = (A _/\_ B) _\/_ (A _/\_ C)
A1: A _/\_ (B _\/_ C) c= (A _/\_ B) _\/_ (A _/\_ C)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A _/\_ (B _\/_ C) or x in (A _/\_ B) _\/_ (A _/\_ C) )
assume  x in A _/\_ (B _\/_ C) ; ::_thesis: x in (A _/\_ B) _\/_ (A _/\_ C)
then consider X, Y being set  such that
A2: ( X in A & Y in UNION (B,C) & x = X /\ Y ) by SETFAM_1:def_5;
consider Z, W being set  such that
A3: ( Z in B & W in C & Y = Z \/ W ) by A2, SETFAM_1:def_4;
A4: ( A is non empty ordered Subset-Family of U & B is non empty ordered Subset-Family of U & C is non empty ordered Subset-Family of U ) by Lm4;
 X /\ (Z \/ W) in INTERSECTION (A,(UNION (B,C))) by A2, A3, SETFAM_1:def_5;
hence  x in (A _/\_ B) _\/_ (A _/\_ C) by A2, A3, Th30, A4; ::_thesis: verum
end;
 (A _/\_ B) _\/_ (A _/\_ C) c= A _/\_ (B _\/_ C)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A _/\_ B) _\/_ (A _/\_ C) or x in A _/\_ (B _\/_ C) )
assume  x in (A _/\_ B) _\/_ (A _/\_ C) ; ::_thesis: x in A _/\_ (B _\/_ C)
then consider X, Y being set  such that
A5: ( X in INTERSECTION (A,B) & Y in INTERSECTION (A,C) & x = X \/ Y ) by SETFAM_1:def_4;
A6: ( A is non empty ordered Subset-Family of U & B is non empty ordered Subset-Family of U & C is non empty ordered Subset-Family of U ) by Lm4;
 x in UNION ((INTERSECTION (A,B)),(INTERSECTION (A,C))) by A5, SETFAM_1:def_4;
hence  x in A _/\_ (B _\/_ C) by Th30, A6; ::_thesis: verum
end;
hence  A _/\_ (B _\/_ C) = (A _/\_ B) _\/_ (A _/\_ C) by A1, XBOOLE_0:def_10; ::_thesis: verum
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
let X be set ; ::_thesis: for A, B being non empty ordered Subset-Family of X holds INTERSECTION (A,(UNION (A,B))) = A
let A, B be non empty ordered Subset-Family of X; ::_thesis: INTERSECTION (A,(UNION (A,B))) = A
set A1 = min A;
set A2 = max A;
A1: INTERSECTION (A,(UNION (A,B))) c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in INTERSECTION (A,(UNION (A,B))) or x in A )
assume  x in INTERSECTION (A,(UNION (A,B))) ; ::_thesis: x in A
then consider Y, Z being set  such that
A2: ( Y in A & Z in UNION (A,B) & x = Y /\ Z ) by SETFAM_1:def_5;
consider Z1, Z2 being set  such that
A3: ( Z1 in A & Z2 in B & Z = Z1 \/ Z2 ) by A2, SETFAM_1:def_4;
A4: x = (Y /\ Z1) \/ (Y /\ Z2) by A2, A3, XBOOLE_1:23;
A5: ( min A c= Y & Y c= max A & min A c= Z1 & Z1 c= max A ) by Th28, A2, A3;
then  ( min A c= Y /\ Z1 & Y /\ Z1 c= (max A) /\ (max A) ) by XBOOLE_1:19, XBOOLE_1:27;
then A6: ( min A c= Y /\ Z1 & Y /\ Z1 c= max A & Y /\ Z1 c= (Y /\ Z1) \/ (Y /\ Z2) ) by XBOOLE_1:7;
then A7: min A c= (Y /\ Z1) \/ (Y /\ Z2) by XBOOLE_1:1;
 Y /\ Z2 c= Y by XBOOLE_1:17;
then  Y /\ Z2 c= max A by A5, XBOOLE_1:1;
then  (Y /\ Z1) \/ (Y /\ Z2) c= max A by A6, XBOOLE_1:8;
hence  x in A by Th28, A4, A7; ::_thesis: verum
end;
 A c= INTERSECTION (A,(UNION (A,B)))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in INTERSECTION (A,(UNION (A,B))) )
assume A8: x in A ; ::_thesis: x in INTERSECTION (A,(UNION (A,B)))
set b = the Element of B;
A9: x = x /\ (x \/ the Element of B) by XBOOLE_1:21;
 x \/ the Element of B in UNION (A,B) by A8, SETFAM_1:def_4;
hence  x in INTERSECTION (A,(UNION (A,B))) by A8, A9, SETFAM_1:def_5; ::_thesis: verum
end;
hence  INTERSECTION (A,(UNION (A,B))) = A by A1, XBOOLE_0:def_10; ::_thesis: verum
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
let X be set ; ::_thesis: for A, B being non empty ordered Subset-Family of X holds UNION ((INTERSECTION (A,B)),B) = B
let A, B be non empty ordered Subset-Family of X; ::_thesis: UNION ((INTERSECTION (A,B)),B) = B
A1: UNION ((INTERSECTION (A,B)),B) c= B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in UNION ((INTERSECTION (A,B)),B) or x in B )
set B1 = min B;
set B2 = max B;
assume  x in UNION ((INTERSECTION (A,B)),B) ; ::_thesis: x in B
then consider Y, Z being set  such that
A2: ( Y in INTERSECTION (A,B) & Z in B & x = Y \/ Z ) by SETFAM_1:def_4;
consider Y1, Y2 being set  such that
A3: ( Y1 in A & Y2 in B & Y = Y1 /\ Y2 ) by A2, SETFAM_1:def_5;
 ( min B c= Y2 & Y2 c= max B & Y1 /\ Y2 c= Y2 ) by A3, Th28, XBOOLE_1:17;
then A4: Y1 /\ Y2 c= max B by XBOOLE_1:1;
 Z c= max B by A2, Th28;
then A5: x c= max B by A2, A3, A4, XBOOLE_1:8;
 ( min B c= Z & Z c= x ) by A2, Th28, XBOOLE_1:7;
then  ( min B c= x & x c= max B ) by A5, XBOOLE_1:1;
hence  x in B by Th28; ::_thesis: verum
end;
 B c= UNION ((INTERSECTION (A,B)),B)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in UNION ((INTERSECTION (A,B)),B) )
assume A6: x in B ; ::_thesis: x in UNION ((INTERSECTION (A,B)),B)
set b = the Element of A;
A7: x = x \/ (x /\ the Element of A) by XBOOLE_1:22;
 the Element of A /\ x in INTERSECTION (A,B) by A6, SETFAM_1:def_5;
hence  x in UNION ((INTERSECTION (A,B)),B) by A7, A6, SETFAM_1:def_4; ::_thesis: verum
end;
hence  UNION ((INTERSECTION (A,B)),B) = B by A1, XBOOLE_0:def_10; ::_thesis: verum
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
let U be non empty set ; ::_thesis: for A, B being non empty IntervalSet of U holds A _/\_ (A _\/_ B) = A
let A, B be non empty IntervalSet of U; ::_thesis: A _/\_ (A _\/_ B) = A
 ( A is non empty ordered Subset-Family of U & B is non empty ordered Subset-Family of U ) by Lm4;
hence  A _/\_ (A _\/_ B) = A by Th33; ::_thesis: verum
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
let U be non empty set ; ::_thesis: for A, B being non empty IntervalSet of U holds (A _/\_ B) _\/_ B = B
let A, B be non empty IntervalSet of U; ::_thesis: (A _/\_ B) _\/_ B = B
 ( A is non empty ordered Subset-Family of U & B is non empty ordered Subset-Family of U ) by Lm4;
hence  (A _/\_ B) _\/_ B = B by Th34; ::_thesis: verum
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
let U be non empty set ; ::_thesis: for A, B being Subset-Family of U holds DIFFERENCE (A,B) is Subset-Family of U
let A, B be Subset-Family of U; ::_thesis: DIFFERENCE (A,B) is Subset-Family of U
 DIFFERENCE (A,B) c= bool U
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in DIFFERENCE (A,B) or x in bool U )
assume  x in DIFFERENCE (A,B) ; ::_thesis: x in bool U
then consider Y, Z being set  such that
A1: ( Y in A & Z in B & x = Y \ Z ) by SETFAM_1:def_6;
 Y \ Z c= U by A1, XBOOLE_1:109;
hence  x in bool U by A1; ::_thesis: verum
end;
hence  DIFFERENCE (A,B) is Subset-Family of U ; ::_thesis: verum
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
let U be non empty set ; ::_thesis: 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) )  }
let A, B be non empty ordered Subset-Family of U; ::_thesis: DIFFERENCE (A,B) =  {  C where C is Subset of U : ( (min A) \ (max B) c= C & C c= (max A) \ (min B) )  }
set A1 = min A;
set B1 = min B;
set A2 = max A;
set B2 = max B;
A1: DIFFERENCE (A,B) c=  {  C where C is Subset of U : ( (min A) \ (max B) c= C & C c= (max A) \ (min B) )  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in DIFFERENCE (A,B) or x in  {  C where C is Subset of U : ( (min A) \ (max B) c= C & C c= (max A) \ (min B) )  }  )
assume A2: x in DIFFERENCE (A,B) ; ::_thesis: x in  {  C where C is Subset of U : ( (min A) \ (max B) c= C & C c= (max A) \ (min B) )  }
then consider Y, Z being set  such that
A3: ( Y in A & Z in B & x = Y \ Z ) by SETFAM_1:def_6;
 DIFFERENCE (A,B) is Subset-Family of U by Th37;
then reconsider x = x as Subset of U by A2;
 ( min A c= Y & Y c= max A & min B c= Z & Z c= max B ) by A3, Th28;
then  ( (min A) \ (max B) c= x & x c= (max A) \ (min B) ) by A3, XBOOLE_1:35;
hence  x in  {  C where C is Subset of U : ( (min A) \ (max B) c= C & C c= (max A) \ (min B) )  }  ; ::_thesis: verum
end;
  {  C where C is Subset of U : ( (min A) \ (max B) c= C & C c= (max A) \ (min B) )  }  c= DIFFERENCE (A,B)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  C where C is Subset of U : ( (min A) \ (max B) c= C & C c= (max A) \ (min B) )  }  or x in DIFFERENCE (A,B) )
assume  x in  {  C where C is Subset of U : ( (min A) \ (max B) c= C & C c= (max A) \ (min B) )  }  ; ::_thesis: x in DIFFERENCE (A,B)
then consider x9 being Subset of U such that
A4: ( x9 = x & (min A) \ (max B) c= x9 & x9 c= (max A) \ (min B) ) ;
set A1 = min A;
set A2 = max A;
set B1 = min B;
set B2 = max B;
set z1 = (x9 \/ (min A)) /\ (max A);
set z2 = ((x9 \/ ((max B) `)) /\ ((min B) `)) ` ;
 min B c= max B by Lm2;
then A5: (max B) ` c= (min B) ` by SUBSET_1:12;
(x9 \/ ((max B) `)) /\ ((min B) `) = (x9 /\ ((min B) `)) \/ (((max B) `) /\ ((min B) `)) by XBOOLE_1:23
.= (x9 /\ ((min B) `)) \/ ((max B) `) by A5, XBOOLE_1:28 ;
then A6: (max B) ` c= (x9 \/ ((max B) `)) /\ ((min B) `) by XBOOLE_1:7;
 (x9 \/ ((max B) `)) /\ ((min B) `) c= (min B) ` by XBOOLE_1:17;
then A7: ( ((x9 \/ ((max B) `)) /\ ((min B) `)) ` c= ((max B) `) ` & ((min B) `) ` c= ((x9 \/ ((max B) `)) /\ ((min B) `)) ` ) by A6, SUBSET_1:12;
(x9 \/ (min A)) /\ (max A) = (x9 /\ (max A)) \/ ((min A) /\ (max A)) by XBOOLE_1:23
.= (x9 /\ (max A)) \/ (min A) by SETFAM_1:2, XBOOLE_1:28 ;
then  ( min A c= (x9 \/ (min A)) /\ (max A) & (x9 \/ (min A)) /\ (max A) c= max A ) by XBOOLE_1:7, XBOOLE_1:17;
then A8: ( (x9 \/ (min A)) /\ (max A) in A & ((x9 \/ ((max B) `)) /\ ((min B) `)) ` in B ) by Th28, A7;
A9: (x9 \/ ((min A) \ (max B))) /\ ((max A) \ (min B)) = x9 /\ ((max A) \ (min B)) by A4, XBOOLE_1:12
.= x9 by A4, XBOOLE_1:28 ;
((x9 \/ (min A)) /\ (max A)) \ (((x9 \/ ((max B) `)) /\ ((min B) `)) `) = ((x9 \/ (min A)) /\ (max A)) /\ ((((x9 \/ ((max B) `)) /\ ((min B) `)) `) `) by SUBSET_1:13
.= (x9 \/ (min A)) /\ ((max A) /\ ((x9 \/ ((max B) `)) /\ ((min B) `))) by XBOOLE_1:16
.= (x9 \/ (min A)) /\ ((x9 \/ ((max B) `)) /\ (((min B) `) /\ (max A))) by XBOOLE_1:16
.= (x9 \/ (min A)) /\ ((x9 \/ ((max B) `)) /\ ((max A) \ (min B))) by SUBSET_1:13
.= ((x9 \/ (min A)) /\ (x9 \/ ((max B) `))) /\ ((max A) \ (min B)) by XBOOLE_1:16
.= (x9 \/ ((min A) /\ ((max B) `))) /\ ((max A) \ (min B)) by XBOOLE_1:24
.= x9 by A9, SUBSET_1:13 ;
hence  x in DIFFERENCE (A,B) by A4, A8, SETFAM_1:def_6; ::_thesis: verum
end;
hence  DIFFERENCE (A,B) =  {  C where C is Subset of U : ( (min A) \ (max B) c= C & C c= (max A) \ (min B) )  }  by A1, XBOOLE_0:def_10; ::_thesis: verum
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
let U be non empty set ; ::_thesis: 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 )  }
let A1, A2, B1, B2 be Subset of U; ::_thesis: ( A1 c= A2 & B1 c= B2 implies DIFFERENCE ((Inter (A1,A2)),(Inter (B1,B2))) =  {  C where C is Subset of U : ( A1 \ B2 c= C & C c= A2 \ B1 )  }  )
assume  ( A1 c= A2 & B1 c= B2 ) ; ::_thesis: DIFFERENCE ((Inter (A1,A2)),(Inter (B1,B2))) =  {  C where C is Subset of U : ( A1 \ B2 c= C & C c= A2 \ B1 )  }
then reconsider A12 = Inter (A1,A2), B12 = Inter (B1,B2) as non empty ordered Subset-Family of U by Th25;
A1: ( min A12 = A1 & max A12 = A2 ) by Th27;
 ( min B12 = B1 & max B12 = B2 ) by Th27;
hence  DIFFERENCE ((Inter (A1,A2)),(Inter (B1,B2))) =  {  C where C is Subset of U : ( A1 \ B2 c= C & C c= A2 \ B1 )  }  by Th38, A1; ::_thesis: verum
end;

definition
let U be non empty set ;
let A, B be non empty IntervalSet of U;
funcA _\_ B ->  IntervalSet of U equals :: INTERVA1:def 9
 DIFFERENCE (A,B);
coherence
 DIFFERENCE (A,B) is IntervalSet of U
proof
set IT = DIFFERENCE (A,B);
consider A1, A2 being Subset of U such that
A1: ( A1 c= A2 & A = Inter (A1,A2) ) by Th11;
consider B1, B2 being Subset of U such that
A2: ( B1 c= B2 & B = Inter (B1,B2) ) by Th11;
set LAB = A1 \ B2;
set UAB = A2 \ B1;
 DIFFERENCE (A,B) = Inter ((A1 \ B2),(A2 \ B1)) by Th39, A1, A2;
hence  DIFFERENCE (A,B) is IntervalSet of U ; ::_thesis: verum
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;
clusterA _\_ B ->  non empty ;
coherence
 not A _\_ B is empty
proof
 A _\_ B <> {}
proof
assume A1: A _\_ B = {} ; ::_thesis: contradiction
consider A1, A2 being Subset of U such that
A2: ( A1 c= A2 & A = Inter (A1,A2) ) by Th11;
consider B1, B2 being Subset of U such that
A3: ( B1 c= B2 & B = Inter (B1,B2) ) by Th11;
consider y being set  such that
A4: y = A1 \ B1 ;
 ( not A1 in A or not B1 in B or not y = A1 \ B1 ) by A1, SETFAM_1:def_6;
hence  contradiction by A4, A2, A3; ::_thesis: verum
end;
hence  not A _\_ B is empty ; ::_thesis: verum
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
let U be non empty set ; ::_thesis: for A, B being non empty IntervalSet of U holds A _\_ B = Inter (((A ``1) \ (B ``2)),((A ``2) \ (B ``1)))
let A, B be non empty IntervalSet of U; ::_thesis: A _\_ B = Inter (((A ``1) \ (B ``2)),((A ``2) \ (B ``1)))
reconsider AA = A, BB = B as non empty ordered Subset-Family of U by Th26;
 ( AA = Inter ((A ``1),(A ``2)) & BB = Inter ((B ``1),(B ``2)) ) by Th15;
then  ( min AA = A ``1 & min BB = B ``1 & max AA = A ``2 & max BB = B ``2 ) by Th27;
hence  A _\_ B = Inter (((A ``1) \ (B ``2)),((A ``2) \ (B ``1))) by Th38; ::_thesis: verum
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
let U be non empty set ; ::_thesis: 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)))
let A, C be non empty IntervalSet of U; ::_thesis: for X, Y being Subset of U st A = Inter (X,Y) holds
A _\_ C = Inter ((X \ (C ``2)),(Y \ (C ``1)))
let X, Y be Subset of U; ::_thesis: ( A = Inter (X,Y) implies A _\_ C = Inter ((X \ (C ``2)),(Y \ (C ``1))) )
assume A1: A = Inter (X,Y) ; ::_thesis: A _\_ C = Inter ((X \ (C ``2)),(Y \ (C ``1)))
 A = Inter ((A ``1),(A ``2)) by Th15;
then  ( X = A ``1 & Y = A ``2 ) by A1, Th6;
hence  A _\_ C = Inter ((X \ (C ``2)),(Y \ (C ``1))) by Th40; ::_thesis: verum
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
let U be non empty set ; ::_thesis: 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))
let A, C be non empty IntervalSet of U; ::_thesis: 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))
let X, Y, W, Z be Subset of U; ::_thesis: ( A = Inter (X,Y) & C = Inter (W,Z) implies A _\_ C = Inter ((X \ Z),(Y \ W)) )
assume A1: ( A = Inter (X,Y) & C = Inter (W,Z) ) ; ::_thesis: A _\_ C = Inter ((X \ Z),(Y \ W))
 ( A = Inter ((A ``1),(A ``2)) & C = Inter ((C ``1),(C ``2)) ) by Th15;
then  ( A ``1 = X & A ``2 = Y & C ``1 = W & C ``2 = Z ) by A1, Th6;
hence  A _\_ C = Inter ((X \ Z),(Y \ W)) by Th40; ::_thesis: verum
end;

theorem Th43: :: INTERVA1:43
for U being non empty set holds Inter (([#] U),([#] U)) is non empty IntervalSet of U
proof
let U be non empty set ; ::_thesis: Inter (([#] U),([#] U)) is non empty IntervalSet of U
 Inter (([#] U),([#] U)) = {([#] U)} by Th8;
hence  Inter (([#] U),([#] U)) is non empty IntervalSet of U ; ::_thesis: verum
end;

theorem Th44: :: INTERVA1:44
for U being non empty set holds Inter (({} U),({} U)) is non empty IntervalSet of U
proof
let U be non empty set ; ::_thesis: Inter (({} U),({} U)) is non empty IntervalSet of U
 Inter (({} U),({} U)) = {{}} by Th8;
hence  Inter (({} U),({} U)) is non empty IntervalSet of U ; ::_thesis: verum
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;
funcA ^  ->  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
let U be non empty set ; ::_thesis: 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 `))
let A be non empty IntervalSet of U; ::_thesis: for X, Y being Subset of U st A = Inter (X,Y) & X c= Y holds
A ^ = Inter ((Y `),(X `))
let X, Y be Subset of U; ::_thesis: ( A = Inter (X,Y) & X c= Y implies A ^ = Inter ((Y `),(X `)) )
assume A1: ( A = Inter (X,Y) & X c= Y ) ; ::_thesis: A ^ = Inter ((Y `),(X `))
then  Inter (X,Y) = Inter ((A ``1),(A ``2)) by Th15;
then  ( X = A ``1 & Y = A ``2 ) by Th6, A1;
hence  A ^ = Inter ((Y `),(X `)) by Th41; ::_thesis: verum
end;

theorem :: INTERVA1:47
for U being non empty set holds (Inter (({} U),({} U))) ^ = Inter (([#] U),([#] U))
proof
let U be non empty set ; ::_thesis: (Inter (({} U),({} U))) ^ = Inter (([#] U),([#] U))
 (Inter (({} U),({} U))) ^ = Inter (([#] U),(({} U) `)) by Th46;
hence  (Inter (({} U),({} U))) ^ = Inter (([#] U),([#] U)) ; ::_thesis: verum
end;

theorem :: INTERVA1:48
for U being non empty set holds (Inter (([#] U),([#] U))) ^ = Inter (({} U),({} U))
proof
let U be non empty set ; ::_thesis: (Inter (([#] U),([#] U))) ^ = Inter (({} U),({} U))
(Inter (([#] U),([#] U))) ^ = Inter ((([#] U) `),(([#] U) `)) by Th46
.= Inter (({} U),(([#] U) `)) by XBOOLE_1:37 ;
hence  (Inter (([#] U),([#] U))) ^ = Inter (({} U),({} U)) by XBOOLE_1:37; ::_thesis: verum
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
let U be non empty set ; ::_thesis: ex A being non empty IntervalSet of U st (A _/\_ A) ^ <> Inter (({} U),({} U))
A1: [#] U in Inter (({} U),([#] U)) ;
then consider A being non empty IntervalSet of U such that
A2: A = Inter (({} U),([#] U)) ;
A3: A ^ = Inter ((([#] U) `),(({} U) `)) by A2, Th46
.= Inter (({} U),([#] U)) ;
 A ^ = Inter (((A ^) ``1),((A ^) ``2)) by Th15;
then  ( (A ^) ``1 = {} U & (A ^) ``2 = [#] U ) by Th6, A3;
then A4: (A _/\_ A) ^ = Inter ((({} U) /\ ({} U)),(([#] U) /\ ([#] U))) by A2, Th18, A3
.= Inter (({} U),([#] U)) ;
 not [#] U c= {} U ;
then  not [#] U in Inter (({} U),({} U)) by Th1;
hence  ex A being non empty IntervalSet of U st (A _/\_ A) ^ <> Inter (({} U),({} U)) by A4, A1; ::_thesis: verum
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
let U be non empty set ; ::_thesis: ex A being non empty IntervalSet of U st (A _\/_ A) ^ <> Inter (([#] U),([#] U))
 not [#] U c= {} U ;
then A1: not {} U in Inter (([#] U),([#] U)) by Th1;
A2: {} U in Inter (({} U),([#] U)) ;
then consider A being non empty IntervalSet of U such that
A3: A = Inter (({} U),([#] U)) ;
A4: A ^ = Inter ((([#] U) `),(({} U) `)) by Th46, A3
.= Inter (({} U),([#] U)) ;
 A ^ = Inter (((A ^) ``1),((A ^) ``2)) by Th15;
then  ( (A ^) ``1 = {} U & (A ^) ``2 = [#] U ) by Th6, A4;
then (A _\/_ A) ^ = Inter ((({} U) \/ ({} U)),(([#] U) \/ ([#] U))) by Th17, A3, A4
.= Inter (({} U),([#] U)) ;
hence  ex A being non empty IntervalSet of U st (A _\/_ A) ^ <> Inter (([#] U),([#] U)) by A2, A1; ::_thesis: verum
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
let U be non empty set ; ::_thesis: ex A being non empty IntervalSet of U st A _\_ A <> Inter (({} U),({} U))
 Inter (({} U),([#] U)) <> {} by Th1;
then consider A being non empty IntervalSet of U such that
A1: A = Inter (({} U),([#] U)) ;
A2: A _\_ A = Inter ((({} U) \ ([#] U)),(([#] U) \ ({} U))) by Th42, A1
.= Inter (({} U),([#] U)) ;
 not U c= {} ;
then  ( [#] U in Inter (({} U),([#] U)) & not [#] U in Inter (({} U),({} U)) ) by Th1;
hence  ex A being non empty IntervalSet of U st A _\_ A <> Inter (({} U),({} U)) by A2; ::_thesis: verum
end;

theorem :: INTERVA1:52
for U being non empty set
for A being non empty IntervalSet of U holds U in A _\/_ (A ^)
proof
let U be non empty set ; ::_thesis: for A being non empty IntervalSet of U holds U in A _\/_ (A ^)
let A be non empty IntervalSet of U; ::_thesis: U in A _\/_ (A ^)
A1: U c= (A ``2) \/ ((A ``1) `)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in U or x in (A ``2) \/ ((A ``1) `) )
assume A2: x in U ; ::_thesis: x in (A ``2) \/ ((A ``1) `)
 A ``1 c= A ``2 by Th16;
then A3: (A ``2) ` c= (A ``1) ` by SUBSET_1:12;
 ( x in A ``2 or x in (A ``2) ` ) by A2, XBOOLE_0:def_5;
hence  x in (A ``2) \/ ((A ``1) `) by A3, XBOOLE_0:def_3; ::_thesis: verum
end;
A4: A ^ = Inter (((A ``2) `),((A ``1) `)) by Th45;
 A ^ = Inter (((A ^) ``1),((A ^) ``2)) by Th15;
then  ( (A ^) ``1 = (A ``2) ` & (A ^) ``2 = (A ``1) ` ) by Th6, A4;
then  A _\/_ (A ^) = Inter (((A ``1) \/ ((A ``2) `)),((A ``2) \/ ((A ``1) `))) by Th17;
hence  U in A _\/_ (A ^) by A1; ::_thesis: verum
end;

theorem :: INTERVA1:53
for U being non empty set
for A being non empty IntervalSet of U holds {} in A _/\_ (A ^)
proof
let U be non empty set ; ::_thesis: for A being non empty IntervalSet of U holds {} in A _/\_ (A ^)
let A be non empty IntervalSet of U; ::_thesis: {} in A _/\_ (A ^)
A1: (A ``1) /\ ((A ``2) `) c= {}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A ``1) /\ ((A ``2) `) or x in {} )
A2: A ``1 c= A ``2 by Th16;
assume  x in (A ``1) /\ ((A ``2) `) ; ::_thesis: x in {}
then  ( x in A ``1 & x in (A ``2) ` ) by XBOOLE_0:def_4;
hence  x in {} by A2, XBOOLE_0:def_5; ::_thesis: verum
end;
A3: A ^ = Inter (((A ``2) `),((A ``1) `)) by Th45;
 A ^ = Inter (((A ^) ``1),((A ^) ``2)) by Th15;
then  ( (A ^) ``1 = (A ``2) ` & (A ^) ``2 = (A ``1) ` ) by Th6, A3;
then A4: A _/\_ (A ^) = Inter (((A ``1) /\ ((A ``2) `)),((A ``2) /\ ((A ``1) `))) by Th18;
 ( (A ``1) /\ ((A ``2) `) c= {} & {} c= (A ``2) /\ ((A ``1) `) ) by A1, XBOOLE_1:2;
hence  {} in A _/\_ (A ^) by A4, Th1; ::_thesis: verum
end;

theorem :: INTERVA1:54
for U being non empty set
for A being non empty IntervalSet of U holds {} in A _\_ A
proof
let U be non empty set ; ::_thesis: for A being non empty IntervalSet of U holds {} in A _\_ A
let A be non empty IntervalSet of U; ::_thesis: {} in A _\_ A
A1: A _\_ A = Inter (((A ``1) \ (A ``2)),((A ``2) \ (A ``1))) by Th40;
A2: (A ``1) \ (A ``2) c= {}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A ``1) \ (A ``2) or x in {} )
assume  x in (A ``1) \ (A ``2) ; ::_thesis: x in {}
then  ( x in A ``1 & not x in A ``2 & A ``1 c= A ``2 ) by Th16, XBOOLE_0:def_5;
hence  x in {} ; ::_thesis: verum
end;
 {} c= (A ``2) \ (A ``1) by XBOOLE_1:2;
hence  {} in A _\_ A by Th1, A2, A1; ::_thesis: verum
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
defpred S1[ set ] means $1 is non empty IntervalSet of U;
 ex X being set st
for x being set holds
( x in X iff ( x in bool (bool U) & S1[x] ) ) from XBOOLE_0:sch_1();
then consider X being set  such that
A1: for x being set holds
( x in X iff ( x in bool (bool U) & S1[x] ) ) ;
set x = the Element of U;
reconsider E = { the Element of U} as Subset of U by ZFMISC_1:31;
 {E} is non empty IntervalSet of U by Th10;
then reconsider X = X as non empty set by A1;
take  X ; ::_thesis: for x being set holds
( x in X iff x is non empty IntervalSet of U )
thus  for x being set holds
( x in X iff x is non empty IntervalSet of U ) by A1; ::_thesis: verum
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
let S1, S2 be non empty set ; ::_thesis: ( ( for x being set holds
( x in S1 iff x is non empty IntervalSet of U ) ) & ( for x being set holds
( x in S2 iff x is non empty IntervalSet of U ) ) implies S1 = S2 )
assume that
A2: for x being set holds
( x in S1 iff x is non empty IntervalSet of U ) and
A3: for x being set holds
( x in S2 iff x is non empty IntervalSet of U ) ; ::_thesis: S1 = S2
 for x being set holds
( x in S1 iff x in S2 )
proof
let x be set ; ::_thesis: ( x in S1 iff x in S2 )
thus  ( x in S1 implies x in S2 ) ::_thesis: ( x in S2 implies x in S1 )
proof
assume  x in S1 ; ::_thesis: x in S2
then  x is non empty IntervalSet of U by A2;
hence  x in S2 by A3; ::_thesis: verum
end;
assume  x in S2 ; ::_thesis: x in S1
then  x is non empty IntervalSet of U by A3;
hence  x in S1 by A2; ::_thesis: verum
end;
hence  S1 = S2 by TARSKI:1; ::_thesis: verum
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
set B = IntervalSets U;
defpred S1[ Element of IntervalSets U, Element of IntervalSets U, Element of IntervalSets U] means  ex a9, b9 being non empty IntervalSet of U st
( a9 = $1 & b9 = $2 & $3 = a9 _\/_ b9 );
A1: for x, y being Element of IntervalSets U ex z being Element of IntervalSets U st S1[x,y,z]
proof
let x, y be Element of IntervalSets U; ::_thesis: ex z being Element of IntervalSets U st S1[x,y,z]
reconsider x9 = x, y9 = y as non empty IntervalSet of U by Def11;
reconsider z = x9 _\/_ y9 as Element of IntervalSets U by Def11;
take  z ; ::_thesis: S1[x,y,z]
thus  S1[x,y,z] ; ::_thesis: verum
end;
consider B1 being BinOp of (IntervalSets U) such that
A2: for x, y being Element of IntervalSets U holds S1[x,y,B1 . (x,y)] from BINOP_1:sch_3(A1);
defpred S2[ Element of IntervalSets U, Element of IntervalSets U, Element of IntervalSets U] means  ex a9, b9 being non empty IntervalSet of U st
( a9 = $1 & b9 = $2 & $3 = a9 _/\_ b9 );
A3: for x, y being Element of IntervalSets U ex z being Element of IntervalSets U st S2[x,y,z]
proof
let x, y be Element of IntervalSets U; ::_thesis: ex z being Element of IntervalSets U st S2[x,y,z]
reconsider x9 = x, y9 = y as non empty IntervalSet of U by Def11;
reconsider z = x9 _/\_ y9 as Element of IntervalSets U by Def11;
take  z ; ::_thesis: S2[x,y,z]
thus  S2[x,y,z] ; ::_thesis: verum
end;
consider B2 being BinOp of (IntervalSets U) such that
A4: for x, y being Element of IntervalSets U holds S2[x,y,B2 . (x,y)] from BINOP_1:sch_3(A3);
take IT = LattStr(# (IntervalSets U),B1,B2 #); ::_thesis: ( 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 ) ) )
thus  the carrier of IT = IntervalSets U ; ::_thesis: 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 )
let a, b be Element of the carrier of IT; ::_thesis: 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 )
let a9, b9 be non empty IntervalSet of U; ::_thesis: ( a9 = a & b9 = b implies ( the L_join of IT . (a,b) = a9 _\/_ b9 & the L_meet of IT . (a,b) = a9 _/\_ b9 ) )
assume A5: ( a9 = a & b9 = b ) ; ::_thesis: ( the L_join of IT . (a,b) = a9 _\/_ b9 & the L_meet of IT . (a,b) = a9 _/\_ b9 )
reconsider x = a, y = b as Element of IntervalSets U ;
consider a9, b9 being non empty IntervalSet of U such that
A6: ( a9 = x & b9 = y & B1 . (x,y) = a9 _\/_ b9 ) by A2;
consider a1, b1 being non empty IntervalSet of U such that
A7: ( a1 = x & b1 = y & B2 . (x,y) = a1 _/\_ b1 ) by A4;
thus  ( the L_join of IT . (a,b) = a9 _\/_ b9 & the L_meet of IT . (a,b) = a9 _/\_ b9 ) by A6, A7, A5; ::_thesis: verum
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
let L1, L2 be non empty strict LattStr ; ::_thesis: ( the carrier of L1 = IntervalSets U & ( for a, b being Element of the carrier of L1
for a9, b9 being non empty IntervalSet of U st a9 = a & b9 = b holds
( the L_join of L1 . (a,b) = a9 _\/_ b9 & the L_meet of L1 . (a,b) = a9 _/\_ b9 ) ) & the carrier of L2 = IntervalSets U & ( for a, b being Element of the carrier of L2
for a9, b9 being non empty IntervalSet of U st a9 = a & b9 = b holds
( the L_join of L2 . (a,b) = a9 _\/_ b9 & the L_meet of L2 . (a,b) = a9 _/\_ b9 ) ) implies L1 = L2 )
assume that
A8: ( the carrier of L1 = IntervalSets U & ( for a, b being Element of the carrier of L1
for a9, b9 being non empty IntervalSet of U st a9 = a & b9 = b holds
( the L_join of L1 . (a,b) = a9 _\/_ b9 & the L_meet of L1 . (a,b) = a9 _/\_ b9 ) ) ) and
A9: ( the carrier of L2 = IntervalSets U & ( for a, b being Element of the carrier of L2
for a9, b9 being non empty IntervalSet of U st a9 = a & b9 = b holds
( the L_join of L2 . (a,b) = a9 _\/_ b9 & the L_meet of L2 . (a,b) = a9 _/\_ b9 ) ) ) ; ::_thesis: L1 = L2
 for a, b being Element of L1 holds the L_join of L1 . (a,b) = the L_join of L2 . (a,b)
proof
let a, b be Element of L1; ::_thesis: the L_join of L1 . (a,b) = the L_join of L2 . (a,b)
reconsider a9 = a, b9 = b as non empty IntervalSet of U by A8, Def11;
the L_join of L1 . (a,b) = a9 _\/_ b9 by A8
.= the L_join of L2 . (a,b) by A9, A8 ;
hence  the L_join of L1 . (a,b) = the L_join of L2 . (a,b) ; ::_thesis: verum
end;
then A10: the L_join of L1 = the L_join of L2 by A8, A9, BINOP_1:2;
 for a, b being Element of L1 holds the L_meet of L1 . (a,b) = the L_meet of L2 . (a,b)
proof
let a, b be Element of L1; ::_thesis: the L_meet of L1 . (a,b) = the L_meet of L2 . (a,b)
reconsider a9 = a, b9 = b as non empty IntervalSet of U by A8, Def11;
the L_meet of L1 . (a,b) = a9 _/\_ b9 by A8
.= the L_meet of L2 . (a,b) by A8, A9 ;
hence  the L_meet of L1 . (a,b) = the L_meet of L2 . (a,b) ; ::_thesis: verum
end;
hence  L1 = L2 by A8, A9, A10, BINOP_1:2; ::_thesis: verum
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
A1: InterLatt U is join-commutative
proof
 for a, b being Element of (InterLatt U) holds a "\/" b = b "\/" a
proof
let a, b be Element of (InterLatt U); ::_thesis: a "\/" b = b "\/" a
 ( a in the carrier of (InterLatt U) & b in the carrier of (InterLatt U) ) ;
then  ( a in IntervalSets U & b in IntervalSets U ) by Def12;
then reconsider a9 = a, b9 = b as non empty IntervalSet of U by Def11;
a "\/" b = a9 _\/_ b9 by Def12
.= b9 _\/_ a9
.= b "\/" a by Def12 ;
hence  a "\/" b = b "\/" a ; ::_thesis: verum
end;
hence  InterLatt U is join-commutative by LATTICES:def_4; ::_thesis: verum
end;
A2: InterLatt U is join-associative
proof
 for a, b, c being Element of (InterLatt U) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c
proof
let a, b, c be Element of (InterLatt U); ::_thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c
 ( a in the carrier of (InterLatt U) & b in the carrier of (InterLatt U) & c in the carrier of (InterLatt U) ) ;
then  ( a in IntervalSets U & b in IntervalSets U & c in IntervalSets U ) by Def12;
then reconsider a9 = a, b9 = b, c9 = c as non empty IntervalSet of U by Def11;
reconsider bc = b9 _\/_ c9 as non empty IntervalSet of U ;
reconsider ab = a9 _\/_ b9 as non empty IntervalSet of U ;
 ( bc in IntervalSets U & ab in IntervalSets U ) by Def11;
then A3: ( bc in the carrier of (InterLatt U) & ab in the carrier of (InterLatt U) ) by Def12;
a "\/" (b "\/" c) = the L_join of (InterLatt U) . (a,bc) by Def12
.= a9 _\/_ bc by Def12, A3
.= (a9 _\/_ b9) _\/_ c9 by Th23
.= the L_join of (InterLatt U) . (ab,c9) by Def12, A3
.= (a "\/" b) "\/" c by Def12 ;
hence  a "\/" (b "\/" c) = (a "\/" b) "\/" c ; ::_thesis: verum
end;
hence  InterLatt U is join-associative by LATTICES:def_5; ::_thesis: verum
end;
A4: InterLatt U is meet-absorbing
proof
 for a, b being Element of (InterLatt U) holds (a "/\" b) "\/" b = b
proof
let a, b be Element of (InterLatt U); ::_thesis: (a "/\" b) "\/" b = b
 ( a in the carrier of (InterLatt U) & b in the carrier of (InterLatt U) ) ;
then  ( a in IntervalSets U & b in IntervalSets U ) by Def12;
then reconsider a9 = a, b9 = b as non empty IntervalSet of U by Def11;
reconsider ab = a9 _/\_ b9 as non empty IntervalSet of U ;
 ab in IntervalSets U by Def11;
then A5: ab in the carrier of (InterLatt U) by Def12;
(a "/\" b) "\/" b = the L_join of (InterLatt U) . (ab,b) by Def12
.= ab _\/_ b9 by Def12, A5
.= b by Th36 ;
hence  (a "/\" b) "\/" b = b ; ::_thesis: verum
end;
hence  InterLatt U is meet-absorbing by LATTICES:def_8; ::_thesis: verum
end;
A6: InterLatt U is meet-associative
proof
 for a, b, c being Element of (InterLatt U) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c
proof
let a, b, c be Element of (InterLatt U); ::_thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c
 ( a in the carrier of (InterLatt U) & b in the carrier of (InterLatt U) & c in the carrier of (InterLatt U) ) ;
then  ( a in IntervalSets U & b in IntervalSets U & c in IntervalSets U ) by Def12;
then reconsider a9 = a, b9 = b, c9 = c as non empty IntervalSet of U by Def11;
reconsider bc = b9 _/\_ c9, ab = a9 _/\_ b9 as non empty IntervalSet of U ;
 ( bc in IntervalSets U & ab in IntervalSets U ) by Def11;
then A7: ( bc in the carrier of (InterLatt U) & ab in the carrier of (InterLatt U) ) by Def12;
a "/\" (b "/\" c) = the L_meet of (InterLatt U) . (a,bc) by Def12
.= a9 _/\_ bc by Def12, A7
.= (a9 _/\_ b9) _/\_ c9 by Th24
.= the L_meet of (InterLatt U) . (ab,c9) by Def12, A7
.= (a "/\" b) "/\" c by Def12 ;
hence  a "/\" (b "/\" c) = (a "/\" b) "/\" c ; ::_thesis: verum
end;
hence  InterLatt U is meet-associative by LATTICES:def_7; ::_thesis: verum
end;
A8: InterLatt U is join-absorbing
proof
 for a, b being Element of the carrier of (InterLatt U) holds a "/\" (a "\/" b) = a
proof
let a, b be Element of the carrier of (InterLatt U); ::_thesis: a "/\" (a "\/" b) = a
 ( a in the carrier of (InterLatt U) & b in the carrier of (InterLatt U) ) ;
then  ( a in IntervalSets U & b in IntervalSets U ) by Def12;
then reconsider a9 = a, b9 = b as non empty IntervalSet of U by Def11;
reconsider ab = a9 _\/_ b9 as non empty IntervalSet of U ;
 ab in IntervalSets U by Def11;
then A9: ab in the carrier of (InterLatt U) by Def12;
a "/\" (a "\/" b) = the L_meet of (InterLatt U) . (a9,(a9 _\/_ b9)) by Def12
.= a9 _/\_ ab by Def12, A9
.= a by Th35 ;
hence  a "/\" (a "\/" b) = a ; ::_thesis: verum
end;
hence  InterLatt U is join-absorbing by LATTICES:def_9; ::_thesis: verum
end;
 InterLatt U is meet-commutative
proof
 for a, b being Element of the carrier of (InterLatt U) holds a "/\" b = b "/\" a
proof
let a, b be Element of the carrier of (InterLatt U); ::_thesis: a "/\" b = b "/\" a
 ( a in the carrier of (InterLatt U) & b in the carrier of (InterLatt U) ) ;
then  ( a in IntervalSets U & b in IntervalSets U ) by Def12;
then reconsider a9 = a, b9 = b as non empty IntervalSet of U by Def11;
 a9 _/\_ b9 = b9 _/\_ a9 ;
then  the L_meet of (InterLatt U) . (a,b) = b9 _/\_ a9 by Def12
.= the L_meet of (InterLatt U) . (b,a) by Def12 ;
hence  a "/\" b = b "/\" a ; ::_thesis: verum
end;
hence  InterLatt U is meet-commutative by LATTICES:def_6; ::_thesis: verum
end;
hence  InterLatt U is Lattice-like by A1, A2, A4, A6, A8; ::_thesis: verum
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
let X be Tolerance_Space; ::_thesis: for A being RoughSet of X ex B, C being Subset of X st A = [B,C]
let A be RoughSet of X; ::_thesis: ex B, C being Subset of X st A = [B,C]
consider A1, A2 being set  such that
A1: ( A1 in bool the carrier of X & A2 in bool the carrier of X & A = [A1,A2] ) by ZFMISC_1:def_2;
reconsider A1 = A1, A2 = A2 as Subset of X by A1;
take  A1 ; ::_thesis: ex C being Subset of X st A = [A1,C]
take  A2 ; ::_thesis: A = [A1,A2]
thus  A = [A1,A2] by A1; ::_thesis: verum
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
 [(LAp A),(UAp A)] in [:(bool the carrier of X),(bool the carrier of X):] by ZFMISC_1:87;
hence  [(LAp A),(UAp A)] is RoughSet of X by Def13; ::_thesis: verum
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
consider A9, B9 being Subset of X such that
A1: A = [A9,B9] by Th55;
thus  A `1 is Subset of X by A1, MCART_1:7; ::_thesis: verum
end;
func UAp A ->  Subset of X equals :: INTERVA1:def 16
A `2 ;
coherence
 A `2 is Subset of X
proof
consider A9, B9 being Subset of X such that
A2: A = [A9,B9] by Th55;
thus  A `2 is Subset of X by A2, MCART_1:7; ::_thesis: verum
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 predA = 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
thus  ( A = B implies ( LAp A = LAp B & UAp A = UAp B ) ) ; ::_thesis: ( LAp A = LAp B & UAp A = UAp B implies A = B )
assume A1: ( LAp A = LAp B & UAp A = UAp B ) ; ::_thesis: A = B
consider A1, B1 being Subset of X such that
A2: A = [A1,B1] by Th55;
consider A2, B2 being Subset of X such that
A3: B = [A2,B2] by Th55;
 LAp A = A1 by A2, MCART_1:7;
then A4: A1 = A2 by A1, A3, MCART_1:7;
 UAp A = B1 by A2, MCART_1:7;
hence  A = B by A2, A4, A3, A1, MCART_1:7; ::_thesis: verum
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;
funcA _\/_ 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
 [((LAp A) \/ (LAp B)),((UAp A) \/ (UAp B))] in [:(bool the carrier of X),(bool the carrier of X):] by ZFMISC_1:87;
hence  [((LAp A) \/ (LAp B)),((UAp A) \/ (UAp B))] is RoughSet of X by Def13; ::_thesis: verum
end;
funcA _/\_ 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
 [((LAp A) /\ (LAp B)),((UAp A) /\ (UAp B))] in [:(bool the carrier of X),(bool the carrier of X):] by ZFMISC_1:87;
hence  [((LAp A) /\ (LAp B)),((UAp A) /\ (UAp B))] is RoughSet of X by Def13; ::_thesis: verum
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
let X be Tolerance_Space; ::_thesis: for A being RoughSet of X holds A _\/_ A = A
let A be RoughSet of X; ::_thesis: A _\/_ A = A
A1: LAp (A _\/_ A) = LAp A by Th56;
 UAp (A _\/_ A) = (UAp A) \/ (UAp A) by Th57;
hence  A _\/_ A = A by A1, Def17; ::_thesis: verum
end;

theorem Th61: :: INTERVA1:61
for X being Tolerance_Space
for A being RoughSet of X holds A _/\_ A = A
proof
let X be Tolerance_Space; ::_thesis: for A being RoughSet of X holds A _/\_ A = A
let A be RoughSet of X; ::_thesis: A _/\_ A = A
A1: LAp (A _/\_ A) = LAp A by Th58;
 UAp (A _/\_ A) = (UAp A) /\ (UAp A) by Th59;
hence  A _/\_ A = A by A1, Def17; ::_thesis: verum
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
let X be Tolerance_Space; ::_thesis: for A, B, C being RoughSet of X holds (A _\/_ B) _\/_ C = A _\/_ (B _\/_ C)
let A, B, C be RoughSet of X; ::_thesis: (A _\/_ B) _\/_ C = A _\/_ (B _\/_ C)
A1: (LAp (A _\/_ B)) \/ (LAp C) = ((LAp A) \/ (LAp B)) \/ (LAp C) by Th56;
A2: ((LAp A) \/ (LAp B)) \/ (LAp C) = (LAp A) \/ ((LAp B) \/ (LAp C)) by XBOOLE_1:4;
A3: (LAp A) \/ ((LAp B) \/ (LAp C)) = (LAp A) \/ (LAp (B _\/_ C)) by Th56;
 (LAp A) \/ (LAp (B _\/_ C)) = LAp (A _\/_ (B _\/_ C)) by Th56;
then A4: LAp ((A _\/_ B) _\/_ C) = LAp (A _\/_ (B _\/_ C)) by Th56, A1, A2, A3;
A5: UAp ((A _\/_ B) _\/_ C) = (UAp (A _\/_ B)) \/ (UAp C) by Th57;
A6: (UAp (A _\/_ B)) \/ (UAp C) = ((UAp A) \/ (UAp B)) \/ (UAp C) by Th57;
A7: ((UAp A) \/ (UAp B)) \/ (UAp C) = (UAp A) \/ ((UAp B) \/ (UAp C)) by XBOOLE_1:4;
A8: (UAp A) \/ ((UAp B) \/ (UAp C)) = (UAp A) \/ (UAp (B _\/_ C)) by Th57;
 (UAp A) \/ (UAp (B _\/_ C)) = UAp (A _\/_ (B _\/_ C)) by Th57;
hence  (A _\/_ B) _\/_ C = A _\/_ (B _\/_ C) by A4, Def17, A5, A6, A7, A8; ::_thesis: verum
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
let X be Tolerance_Space; ::_thesis: for A, B, C being RoughSet of X holds (A _/\_ B) _/\_ C = A _/\_ (B _/\_ C)
let A, B, C be RoughSet of X; ::_thesis: (A _/\_ B) _/\_ C = A _/\_ (B _/\_ C)
A1: (LAp (A _/\_ B)) /\ (LAp C) = ((LAp A) /\ (LAp B)) /\ (LAp C) by Th58;
A2: ((LAp A) /\ (LAp B)) /\ (LAp C) = (LAp A) /\ ((LAp B) /\ (LAp C)) by XBOOLE_1:16;
A3: (UAp (A _/\_ B)) /\ (UAp C) = ((UAp A) /\ (UAp B)) /\ (UAp C) by Th59;
A4: ((UAp A) /\ (UAp B)) /\ (UAp C) = (UAp A) /\ ((UAp B) /\ (UAp C)) by XBOOLE_1:16;
 (UAp A) /\ ((UAp B) /\ (UAp C)) = (UAp A) /\ (UAp (B _/\_ C)) by Th59;
hence  (A _/\_ B) _/\_ C = A _/\_ (B _/\_ C) by A1, A2, Th58, A3, A4; ::_thesis: verum
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
let X be Tolerance_Space; ::_thesis: for A, B, C being RoughSet of X holds A _/\_ (B _\/_ C) = (A _/\_ B) _\/_ (A _/\_ C)
let A, B, C be RoughSet of X; ::_thesis: A _/\_ (B _\/_ C) = (A _/\_ B) _\/_ (A _/\_ C)
A1: LAp (A _/\_ (B _\/_ C)) = (LAp A) /\ (LAp (B _\/_ C)) by Th58;
A2: (LAp A) /\ (LAp (B _\/_ C)) = (LAp A) /\ ((LAp B) \/ (LAp C)) by Th56;
A3: (LAp A) /\ ((LAp B) \/ (LAp C)) = ((LAp A) /\ (LAp B)) \/ ((LAp A) /\ (LAp C)) by XBOOLE_1:23;
A4: ((LAp A) /\ (LAp B)) \/ ((LAp A) /\ (LAp C)) = (LAp (A _/\_ B)) \/ ((LAp A) /\ (LAp C)) by Th58;
 (LAp (A _/\_ B)) \/ ((LAp A) /\ (LAp C)) = (LAp (A _/\_ B)) \/ (LAp (A _/\_ C)) by Th58;
then A5: LAp (A _/\_ (B _\/_ C)) = LAp ((A _/\_ B) _\/_ (A _/\_ C)) by A1, A2, A3, A4, Th56;
A6: UAp (A _/\_ (B _\/_ C)) = (UAp A) /\ (UAp (B _\/_ C)) by Th59;
A7: (UAp A) /\ (UAp (B _\/_ C)) = (UAp A) /\ ((UAp B) \/ (UAp C)) by Th57;
A8: (UAp A) /\ ((UAp B) \/ (UAp C)) = ((UAp A) /\ (UAp B)) \/ ((UAp A) /\ (UAp C)) by XBOOLE_1:23;
A9: ((UAp A) /\ (UAp B)) \/ ((UAp A) /\ (UAp C)) = (UAp (A _/\_ B)) \/ ((UAp A) /\ (UAp C)) by Th59;
 (UAp (A _/\_ B)) \/ ((UAp A) /\ (UAp C)) = (UAp (A _/\_ B)) \/ (UAp (A _/\_ C)) by Th59;
then  UAp (A _/\_ (B _\/_ C)) = UAp ((A _/\_ B) _\/_ (A _/\_ C)) by A6, A7, A8, A9, Th57;
hence  A _/\_ (B _\/_ C) = (A _/\_ B) _\/_ (A _/\_ C) by A5, Def17; ::_thesis: verum
end;

theorem Th67: :: INTERVA1:67
for X being Tolerance_Space
for A, B being RoughSet of X holds A _\/_ (A _/\_ B) = A
proof
let X be Tolerance_Space; ::_thesis: for A, B being RoughSet of X holds A _\/_ (A _/\_ B) = A
let A, B be RoughSet of X; ::_thesis: A _\/_ (A _/\_ B) = A
A1: LAp (A _\/_ (A _/\_ B)) = (LAp A) \/ (LAp (A _/\_ B)) by Th56
.= (LAp A) \/ ((LAp A) /\ (LAp B)) by Th58
.= LAp A by XBOOLE_1:22 ;
UAp (A _\/_ (A _/\_ B)) = (UAp A) \/ (UAp (A _/\_ B)) by Th57
.= (UAp A) \/ ((UAp A) /\ (UAp B)) by Th59
.= UAp A by XBOOLE_1:22 ;
hence  A _\/_ (A _/\_ B) = A by A1, Def17; ::_thesis: verum
end;

theorem :: INTERVA1:68
for X being Tolerance_Space
for A, B being RoughSet of X holds A _/\_ (A _\/_ B) = A
proof
let X be Tolerance_Space; ::_thesis: for A, B being RoughSet of X holds A _/\_ (A _\/_ B) = A
let A, B be RoughSet of X; ::_thesis: A _/\_ (A _\/_ B) = A
A1: LAp (A _/\_ (A _\/_ B)) = (LAp A) /\ (LAp (A _\/_ B)) by Th58
.= (LAp A) /\ ((LAp A) \/ (LAp B)) by Th56
.= LAp A by XBOOLE_1:21 ;
UAp (A _/\_ (A _\/_ B)) = (UAp A) /\ (UAp (A _\/_ B)) by Th59
.= (UAp A) /\ ((UAp A) \/ (UAp B)) by Th57
.= UAp A by XBOOLE_1:21 ;
hence  A _/\_ (A _\/_ B) = A by A1, Def17; ::_thesis: verum
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
defpred S1[ set ] means $1 is RoughSet of X;
consider F being set  such that
A1: for x being set holds
( x in F iff ( x in [:(bool the carrier of X),(bool the carrier of X):] & S1[x] ) ) from XBOOLE_0:sch_1();
take  F ; ::_thesis: for x being set holds
( x in F iff x is RoughSet of X )
let x be set ; ::_thesis: ( x in F iff x is RoughSet of X )
thus  ( x in F implies x is RoughSet of X ) by A1; ::_thesis: ( x is RoughSet of X implies x in F )
assume  x is RoughSet of X ; ::_thesis: x in F
hence  x in F by A1; ::_thesis: verum
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
let F1, F2 be set ; ::_thesis: ( ( for x being set holds
( x in F1 iff x is RoughSet of X ) ) & ( for x being set holds
( x in F2 iff x is RoughSet of X ) ) implies F1 = F2 )
assume A2: ( ( for x being set holds
( x in F1 iff x is RoughSet of X ) ) & ( for x being set holds
( x in F2 iff x is RoughSet of X ) ) ) ; ::_thesis: F1 = F2
now__::_thesis:_for_x_being_set_holds_
(_x_in_F1_iff_x_in_F2_)
let x be set ; ::_thesis: ( x in F1 iff x in F2 )
 ( ( x in F1 implies x is RoughSet of X ) & ( x is RoughSet of X implies x in F1 ) & ( x in F2 implies x is RoughSet of X ) & ( x is RoughSet of X implies x in F2 ) ) by A2;
hence  ( x in F1 iff x in F2 ) ; ::_thesis: verum
end;
hence  F1 = F2 by TARSKI:1; ::_thesis: verum
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
set A = the RoughSet of X;
 the RoughSet of X in RoughSets X by Def20;
hence  not RoughSets X is empty ; ::_thesis: verum
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;
funcR @  ->  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
deffunc H1( Element of RoughSets X, Element of RoughSets X) ->  Element of RoughSets X = ((@ $1) _\/_ (@ $2)) @ ;
consider j being BinOp of (RoughSets X) such that
A1: for x, y being Element of RoughSets X holds j . (x,y) = H1(x,y) from BINOP_1:sch_4();
deffunc H2( Element of RoughSets X, Element of RoughSets X) ->  Element of RoughSets X = ((@ $1) _/\_ (@ $2)) @ ;
consider m being BinOp of (RoughSets X) such that
A2: for x, y being Element of RoughSets X holds m . (x,y) = H2(x,y) from BINOP_1:sch_4();
take IT = LattStr(# (RoughSets X),j,m #); ::_thesis: ( 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 ) ) )
thus  the carrier of IT = RoughSets X ; ::_thesis: 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 )
let A, B be Element of RoughSets X; ::_thesis: 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 )
let A9, B9 be RoughSet of X; ::_thesis: ( A = A9 & B = B9 implies ( the L_join of IT . (A,B) = A9 _\/_ B9 & the L_meet of IT . (A,B) = A9 _/\_ B9 ) )
assume A3: ( A = A9 & B = B9 ) ; ::_thesis: ( the L_join of IT . (A,B) = A9 _\/_ B9 & the L_meet of IT . (A,B) = A9 _/\_ B9 )
thus  the L_join of IT . (A,B) = H1(A,B) by A1
.= A9 _\/_ B9 by A3 ; ::_thesis: the L_meet of IT . (A,B) = A9 _/\_ B9
thus  the L_meet of IT . (A,B) = H2(A,B) by A2
.= A9 _/\_ B9 by A3 ; ::_thesis: verum
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
let A1, A2 be strict LattStr ; ::_thesis: ( the carrier of A1 = 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 A1 . (A,B) = A9 _\/_ B9 & the L_meet of A1 . (A,B) = A9 _/\_ B9 ) ) & the carrier of A2 = 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 A2 . (A,B) = A9 _\/_ B9 & the L_meet of A2 . (A,B) = A9 _/\_ B9 ) ) implies A1 = A2 )
assume that
A4: ( the carrier of A1 = 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 A1 . (A,B) = A9 _\/_ B9 & the L_meet of A1 . (A,B) = A9 _/\_ B9 ) ) ) and
A5: ( the carrier of A2 = 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 A2 . (A,B) = A9 _\/_ B9 & the L_meet of A2 . (A,B) = A9 _/\_ B9 ) ) ) ; ::_thesis: A1 = A2
reconsider a3 = the L_meet of A1, a4 = the L_meet of A2, a1 = the L_join of A1, a2 = the L_join of A2 as BinOp of (RoughSets X) by A4, A5;
now__::_thesis:_for_x,_y_being_Element_of_RoughSets_X_holds_a1_._(x,y)_=_a2_._(x,y)
let x, y be Element of RoughSets X; ::_thesis: a1 . (x,y) = a2 . (x,y)
thus a1 . (x,y) = (@ x) _\/_ (@ y) by A4
.= a2 . (x,y) by A5 ; ::_thesis: verum
end;
then A6: a1 = a2 by BINOP_1:2;
now__::_thesis:_for_x,_y_being_Element_of_RoughSets_X_holds_a3_._(x,y)_=_a4_._(x,y)
let x, y be Element of RoughSets X; ::_thesis: a3 . (x,y) = a4 . (x,y)
thus a3 . (x,y) = (@ x) _/\_ (@ y) by A4
.= a4 . (x,y) by A5 ; ::_thesis: verum
end;
hence  A1 = A2 by A4, A5, A6, BINOP_1:2; ::_thesis: verum
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
 the carrier of (RSLattice X) = RoughSets X by Def23;
hence  not RSLattice X is empty ; ::_thesis: verum
end;
end;

Lm6:  for X being Tolerance_Space
for a, b being Element of (RSLattice X) holds a "\/" b = b "\/" a
proof
let X be Tolerance_Space; ::_thesis: for a, b being Element of (RSLattice X) holds a "\/" b = b "\/" a
set G = RSLattice X;
let a, b be Element of (RSLattice X); ::_thesis: a "\/" b = b "\/" a
reconsider a1 = a, b1 = b as Element of RoughSets X by Def23;
reconsider a9 = a1, b9 = b1 as RoughSet of X by Def20;
a "\/" b = a9 _\/_ b9 by Def23
.= b9 _\/_ a9
.= b "\/" a by Def23 ;
hence  a "\/" b = b "\/" a ; ::_thesis: verum
end;

Lm7:  for X being Tolerance_Space
for a, b, c being Element of (RSLattice X) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c
proof
let X be Tolerance_Space; ::_thesis: for a, b, c being Element of (RSLattice X) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c
let a, b, c be Element of (RSLattice X); ::_thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c
reconsider a1 = a, b1 = b, c1 = c as Element of RoughSets X by Def23;
reconsider a9 = a1, b9 = b1, c9 = c1 as RoughSet of X by Def20;
set G = RSLattice X;
A1: b9 _\/_ c9 is Element of RoughSets X by Def20;
A2: a9 _\/_ b9 is Element of RoughSets X by Def20;
a "\/" (b "\/" c) = the L_join of (RSLattice X) . (a,(b9 _\/_ c9)) by Def23
.= a9 _\/_ (b9 _\/_ c9) by Def23, A1
.= (a9 _\/_ b9) _\/_ c9 by Th64
.= the L_join of (RSLattice X) . ((a9 _\/_ b9),c1) by Def23, A2
.= (a "\/" b) "\/" c by Def23 ;
hence  a "\/" (b "\/" c) = (a "\/" b) "\/" c ; ::_thesis: verum
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
let X be Tolerance_Space; ::_thesis: 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
let K, L be Element of RoughSets X; ::_thesis: the L_join of (RSLattice X) . (( the L_meet of (RSLattice X) . (K,L)),L) = L
reconsider K9 = K, L9 = L as RoughSet of X by Def20;
A1: K9 _/\_ L9 is Element of RoughSets X by Def20;
thus  the L_join of (RSLattice X) . (( the L_meet of (RSLattice X) . (K,L)),L) = the L_join of (RSLattice X) . ((K9 _/\_ L9),L) by Def23
.= (K9 _/\_ L9) _\/_ L9 by Def23, A1
.= L9 _\/_ (L9 _/\_ K9)
.= L by Th67 ; ::_thesis: verum
end;

Lm9:  for X being Tolerance_Space
for a, b being Element of (RSLattice X) holds (a "/\" b) "\/" b = b
proof
let X be Tolerance_Space; ::_thesis: for a, b being Element of (RSLattice X) holds (a "/\" b) "\/" b = b
let a, b be Element of (RSLattice X); ::_thesis: (a "/\" b) "\/" b = b
set G = RSLattice X;
reconsider a1 = a, b1 = b as Element of RoughSets X by Def23;
thus (a "/\" b) "\/" b = the L_join of (RSLattice X) . (( the L_meet of (RSLattice X) . (a1,b1)),b1)
.= b by Lm8 ; ::_thesis: verum
end;

Lm10:  for X being Tolerance_Space
for a, b being Element of (RSLattice X) holds a "/\" b = b "/\" a
proof
let X be Tolerance_Space; ::_thesis: for a, b being Element of (RSLattice X) holds a "/\" b = b "/\" a
let a, b be Element of (RSLattice X); ::_thesis: a "/\" b = b "/\" a
reconsider a1 = a, b1 = b as Element of RoughSets X by Def23;
reconsider a9 = a1, b9 = b1 as RoughSet of X by Def20;
a "/\" b = a9 _/\_ b9 by Def23
.= b9 _/\_ a9
.= b "/\" a by Def23 ;
hence  a "/\" b = b "/\" a ; ::_thesis: verum
end;

Lm11:  for X being Tolerance_Space
for a, b, c being Element of (RSLattice X) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c
proof
let X be Tolerance_Space; ::_thesis: for a, b, c being Element of (RSLattice X) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c
let a, b, c be Element of (RSLattice X); ::_thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c
reconsider a1 = a, b1 = b, c1 = c as Element of RoughSets X by Def23;
reconsider a9 = a1, b9 = b1, c9 = c1 as RoughSet of X by Def20;
set G = RSLattice X;
A1: b9 _/\_ c9 is Element of RoughSets X by Def20;
A2: a9 _/\_ b9 is Element of RoughSets X by Def20;
a "/\" (b "/\" c) = the L_meet of (RSLattice X) . (a1,(b9 _/\_ c9)) by Def23
.= a9 _/\_ (b9 _/\_ c9) by Def23, A1
.= (a9 _/\_ b9) _/\_ c9 by Th65
.= the L_meet of (RSLattice X) . ((a9 _/\_ b9),c1) by Def23, A2
.= (a "/\" b) "/\" c by Def23 ;
hence  a "/\" (b "/\" c) = (a "/\" b) "/\" c ; ::_thesis: verum
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
let X be Tolerance_Space; ::_thesis: 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)))
let K, L, M be Element of RoughSets X; ::_thesis: 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)))
set G = RSLattice X;
reconsider K9 = K, L9 = L, M9 = M as RoughSet of X by Def20;
A1: L9 _\/_ M9 is Element of RoughSets X by Def20;
A2: K9 _/\_ L9 is Element of RoughSets X by Def20;
A3: K9 _/\_ M9 is Element of RoughSets X by Def20;
the L_meet of (RSLattice X) . (K,( the L_join of (RSLattice X) . (L,M))) = the L_meet of (RSLattice X) . (K,(L9 _\/_ M9)) by Def23
.= K9 _/\_ (L9 _\/_ M9) by Def23, A1
.= (K9 _/\_ L9) _\/_ (K9 _/\_ M9) by Th66
.= the L_join of (RSLattice X) . ((K9 _/\_ L9),(K9 _/\_ M9)) by Def23, A2, A3
.= the L_join of (RSLattice X) . (( the L_meet of (RSLattice X) . (K,L)),(K9 _/\_ M9)) by Def23
.= the L_join of (RSLattice X) . (( the L_meet of (RSLattice X) . (K,L)),( the L_meet of (RSLattice X) . (K,M))) by Def23 ;
hence  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))) ; ::_thesis: verum
end;

Lm13:  for X being Tolerance_Space
for a, b being Element of (RSLattice X) holds a "/\" (a "\/" b) = a
proof
let X be Tolerance_Space; ::_thesis: for a, b being Element of (RSLattice X) holds a "/\" (a "\/" b) = a
let a, b be Element of (RSLattice X); ::_thesis: a "/\" (a "\/" b) = a
set G = RSLattice X;
reconsider a1 = a, b1 = b as Element of RoughSets X by Def23;
reconsider a9 = a1 as RoughSet of X by Def20;
thus a "/\" (a "\/" b) = the L_join of (RSLattice X) . (( the L_meet of (RSLattice X) . (a1,a1)),( the L_meet of (RSLattice X) . (a1,b1))) by Lm12
.= the L_join of (RSLattice X) . ((a9 _/\_ a9),( the L_meet of (RSLattice X) . (a1,b1))) by Def23
.= a "\/" (a "/\" b) by Th61
.= (a "/\" b) "\/" a by Lm6
.= (b "/\" a) "\/" a by Lm10
.= a by Lm9 ; ::_thesis: verum
end;

registration
let X be Tolerance_Space;
cluster RSLattice X ->  strict Lattice-like ;
coherence
 RSLattice X is Lattice-like
proof
set G = RSLattice X;
thus  for u, v being Element of (RSLattice X) holds u "\/" v = v "\/" u by Lm6; :: according to LATTICES:def_4,LATTICES:def_10 ::_thesis: ( RSLattice X is join-associative & RSLattice X is meet-absorbing & RSLattice X is meet-commutative & RSLattice X is meet-associative & RSLattice X is join-absorbing )
thus  for u, v, w being Element of (RSLattice X) holds u "\/" (v "\/" w) = (u "\/" v) "\/" w by Lm7; :: according to LATTICES:def_5 ::_thesis: ( RSLattice X is meet-absorbing & RSLattice X is meet-commutative & RSLattice X is meet-associative & RSLattice X is join-absorbing )
thus  for u, v being Element of (RSLattice X) holds (u "/\" v) "\/" v = v by Lm9; :: according to LATTICES:def_8 ::_thesis: ( RSLattice X is meet-commutative & RSLattice X is meet-associative & RSLattice X is join-absorbing )
thus  for u, v being Element of (RSLattice X) holds u "/\" v = v "/\" u by Lm10; :: according to LATTICES:def_6 ::_thesis: ( RSLattice X is meet-associative & RSLattice X is join-absorbing )
thus  for u, v, w being Element of (RSLattice X) holds u "/\" (v "/\" w) = (u "/\" v) "/\" w by Lm11; :: according to LATTICES:def_7 ::_thesis: RSLattice X is join-absorbing
let u, v be Element of (RSLattice X); :: according to LATTICES:def_9 ::_thesis: u "/\" (u "\/" v) = u
thus  u "/\" (u "\/" v) = u by Lm13; ::_thesis: verum
end;
end;

registration
let X be Tolerance_Space;
cluster RSLattice X ->  strict distributive ;
coherence
 RSLattice X is distributive
proof
let u, v, w be Element of (RSLattice X); :: according to LATTICES:def_11 ::_thesis: u "/\" (v "\/" w) = (u "/\" v) "\/" (u "/\" w)
reconsider K = u, L = v, M = w as Element of RoughSets X by Def23;
thus u "/\" (v "\/" w) = the L_join of (RSLattice X) . (( the L_meet of (RSLattice X) . (K,L)),( the L_meet of (RSLattice X) . (K,M))) by Lm12
.= (u "/\" v) "\/" (u "/\" w) ; ::_thesis: verum
end;
end;

definition
let X be Tolerance_Space;
func ERS X ->  RoughSet of X equals :: INTERVA1:def 24
[{},{}];
coherence
 [{},{}] is RoughSet of X
proof
reconsider A = {} as Subset of X by XBOOLE_1:2;
 A = {} X ;
then A1: ( LAp A = {} & UAp A = {} ) by ROUGHS_1:18, ROUGHS_1:19;
 [(LAp A),(UAp A)] in [:(bool the carrier of X),(bool the carrier of X):] by ZFMISC_1:87;
hence  [{},{}] is RoughSet of X by Def13, A1; ::_thesis: verum
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
let X be Tolerance_Space; ::_thesis: for A being RoughSet of X holds (ERS X) _\/_ A = A
let A be RoughSet of X; ::_thesis: (ERS X) _\/_ A = A
A1: LAp (ERS X) = {} by MCART_1:7;
A2: UAp (ERS X) = {} by MCART_1:7;
A3: LAp ((ERS X) _\/_ A) = LAp A by A1, Th56;
 UAp ((ERS X) _\/_ A) = UAp A by A2, Th57;
hence  (ERS X) _\/_ A = A by A3, Def17; ::_thesis: verum
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
reconsider A = [#] X as Subset of X ;
A1: ( LAp A = [#] X & UAp A = [#] X ) by ROUGHS_1:20, ROUGHS_1:21;
 [(LAp A),(UAp A)] in [:(bool the carrier of X),(bool the carrier of X):] by ZFMISC_1:87;
hence  [([#] X),([#] X)] is RoughSet of X by Def13, A1; ::_thesis: verum
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
let X be Tolerance_Space; ::_thesis: for A being RoughSet of X holds (TRS X) _/\_ A = A
let A be RoughSet of X; ::_thesis: (TRS X) _/\_ A = A
A1: LAp (TRS X) = [#] X by MCART_1:7;
A2: UAp (TRS X) = [#] X by MCART_1:7;
A3: LAp ((TRS X) _/\_ A) = (LAp (TRS X)) /\ (LAp A) by Th58
.= LAp A by A1, XBOOLE_1:28 ;
UAp ((TRS X) _/\_ A) = (UAp (TRS X)) /\ (UAp A) by Th59
.= UAp A by A2, XBOOLE_1:28 ;
hence  (TRS X) _/\_ A = A by A3, Def17; ::_thesis: verum
end;

registration
let X be Tolerance_Space;
cluster RSLattice X ->  strict bounded ;
coherence
 RSLattice X is bounded
proof
thus  RSLattice X is lower-bounded :: according to LATTICES:def_15 ::_thesis: RSLattice X is upper-bounded
proof
reconsider E = ERS X as Element of RoughSets X by Lm14;
reconsider e = E as Element of (RSLattice X) by Def23;
take  e ; :: according to LATTICES:def_13 ::_thesis: for b1 being Element of the carrier of (RSLattice X) holds
( e "/\" b1 = e & b1 "/\" e = e )
let u be Element of (RSLattice X); ::_thesis: ( e "/\" u = e & u "/\" e = e )
reconsider K = u as Element of RoughSets X by Def23;
reconsider E9 = E, K9 = K as RoughSet of X by Def20;
e "\/" u = E9 _\/_ K9 by Def23
.= u by Th69 ;
then  ( e "/\" u = e & u "/\" e = e ) by LATTICES:def_9;
hence  ( e "/\" u = e & u "/\" e = e ) ; ::_thesis: verum
end;
thus  RSLattice X is upper-bounded ::_thesis: verum
proof
reconsider E = TRS X as Element of RoughSets X by Lm15;
reconsider e = E as Element of (RSLattice X) by Def23;
take  e ; :: according to LATTICES:def_14 ::_thesis: for b1 being Element of the carrier of (RSLattice X) holds
( e "\/" b1 = e & b1 "\/" e = e )
let u be Element of (RSLattice X); ::_thesis: ( e "\/" u = e & u "\/" e = e )
reconsider K = u as Element of RoughSets X by Def23;
reconsider E9 = E, K9 = K as RoughSet of X by Def20;
e "/\" u = E9 _/\_ K9 by Def23
.= u by Th70 ;
then  ( e "\/" u = e & u "\/" e = e ) by LATTICES:def_8;
hence  ( e "\/" u = e & u "\/" e = e ) ; ::_thesis: verum
end;
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
let X be Tolerance_Space; ::_thesis: 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 ) )
let A, B be Element of (RSLattice X); ::_thesis: 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 ) )
let A9, B9 be RoughSet of X; ::_thesis: ( A = A9 & B = B9 implies ( A [= B iff ( LAp A9 c= LAp B9 & UAp A9 c= UAp B9 ) ) )
assume A1: ( A = A9 & B = B9 ) ; ::_thesis: ( A [= B iff ( LAp A9 c= LAp B9 & UAp A9 c= UAp B9 ) )
A2: ( A is Element of RoughSets X & B is Element of RoughSets X ) by Def23;
thus  ( A [= B implies ( LAp A9 c= LAp B9 & UAp A9 c= UAp B9 ) ) ::_thesis: ( LAp A9 c= LAp B9 & UAp A9 c= UAp B9 implies A [= B )
proof
assume  A [= B ; ::_thesis: ( LAp A9 c= LAp B9 & UAp A9 c= UAp B9 )
then  A "\/" B = B by LATTICES:def_3;
then  A9 _\/_ B9 = B9 by A1, Def23, A2;
then  ( (LAp A9) \/ (LAp B9) = LAp B9 & (UAp A9) \/ (UAp B9) = UAp B9 ) by Th56, Th57;
hence  ( LAp A9 c= LAp B9 & UAp A9 c= UAp B9 ) by XBOOLE_1:11; ::_thesis: verum
end;
assume  ( LAp A9 c= LAp B9 & UAp A9 c= UAp B9 ) ; ::_thesis: A [= B
then  ( (LAp A9) \/ (LAp B9) = LAp B9 & (UAp A9) \/ (UAp B9) = UAp B9 ) by XBOOLE_1:12;
then  ( LAp (A9 _\/_ B9) = LAp B9 & UAp (A9 _\/_ B9) = UAp B9 ) by Th56, Th57;
then A3: A9 _\/_ B9 = B9 by Def17;
reconsider A1 = A, B1 = B as Element of RoughSets X by Def23;
reconsider A9 = A1, B9 = B1 as RoughSet of X by Def20;
 A9 _\/_ B9 = A "\/" B by Def23;
hence  A [= B by A3, A1, LATTICES:def_3; ::_thesis: verum
end;

Lm16:  for X being Tolerance_Space holds RSLattice X is complete
proof
let X be Tolerance_Space; ::_thesis: RSLattice X is complete
let Y be Subset of (RSLattice X); :: according to VECTSP_8:def_6 ::_thesis: ex b1 being Element of the carrier of (RSLattice X) st
( b1 is_less_than Y & ( for b2 being Element of the carrier of (RSLattice X) holds
( not b2 is_less_than Y or b2 [= b1 ) ) )
 ex a being Element of (RSLattice X) st
( a is_less_than Y & ( for b being Element of (RSLattice X) st b is_less_than Y holds
b [= a ) )
proof
percases ( Y is empty or not Y is empty ) ;
supposeA1: Y is empty ; ::_thesis: ex a being Element of (RSLattice X) st
( a is_less_than Y & ( for b being Element of (RSLattice X) st b is_less_than Y holds
b [= a ) )
take a = Top (RSLattice X); ::_thesis: ( a is_less_than Y & ( for b being Element of (RSLattice X) st b is_less_than Y holds
b [= a ) )
 for q being Element of (RSLattice X) st q in Y holds
a [= q by A1;
hence  a is_less_than Y by LATTICE3:def_16; ::_thesis: for b being Element of (RSLattice X) st b is_less_than Y holds
b [= a
let b be Element of (RSLattice X); ::_thesis: ( b is_less_than Y implies b [= a )
assume  b is_less_than Y ; ::_thesis: b [= a
thus  b [= a by LATTICES:19; ::_thesis: verum
end;
supposeA2: not Y is empty ; ::_thesis: ex a being Element of (RSLattice X) st
( a is_less_than Y & ( for b being Element of (RSLattice X) st b is_less_than Y holds
b [= a ) )
set A1 =  {  (LAp a1) where a1 is RoughSet of X : a1 in Y  }  ;
set A2 =  {  (UAp a1) where a1 is RoughSet of X : a1 in Y  }  ;
set a9 = [(meet  {  (LAp a1) where a1 is RoughSet of X : a1 in Y  }  ),(meet  {  (UAp a1) where a1 is RoughSet of X : a1 in Y  }  )];
consider f being set  such that
A3: f in Y by A2, XBOOLE_0:def_1;
 Y is Subset of (RoughSets X) by Def23;
then reconsider f = f as RoughSet of X by A3, Def20;
A4: LAp f in  {  (LAp a1) where a1 is RoughSet of X : a1 in Y  }  by A3;
then A5:  {  (LAp a1) where a1 is RoughSet of X : a1 in Y  }  <> {} ;
consider g being set  such that
A6: g in Y by A2, XBOOLE_0:def_1;
 Y is Subset of (RoughSets X) by Def23;
then reconsider g = g as RoughSet of X by A6, Def20;
 UAp g in  {  (UAp a1) where a1 is RoughSet of X : a1 in Y  }  by A6;
then A7:  {  (UAp a1) where a1 is RoughSet of X : a1 in Y  }  <> {} ;
A8: meet  {  (LAp a1) where a1 is RoughSet of X : a1 in Y  }  c= the carrier of X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in meet  {  (LAp a1) where a1 is RoughSet of X : a1 in Y  }  or x in the carrier of X )
assume  x in meet  {  (LAp a1) where a1 is RoughSet of X : a1 in Y  }  ; ::_thesis: x in the carrier of X
then A9: for Z being set st Z in  {  (LAp a1) where a1 is RoughSet of X : a1 in Y  }  holds
x in Z by SETFAM_1:def_1;
consider c being set  such that
A10: c in  {  (LAp a1) where a1 is RoughSet of X : a1 in Y  }  by A4;
consider c9 being RoughSet of X such that
A11: ( c = LAp c9 & c9 in Y ) by A10;
A12: c in bool the carrier of X by A11;
 x in c by A10, A9;
hence  x in the carrier of X by A12; ::_thesis: verum
end;
 [(meet  {  (LAp a1) where a1 is RoughSet of X : a1 in Y  }  ),(meet  {  (UAp a1) where a1 is RoughSet of X : a1 in Y  }  )] is RoughSet of X
proof
 meet  {  (UAp a1) where a1 is RoughSet of X : a1 in Y  }  c= the carrier of X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in meet  {  (UAp a1) where a1 is RoughSet of X : a1 in Y  }  or x in the carrier of X )
assume  x in meet  {  (UAp a1) where a1 is RoughSet of X : a1 in Y  }  ; ::_thesis: x in the carrier of X
then A13: for Z being set st Z in  {  (UAp a1) where a1 is RoughSet of X : a1 in Y  }  holds
x in Z by SETFAM_1:def_1;
consider c being set  such that
A14: c in  {  (UAp a1) where a1 is RoughSet of X : a1 in Y  }  by A7, XBOOLE_0:def_1;
consider c9 being RoughSet of X such that
A15: ( c = UAp c9 & c9 in Y ) by A14;
A16: c c= the carrier of X by A15;
 x in c by A14, A13;
hence  x in the carrier of X by A16; ::_thesis: verum
end;
then  [(meet  {  (LAp a1) where a1 is RoughSet of X : a1 in Y  }  ),(meet  {  (UAp a1) where a1 is RoughSet of X : a1 in Y  }  )] in [:(bool the carrier of X),(bool the carrier of X):] by A8, ZFMISC_1:87;
hence  [(meet  {  (LAp a1) where a1 is RoughSet of X : a1 in Y  }  ),(meet  {  (UAp a1) where a1 is RoughSet of X : a1 in Y  }  )] is RoughSet of X by Def13; ::_thesis: verum
end;
then reconsider a9 = [(meet  {  (LAp a1) where a1 is RoughSet of X : a1 in Y  }  ),(meet  {  (UAp a1) where a1 is RoughSet of X : a1 in Y  }  )] as RoughSet of X ;
 a9 in RoughSets X by Def20;
then reconsider a = a9 as Element of (RSLattice X) by Def23;
take  a ; ::_thesis: ( a is_less_than Y & ( for b being Element of (RSLattice X) st b is_less_than Y holds
b [= a ) )
thus  a is_less_than Y ::_thesis: for b being Element of (RSLattice X) st b is_less_than Y holds
b [= a
proof
let q be Element of (RSLattice X); :: according to LATTICE3:def_16 ::_thesis: ( not q in Y or a [= q )
assume A17: q in Y ; ::_thesis: a [= q
 q in the carrier of (RSLattice X) ;
then  q in RoughSets X by Def23;
then reconsider q9 = q as RoughSet of X by Def20;
consider q1, q2 being Subset of X such that
A18: q9 = [q1,q2] by Th55;
A19: q1 = LAp q9 by A18, MCART_1:7;
then A20: q1 in  {  (LAp a1) where a1 is RoughSet of X : a1 in Y  }  by A17;
 meet  {  (LAp a1) where a1 is RoughSet of X : a1 in Y  }  c= LAp q9
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in meet  {  (LAp a1) where a1 is RoughSet of X : a1 in Y  }  or x in LAp q9 )
assume  x in meet  {  (LAp a1) where a1 is RoughSet of X : a1 in Y  }  ; ::_thesis: x in LAp q9
hence  x in LAp q9 by A19, A20, SETFAM_1:def_1; ::_thesis: verum
end;
then A21: LAp a9 c= LAp q9 by MCART_1:7;
A22: UAp a9 = meet  {  (UAp a1) where a1 is RoughSet of X : a1 in Y  }  by MCART_1:7;
A23: q2 = UAp q9 by A18, MCART_1:7;
then A24: q2 in  {  (UAp a1) where a1 is RoughSet of X : a1 in Y  }  by A17;
 meet  {  (UAp a1) where a1 is RoughSet of X : a1 in Y  }  c= UAp q9
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in meet  {  (UAp a1) where a1 is RoughSet of X : a1 in Y  }  or x in UAp q9 )
assume  x in meet  {  (UAp a1) where a1 is RoughSet of X : a1 in Y  }  ; ::_thesis: x in UAp q9
hence  x in UAp q9 by A23, A24, SETFAM_1:def_1; ::_thesis: verum
end;
hence  a [= q by A21, Th71, A22; ::_thesis: verum
end;
thus  for b being Element of (RSLattice X) st b is_less_than Y holds
b [= a ::_thesis: verum
proof
let b be Element of (RSLattice X); ::_thesis: ( b is_less_than Y implies b [= a )
assume A25: b is_less_than Y ; ::_thesis: b [= a
 b is Element of RoughSets X by Def23;
then reconsider b9 = b as RoughSet of X by Def20;
reconsider a9 = a as RoughSet of X ;
A26: for q being Element of (RSLattice X) st q in Y holds
b [= q by A25, LATTICE3:def_16;
 for Z1 being set st Z1 in  {  (LAp a1) where a1 is RoughSet of X : a1 in Y  }  holds
LAp b9 c= Z1
proof
let Z1 be set ; ::_thesis: ( Z1 in  {  (LAp a1) where a1 is RoughSet of X : a1 in Y  }  implies LAp b9 c= Z1 )
assume  Z1 in  {  (LAp a1) where a1 is RoughSet of X : a1 in Y  }  ; ::_thesis: LAp b9 c= Z1
then consider c1 being RoughSet of X such that
A27: ( Z1 = LAp c1 & c1 in Y ) ;
reconsider c19 = c1 as Element of (RSLattice X) by A27;
 b [= c19 by A25, A27, LATTICE3:def_16;
hence  LAp b9 c= Z1 by A27, Th71; ::_thesis: verum
end;
then A28: LAp b9 c= meet  {  (LAp a1) where a1 is RoughSet of X : a1 in Y  }  by A5, SETFAM_1:5;
 meet  {  (LAp a1) where a1 is RoughSet of X : a1 in Y  }  c= LAp a9 by MCART_1:7;
then A29: LAp b9 c= LAp a9 by A28, XBOOLE_1:1;
 for Z1 being set st Z1 in  {  (UAp a1) where a1 is RoughSet of X : a1 in Y  }  holds
UAp b9 c= Z1
proof
let Z1 be set ; ::_thesis: ( Z1 in  {  (UAp a1) where a1 is RoughSet of X : a1 in Y  }  implies UAp b9 c= Z1 )
assume  Z1 in  {  (UAp a1) where a1 is RoughSet of X : a1 in Y  }  ; ::_thesis: UAp b9 c= Z1
then consider c2 being RoughSet of X such that
A30: ( Z1 = UAp c2 & c2 in Y ) ;
reconsider c29 = c2 as Element of (RSLattice X) by A30;
 b [= c29 by A26, A30;
hence  UAp b9 c= Z1 by A30, Th71; ::_thesis: verum
end;
then A31: UAp b9 c= meet  {  (UAp a1) where a1 is RoughSet of X : a1 in Y  }  by A7, SETFAM_1:5;
 meet  {  (UAp a1) where a1 is RoughSet of X : a1 in Y  }  c= UAp a9 by MCART_1:7;
then  UAp b9 c= UAp a9 by A31, XBOOLE_1:1;
hence  b [= a by A29, Th71; ::_thesis: verum
end;
end;
end;
end;
hence  ex b1 being Element of the carrier of (RSLattice X) st
( b1 is_less_than Y & ( for b2 being Element of the carrier of (RSLattice X) holds
( not b2 is_less_than Y or b2 [= b1 ) ) ) ; ::_thesis: verum
end;

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