MATHMORP

:: Preliminaries to Mathematical Morphology and Its Properties
::  by Yuzhong Ding and Xiquan Liang
::
:: Received January 7, 2005
:: Copyright (c) 2005-2026 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SUBSET_1, PRE_TOPC, EUCLID, ARYTM_3, STRUCT_0, REALSET1,
      ARYTM_1, VALUED_2, TARSKI, SUPINF_2, XBOOLE_0, RELAT_1, CARD_1, MONOID_0,
      RLVECT_1, CONVEX1, XXREAL_0, REAL_1, RLTOPSP1, MATHMORP, ALGSTR_0;
 notations TARSKI, ORDINAL1, XBOOLE_0, SUBSET_1, NUMBERS, XCMPLX_0, XXREAL_0,
      DOMAIN_1, STRUCT_0, ALGSTR_0, PRE_TOPC, XREAL_0, REAL_1, RLVECT_1,
      RLTOPSP1, EUCLID, RUSUB_4;
 constructors DOMAIN_1, REAL_1, JORDAN1, CONVEX1, BINOP_2, RUSUB_4;
 registrations XXREAL_0, XREAL_0, STRUCT_0, EUCLID, RLVECT_1, ORDINAL1;
 requirements REAL, BOOLE, SUBSET, NUMERALS, ARITHM;
 definitions TARSKI, XBOOLE_0;
 equalities XBOOLE_0, SUBSET_1, ALGSTR_0, RUSUB_4;
 expansions TARSKI, XBOOLE_0;
 theorems XBOOLE_1, XCMPLX_1, TARSKI, SUBSET_1, ZFMISC_1, XBOOLE_0, JORDAN1,
      XREAL_1, RLTOPSP1, RLVECT_1, RLVECT_4;

begin :: 1. The definition of Erosion and Dilation and their
::          Algebraic Properties
:: Translation of X according to p

definition
  let T be non empty addMagma, p be Element of T, X be Subset of T;
  func X+p -> Subset of T equals
  {q + p where q is Element of T : q in X};
  coherence
  proof
    now
      let x be object;
      assume x in {q+p where q is Point of T : q in X};
      then ex q being Point of T st x = q + p & q in X;
      hence x in the carrier of T;
    end;
    hence thesis by TARSKI:def 3;
  end;
end;

:: Reflected of X

definition
  let T be non empty addLoopStr, X be Subset of T;
  func X! -> Subset of T equals
  {-q where q is Point of T : q in X};
  coherence
  proof
    now
      let x be object;
      assume x in {-q where q is Point of T : q in X};
      then ex q being Point of T st x = -q & q in X;
      hence x in the carrier of T;
    end;
    hence thesis by TARSKI:def 3;
  end;
end;

:: Set Erosion

definition
  let T be non empty addMagma, X,B be Subset of T;
  func X (-) B -> Subset of T equals
  {y where y is Point of T : B+y c= X};
  coherence
  proof
    now
      let x be object;
      assume x in {y where y is Point of T : B+y c= X};
      then ex q being Point of T st x = q & B+q c= X;
      hence x in the carrier of T;
    end;
    hence thesis by TARSKI:def 3;
  end;

end;

:: Set Dilation

notation
  let T be non empty addLoopStr;
  let A, B be Subset of T;
  synonym A(+)B for A + B;
end;

reserve T for non empty Abelian
  add-associative right_zeroed right_complementable RLSStruct,
  X,Y,Z,B,C,B1,B2 for Subset of T,
  x,y,p for Point of T;

theorem Th1:
  for T being add-associative right_zeroed right_complementable
    non empty RLSStruct,
       B being Subset of T holds
  (B!)! = B
proof
  let T be add-associative right_zeroed right_complementable
    non empty RLSStruct,
      B be Subset of T;
  thus (B!)! c= B
  proof
    let x be object;
    assume x in (B!)!;
    then consider q being Element of T such that
A1: x = -q and
A2: q in B!;
    ex q1 being Element of T st q = -q1 & q1 in B by A2;
    hence thesis by A1;
  end;
  let x be object;
  assume
A3: x in B;
  then reconsider xx = x as Point of T;
  -xx in {-q where q is Point of T : q in B}by A3;
  then -(-xx) in {-q where q is Point of T : q in B!};
  hence thesis;
end;

theorem Th2:
  {0.T} + x = {x}
proof
  thus {0.T} + x c= {x}
  proof
    let a be object;
    assume a in {0.T} + x;
    then consider q being Point of T such that
A1: a=q+x and
A2: q in {0.T};
    {q} c= {0.T} by A2,ZFMISC_1:31;
    then q = 0.T by ZFMISC_1:18;
    then {a} c= {x} by A1;
    hence thesis by ZFMISC_1:31;
  end;
  let a be object;
  assume a in {x};
  then {a} c= {x} by ZFMISC_1:31;
  then a = x by ZFMISC_1:18;
  then
A3: a = 0.T + x;
  0.T in {0.T} by ZFMISC_1:31;
  hence thesis by A3;
end;

theorem Th3:
  B1 c= B2 implies B1+p c= B2+p
proof
  assume
A1: B1 c= B2;
  let p1 be object;
  assume p1 in B1+p;
  then ex p2 being Point of T st p1 =p2+p & p2 in B1;
  hence thesis by A1;
end;

theorem Th4:
  for X st X = {} holds X+x = {}
proof
  let X;
  assume
A1: X = {};
  now
    given y being object such that
A2: y in X+x;
    ex y1 being Point of T st y = y1+x & y1 in X by A2;
    hence contradiction by A1;
  end;
  hence thesis by XBOOLE_0:def 1;
end;

theorem
  X (-) {0.T} = X
proof
  thus X (-) {0.T} c= X
  proof
    let x be object;
    assume x in X (-) {0.T};
    then ex y being Point of T st x=y & {0.T}+y c= X;
    then {x} c= X by Th2;
    hence thesis by ZFMISC_1:31;
  end;
  let x be object;
  assume
A1: x in X;
  then reconsider xx=x as Point of T;
  {x} c= X by A1,ZFMISC_1:31;
  then {0.T}+xx c= X by Th2;
  hence thesis;
end;

Lm1: {x}+y = {y}+x
proof
  thus {x}+y c= {y}+x
  proof
    let x1 be object;
    assume x1 in {x}+y;
    then consider p1 being Point of T such that
A1: x1=p1+y and
A2: p1 in {x};
    {p1} c= {x} by A2,ZFMISC_1:31; then
A3: x1=x+y by A1,ZFMISC_1:18;
    y in {y} by TARSKI:def 1;
    hence thesis by A3;
  end;
  let x1 be object;
  assume x1 in {y}+x;
  then consider p1 being Point of T such that
A4: x1=p1+x and
A5: p1 in {y};
  {p1} c= {y} by A5,ZFMISC_1:31;
  then
A6: x1=x+y by A4,ZFMISC_1:18;
  x in {x}by TARSKI:def 1;
  hence thesis by A6;
end;

theorem
  X (+) {0.T} = X
proof
  thus X (+) {0.T} c= X
  proof
    let x be object;
    assume x in X (+) {0.T};
    then consider y,z being Point of T such that
A1: x=y+z & y in X and
A2: z in {0.T};
    {z} c= {0.T} by A2,ZFMISC_1:31;
    then z = 0.T by ZFMISC_1:18;
    hence thesis by A1;
  end;
  let x be object;
  assume
A3: x in X;
  then reconsider x as Point of T;
  0.T in {0.T} by TARSKI:def 1;
  then
  x+0.T in {y+z where y,z is Point of T : y in X & z in {0.T}} by A3;
  hence thesis;
end;

theorem
  X (+) {x} = X+x
proof
  thus X (+) {x} c= X+x
  proof
    let p be object;
    assume p in X (+) {x};
    then consider y,z being Point of T such that
A1: p=y+z and
A2: y in X and
A3: z in {x};
    {z} c= {x} by A3,ZFMISC_1:31;
    then p=y+x by A1,ZFMISC_1:18;
    hence thesis by A2;
  end;
  let p be object;
  assume p in X+x;
  then
A4: ex q being Point of T st p=q+x & q in X;
  x in {x} by TARSKI:def 1;
  hence thesis by A4;
end;

theorem Th8:
  for X,Y st Y = {} holds X (-) Y = the carrier of T
proof
  let X,Y;
  assume
A1: Y = {};
  {y where y is Point of T:Y+y c= X} = the carrier of T
  proof
    thus {y where y is Point of T:Y+y c= X} c= the carrier of T
    proof
      let x be object;
      assume x in {y where y is Point of T:Y+y c= X};
      then ex y being Point of T st x=y & Y+y c= X;
      hence thesis;
    end;
    let x be object;
    assume x in the carrier of T;
    then reconsider a=x as Point of T;
    Y+a = {} by A1,Th4;
    then Y+a c= X;
    hence thesis;
  end;
  hence thesis;
end;

theorem Th9:
  X c= Y implies X (-) B c= Y (-) B & X (+) B c= Y (+) B
proof
  assume
A1: X c= Y;
  thus X (-) B c= Y (-) B
  proof
    let p be object;
    assume p in X (-) B;
    then consider p1 being Point of T such that
A2: p = p1 and
A3: B+p1 c= X;
    B+p1 c= Y by A1,A3;
    hence thesis by A2;
  end;
  let p be object;
  assume p in X (+) B;
  then ex p1,p2 being Point of T st p = p1+p2 & p1 in X & p2 in B;
  hence thesis by A1;
end;

theorem Th10:
  B1 c= B2 implies X (-) B2 c= X (-) B1 & X (+) B1 c= X (+) B2
proof
  assume
A1: B1 c= B2;
  thus X (-) B2 c= X (-) B1
  proof
    let p be object;
    assume p in X (-) B2;
    then consider p1 being Point of T such that
A2: p = p1 and
A3: B2+p1 c= X;
    B1+p1 c= B2 + p1 by A1,Th3;
    then B1+p1 c= X by A3;
    hence thesis by A2;
  end;
  let p be object;
  assume p in X (+) B1;
  then ex x,b being Point of T st p = x+b & x in X & b in B1;
  hence thesis by A1;
end;

theorem
  0.T in B implies X (-) B c= X & X c= X (+) B
proof
  assume
A1: 0.T in B;
  thus X (-) B c= X
  proof
    let p be object;
    assume p in X (-) B;
    then consider p1 being Point of T such that
A2: p = p1 and
A3: B+p1 c= X;
    0.T+p1 in {q+p1 where q is Point of T:q in B} by A1;
    then 0.T+p1 in X by A3;
    hence thesis by A2;
  end;
  let p be object;
  assume
A4: p in X;
  then reconsider p as Point of T;
  p + 0.T in {x+b where x,b is Point of T:x in X & b in B} by A1,A4;
  hence thesis;
end;

theorem Th12:
  X (+) Y = Y (+) X
proof
  thus X (+) Y c= Y (+) X
  proof
    let p be object;
    assume p in X (+) Y; then
    ex p1,p2 being Point of T st p = p1+p2 & p1 in X & p2 in Y;
    hence thesis;
  end;
  let p be object;
  assume p in Y (+) X;
  then ex p1,p2 being Point of T st p = p1+p2 & p1 in Y & p2 in X;
  hence thesis;
end;

Lm2:
  p - x + x = p & p + x - x = p
  proof
    p + x - x = p + (x - x) by RLVECT_1:def 3
      .= p + 0.T by RLVECT_1:15
      .= p;
    hence thesis by RLVECT_1:28;
  end;

theorem Th13:
  Y+y c= X+x iff Y+(y-x) c= X
proof
  thus Y+y c= X+x implies Y+(y-x) c= X
  proof
    assume
A1: Y+y c= X+x;
    let p be object;
    assume p in Y+(y-x);
    then consider q1 being Point of T such that
A2: p = q1 + (y-x) and
A3: q1 in Y;
    reconsider p as Point of T by A2;
    p = q1 + y - x by A2,RLVECT_1:28; then
A4: p + x = q1 + y by Lm2;
    q1 + y in {q+y where q is Point of T:q in Y} by A3;
    then p + x in X + x by A1,A4;
    then consider p1 being Point of T such that
A5: p+x =p1+x and
A6: p1 in X;
    p +x-x= p1 by A5,Lm2;
    hence thesis by A6,Lm2;
  end;
  assume
A7: Y+(y-x) c= X;
  let p be object;
  assume p in Y+y;
  then consider q1 being Point of T such that
A8: p = q1 + y and
A9: q1 in Y;
  reconsider p as Point of T by A8;
  p-x = q1 + (y -x) & q1+(y-x) in {q+(y-x) where q is Point of T
  :q in Y} by A8,A9,RLVECT_1:28;
  then (p-x)+x in {q+x where q is Point of T:q in X}by A7;
  hence thesis by Lm2;
end;

theorem Th14:
  (X+p) (-) Y = (X (-) Y)+p
proof
  thus (X+p) (-) Y c= (X (-) Y)+p
  proof
    let x be object;
    assume x in (X+p) (-) Y;
    then consider y being Point of T such that
A1: x = y and
A2: Y+y c= X+p;
    Y+(y-p) c= X by A2,Th13;
    then y-p in {y1 where y1 is Point of T:Y+y1 c= X};
    then (y-p)+p in {q+p where q is Point of T:q in X (-) Y};
    hence thesis by A1,Lm2;
  end;
  let x be object;
  assume x in (X (-) Y)+p;
  then consider y being Point of T such that
A3: x = y+p and
A4: y in X (-) Y;
  reconsider x as Point of T by A3;
  x-p = y & ex y2 being Point of T st y = y2 & Y+y2 c= X by A3,A4,Lm2;
  then Y + x c= X + p by Th13;
  hence thesis;
end;

theorem Th15:
  (X+p) (+) Y = (X (+) Y)+p
proof
  thus (X+p) (+) Y c= (X (+) Y)+p
  proof
    let x be object;
    assume x in (X+p) (+) Y;
    then consider x2,y2 being Point of T such that
A1: x = x2+y2 and
A2: x2 in X+p and
A3: y2 in Y;
    consider x3 being Point of T such that
A4: x2 = x3+p & x3 in X by A2;
    x=x3+y2+p & x3+y2 in X (+) Y by A1,A3,A4,RLVECT_1:def 3;
    hence thesis;
  end;
  let x be object;
  assume x in (X (+) Y)+p;
  then consider x2 being Point of T such that
A5: x = x2+p and
A6: x2 in X (+) Y;
  consider x3,y3 being Point of T such that
A7: x2 = x3+y3 and
A8: x3 in X and
A9: y3 in Y by A6;
A10: x3+p in X+p by A8;
  x=x3+p+y3 by A5,A7,RLVECT_1:def 3;
  hence thesis by A9,A10;
end;

theorem Th16:
  (X+x)+y = X+(x+y)
proof
  thus X+x+y c= X+(x+y)
  proof
    let p be object;
    assume p in (X+x)+y;
    then consider x2 being Point of T such that
A1: p = x2+y and
A2: x2 in X+x;
    consider x3 being Point of T such that
A3: x2 = x3+x and
A4: x3 in X by A2;
    p=x3+(x+y) by A1,A3,RLVECT_1:def 3;
    hence thesis by A4;
  end;
  let p be object;
  assume p in X+(x+y);
  then consider x2 being Point of T such that
A5: p = x2+(x+y) & x2 in X;
  p = x2 + x + y & x2+x in X+x by A5,RLVECT_1:def 3;
  hence thesis;
end;

theorem Th17:
  X (-) (Y+p) = (X (-) Y)+(-p)
proof
  thus X (-) (Y+p) c= (X (-) Y)+(-p)
  proof
    let x be object;
    assume x in X (-) (Y+p);
    then consider y being Point of T such that
A1: x = y and
A2: (Y+p)+y c= X;
    Y+(y+p) c= X by A2,Th16;
    then y+p in {y1 where y1 is Point of T:Y+y1 c= X};
    then y+p-p in (X (-) Y)+(-p);
    hence thesis by A1,Lm2;
  end;
  let x be object;
  assume x in (X (-) Y)+(-p);
  then consider y being Point of T such that
A3: x = y+(-p) and
A4: y in X (-) Y;
  reconsider x as Point of T by A3;
  x+p = y-p+p by A3; then
A5: x+p =y by Lm2;
  ex y2 being Point of T st y = y2 & Y+y2 c= X by A4;
  then Y+p+x c= X by A5,Th16;
  hence thesis;
end;

theorem
  X (+) (Y+p) = (X (+) Y)+p
proof
  thus X (+) (Y+p) c= (X (+) Y)+p
  proof
    let x be object;
    assume x in X (+) (Y+p);
    then consider x2,y2 being Point of T such that
A1: x = x2+y2 & x2 in X and
A2: y2 in Y+p;
    consider y3 being Point of T such that
A3: y2 = y3+p & y3 in Y by A2;
    x=x2+y3+p & x2+y3 in X (+) Y by A1,A3,RLVECT_1:def 3;
    hence thesis;
  end;
  let x be object;
  assume x in (X (+) Y)+p;
  then consider x2 being Point of T such that
A4: x = x2+p and
A5: x2 in X (+) Y;
  consider x3,y3 being Point of T such that
A6: x2 = x3+y3 and
A7: x3 in X and
A8: y3 in Y by A5;
A9: y3+p in Y+p by A8;
  x=x3+(y3+p) by A4,A6,RLVECT_1:def 3;
  hence thesis by A7,A9;
end;

theorem Th19:
  x in X implies B+x c= B (+) X
proof
  assume
A1: x in X;
  let y be object;
  assume y in B+x;
  then ex y1 being Point of T st y = y1+x & y1 in B;
  hence thesis by A1;
end;

theorem Th20:
  X c= (X (+) B) (-) B
proof
  let x be object;
  assume
A1: x in X;
  then consider x1 being Point of T such that
A2: x1=x;
  B+x1 c= B (+) X by A1,A2,Th19;
  then x in (B (+) X) (-) B by A2;
  hence thesis by Th12;
end;

theorem Th21:
  X+0.T = X
proof
  thus X+0.T c= X
  proof
    let x be object;
    assume x in X+0.T;
    then ex q being Point of T st x = q + 0.T & q in X;
    hence thesis;
  end;
  let x be object;
  assume
A1: x in X;
  then reconsider x1=x as Point of T;
  x1=x1+0.T;
  hence thesis by A1;
end;

theorem
  X (-) {x} = X+(-x)
proof
  thus X (-) {x} c= X+(-x)
  proof
    let y be object;
    assume y in X (-) {x};
    then consider p being Point of T such that
A1: p=y and
A2: {x}+p c= X;
    {p}+x c= X by A2,Lm1;
    then {p}+x+(-x) c= X+(-x) by Th3;
    then {p}+(x+(-x)) c= X+(-x) by Th16;
    then {p}+0.T c= X+(-x) by RLVECT_1:5;
    then {p} c= X+(-x) by Th21;
    hence thesis by A1,ZFMISC_1:31;
  end;
  let y be object;
  assume y in X+(-x);
  then consider p being Point of T such that
A3: y=p+(-x) and
A4: p in X;
  reconsider y as Point of T by A3;
  y = p - x by A3;
  then
A5: y+x = p by Lm2;
  {x}+y c= X
  proof
    let q be object;
    assume q in {x}+y;
    then consider qq being Point of T such that
A6: q=qq+y and
A7: qq in {x};
    {qq} c= {x} by A7,ZFMISC_1:31;
    hence thesis by A4,A5,A6,ZFMISC_1:18;
  end;
  hence thesis;
end;

Lm3: (X (-) B) (+) B c= X
proof
  let x be object;
  assume x in (X (-) B) (+) B;
  then consider y1,y2 being Point of T such that
A1: x=y1+y2 and
A2: y1 in X (-) B and
A3: y2 in B;
  consider y being Point of T such that
A4: y1=y and
A5: B+y c= X by A2;
  x in B+y by A1,A3,A4;
  hence thesis by A5;
end;

theorem Th23:
  X (-) (Y (+) Z) = (X (-) Y) (-) Z
proof
A1: (X (-) Y) (+) Y c= X by Lm3;
  thus X (-) (Y (+) Z) c= (X (-) Y) (-) Z
  proof
    let p be object;
    assume p in X (-) (Y (+) Z);
    then consider x being Point of T such that
A2: p = x and
A3: (Y (+) Z)+x c= X;
    (Y+x) (+) Z c= X by A3,Th15;
    then Z (+) (Y+x) c= X by Th12;
    then
A4: (Z (+) (Y+x)) (-) (Y+x) c= X (-) (Y+x) by Th9;
    Z c= (Z (+) (Y+x)) (-) (Y+x) by Th20;
    then Z c= X (-) (Y+x) by A4;
    then Z c= (X (-) Y)+(-x) by Th17;
    then Z+x c= (X (-) Y)+(-x)+x by Th3;
    then Z+x c= (X (-) Y)+((-x)+x) by Th16;
    then Z+x c= (X (-) Y)+(x-x);
    then Z+x c= (X (-) Y)+0.T by RLVECT_1:15;
    then Z+x c= X (-) Y by Th21;
    hence thesis by A2;
  end;
  let p be object;
  assume p in (X (-) Y) (-) Z;
  then consider y being Point of T such that
A5: p = y and
A6: Z+y c= X (-) Y;
  (Z+y) (+) Y c= (X (-) Y) (+) Y by A6,Th9;
  then (Z+y) (+) Y c= X by A1;
  then (Z (+) Y)+y c= X by Th15;
  then p in X (-) (Z (+) Y) by A5;
  hence thesis by Th12;
end;

theorem
  X (-) (Y (+) Z) = (X (-) Z) (-) Y
proof
  X (-) (Y (+) Z) = X (-) (Z (+) Y) by Th12
    .=X (-) Z (-) Y by Th23;
  hence thesis;
end;

theorem
  X (+) (Y (-) Z) c= (X (+) Y) (-) Z
proof
  let x be object;
  assume x in X (+) (Y (-) Z);
  then consider a,b being Point of T such that
A1: x=a+b and
A2: a in X and
A3: b in Y (-) Z;
  ex c being Point of T st b=c & Z+c c= Y by A3;
  then Z+b+a c= Y+a by Th3;
  then
A4: Z+(b+a) c= Y+a by Th16;
  Y+a c= Y (+) X by A2,Th19;
  then Z+(b+a) c= Y (+) X by A4;
  then x in (Y (+) X) (-) Z by A1;
  hence thesis by Th12;
end;

theorem
  X (+) (Y (+) Z) = (X (+) Y) (+) Z
proof
  thus X (+) ( Y (+) Z) c= (X (+) Y) (+) Z
  proof
    let p be object;
    assume p in X (+) ( Y (+) Z);
    then consider x1,p2 being Point of T such that
A1: p = x1+p2 & x1 in X and
A2: p2 in Y (+) Z;
    consider y,z being Point of T such that
A3: p2=y+z & y in Y and
A4: z in Z by A2;
    set p3=x1+y;
    p=x1+y+z & p3 in X (+) Y by A1,A3,RLVECT_1:def 3;
    hence thesis by A4;
  end;
  let p be object;
  assume p in (X (+) Y) (+) Z;
  then consider x1,p2 being Point of T such that
A5: p = x1+p2 and
A6: x1 in X (+) Y and
A7: p2 in Z;
  consider y,z being Point of T such that
A8: x1=y+z and
A9: y in X and
A10: z in Y by A6;
  set p3=z+p2;
  p=y+(z+p2) & p3 in Y (+) Z by A5,A7,A8,A10,RLVECT_1:def 3;
  hence thesis by A9;
end;

theorem Th27:
  (B\/C)+y = (B+y) \/ (C+y)
proof
  thus (B\/C)+y c= (B+y) \/ (C+y)
  proof
    let x be object;
    assume x in (B\/C)+y;
    then consider y2 being Point of T such that
A1: x=y2+y and
A2: y2 in B\/C;
    y2 in B or y2 in C by A2,XBOOLE_0:def 3;
    then x in {y1+y where y1 is Point of T : y1 in B} or x in {y1+y
    where y1 is Point of T:y1 in C} by A1;
    hence thesis by XBOOLE_0:def 3;
  end;
  let x be object;
  assume x in (B+y) \/ (C+y);
  then x in B+y or x in C+y by XBOOLE_0:def 3;
  then consider y2 being Point of T such that
A3: x=y2+y & y2 in B or x=y2+y & y2 in C;
  y2 in B\/C by A3,XBOOLE_0:def 3;
  hence thesis by A3;
end;

theorem Th28:
  (B/\C)+y = (B+y) /\ (C+y)
proof
  thus (B/\C)+y c= (B+y) /\ (C+y)
  proof
    let x be object;
    assume x in (B/\C)+y;
    then consider y2 being Point of T such that
A1: x=y2+y and
A2: y2 in B/\C;
    y2 in C by A2,XBOOLE_0:def 4;
    then
A3: x in {y1+y where y1 is Point of T:y1 in C} by A1;
    y2 in B by A2,XBOOLE_0:def 4;
    then x in {y1+y where y1 is Point of T:y1 in B} by A1;
    hence thesis by A3,XBOOLE_0:def 4;
  end;
  let x be object;
  assume
A4: x in (B+y) /\ (C+y);
  then x in B+y by XBOOLE_0:def 4;
  then consider y3 being Point of T such that
A5: x=y3+y and
A6: y3 in B;
  x in C+y by A4,XBOOLE_0:def 4;
  then consider y2 being Point of T such that
A7: x=y2+y and
A8: y2 in C;
  y2+y-y=y3 by A5,A7,Lm2; then
A9: y2=y3 by Lm2;
  then y2 in B/\C by A6,A8,XBOOLE_0:def 4;
  hence thesis by A5,A9;
end;

theorem
  X (-) (B\/C) = (X (-) B)/\(X (-) C)
proof
  thus X (-) (B\/C) c= (X (-) B)/\(X (-) C)
  proof
    let x be object;
    assume x in X (-) (B\/C);
    then consider y being Point of T such that
A1: x = y and
A2: (B\/C)+y c= X;
A3: (B+y)\/(C+y) c= X by A2,Th27;
    then C+y c= X by XBOOLE_1:11;
    then
A4: x in {y1 where y1 is Point of T:C+y1 c= X} by A1;
    B+y c= X by A3,XBOOLE_1:11;
    then x in {y1 where y1 is Point of T:B+y1 c= X} by A1;
    hence thesis by A4,XBOOLE_0:def 4;
  end;
  let x be object;
  assume
A5: x in (X (-) B)/\(X (-) C);
  then x in X (-) B by XBOOLE_0:def 4;
  then consider y being Point of T such that
A6: x = y and
A7: B+y c= X;
  x in X (-) C by A5,XBOOLE_0:def 4;
  then ex y2 being Point of T st x = y2 & C+y2 c= X;
  then (B+y)\/(C+y) c= X by A6,A7,XBOOLE_1:8;
  then (B\/C)+y c= X by Th27;
  hence thesis by A6;
end;

theorem
  X (+) (B\/C) = (X (+) B)\/(X (+) C)
proof
  thus X (+) (B\/C) c= (X (+) B)\/(X (+) C)
  proof
    let x be object;
    assume x in X (+) (B\/C);
    then consider y3,y4 being Point of T such that
A1: x = y3+y4 & y3 in X and
A2: y4 in (B\/C);
    y4 in B or y4 in C by A2,XBOOLE_0:def 3;
    then
    x in {y1+y2 where y1,y2 is Point of T :y1 in X & y2 in B} or x
    in {y1+y2 where y1,y2 is Point of T:y1 in X & y2 in C} by A1;
    hence thesis by XBOOLE_0:def 3;
  end;
  let x be object;
  assume x in (X (+) B)\/(X (+) C);
  then x in X (+) B or x in X (+) C by XBOOLE_0:def 3;
  then consider y3,y4 being Point of T such that
A3: x=y3+y4 & y3 in X & y4 in B or x=y3+y4 & y3 in X & y4 in C;
  y4 in B\/C by A3,XBOOLE_0:def 3;
  hence thesis by A3;
end;

theorem
  (X (-) B)\/(Y (-) B) c= (X\/Y) (-) B
proof
  let x be object;
  assume x in (X (-) B)\/(Y (-) B);
  then x in X (-) B or x in Y (-) B by XBOOLE_0:def 3;
  then consider y being Point of T such that
A1: x=y & B+y c= X or x=y & B+y c= Y;
  B+y c= X \/ Y
  by A1,XBOOLE_0:def 3;
  hence thesis by A1;
end;

theorem
  (X\/Y) (+) B = (X (+) B)\/(Y (+) B)
proof
  thus (X\/Y) (+) B c= (X (+) B)\/(Y (+) B)
  proof
    let x be object;
    assume x in (X\/Y) (+) B;
    then consider y1,y2 being Point of T such that
A1: x=y1+y2 and
A2: y1 in X\/Y and
A3: y2 in B;
    y1 in X or y1 in Y by A2,XBOOLE_0:def 3;
    then
    x in {y3+y4 where y3,y4 is Point of T:y3 in X & y4 in B} or x
    in {y3+y4 where y3,y4 is Point of T:y3 in Y & y4 in B} by A1,A3;
    hence thesis by XBOOLE_0:def 3;
  end;
  let x be object;
  assume x in (X (+) B)\/(Y (+) B);
  then x in X (+) B or x in Y (+) B by XBOOLE_0:def 3;
  then consider y1,y2 being Point of T such that
A4: x=y1+y2 & y1 in X & y2 in B or x=y1+y2 & y1 in Y & y2 in B;
  y1 in X\/Y by A4,XBOOLE_0:def 3;
  hence thesis by A4;
end;

theorem
  (X/\Y) (-) B = (X (-) B)/\(Y (-) B)
proof
  thus (X/\Y) (-) B c= (X (-) B)/\(Y (-) B)
  proof
    let x be object;
    assume x in (X/\Y) (-) B;
    then consider y being Point of T such that
A1: x=y and
A2: B+y c= X/\Y;
    B+y c= Y by A2,XBOOLE_1:18;
    then
A3: x in {y1 where y1 is Point of T:B+y1 c= Y} by A1;
    B+y c= X by A2,XBOOLE_1:18;
    then x in {y1 where y1 is Point of T:B+y1 c= X} by A1;
    hence thesis by A3,XBOOLE_0:def 4;
  end;
  let x be object;
  assume
A4: x in (X (-) B)/\(Y (-) B);
  then x in X (-) B by XBOOLE_0:def 4;
  then consider y being Point of T such that
A5: x=y and
A6: B+y c= X;
  x in Y (-) B by A4,XBOOLE_0:def 4;
  then
A7: ex y2 being Point of T st x=y2 & B+y2 c= Y;
  B+y c= X/\Y
  by A5,A6,A7,XBOOLE_0:def 4;
  hence thesis by A5;
end;

theorem Th34:
  (X/\Y) (+) B c= (X (+) B)/\(Y (+) B)
proof
  let x be object;
  assume x in (X/\Y) (+) B;
  then consider y1,y2 being Point of T such that
A1: x=y1+y2 and
A2: y1 in X/\Y and
A3: y2 in B;
  y1 in Y by A2,XBOOLE_0:def 4;
  then
A4: x in {y3+y4 where y3,y4 is Point of T:y3 in Y & y4 in B} by A1,A3;
  y1 in X by A2,XBOOLE_0:def 4;
  then
  x in {y3+y4 where y3,y4 is Point of T:y3 in X & y4 in B} by A1,A3;
  hence thesis by A4,XBOOLE_0:def 4;
end;

theorem
  B (+) (X/\Y) c= (B (+) X)/\(B (+) Y)
proof
  B (+) (X/\Y) = (X/\Y) (+) B by Th12;
  then B (+) (X/\Y) c= (X (+) B)/\(Y (+) B) by Th34;
  then B (+) (X/\Y) c= (B (+) X)/\(Y (+) B) by Th12;
  hence thesis by Th12;
end;

theorem
  (B (-) X)\/(B (-) Y) c= B (-) (X/\Y)
proof
  let x be object;
  assume x in (B (-) X)\/(B (-) Y);
  then x in B (-) X or x in B (-) Y by XBOOLE_0:def 3;
  then consider y being Point of T such that
A1: x=y & X+y c= B or x=y & Y+y c= B;
  (X+y)/\(Y+y) c= B
  proof
    let a be object;
    assume
A2: a in (X+y)/\(Y+y);
    then
A3: a in X+y by XBOOLE_0:def 4;
A4: a in Y+y by A2,XBOOLE_0:def 4;
    per cases by A1;
    suppose
      X+y c= B;
      hence thesis by A3;
    end;
    suppose
      Y+y c= B;
      hence thesis by A4;
    end;
  end;
  then (X/\Y)+y c= B by Th28;
  hence thesis by A1;
end;

theorem Th37:
  (X` (-) B)` = X (+) B!
proof
  thus ((X`) (-) B)` c= X (+) B!
  proof
    let x be object;
    assume
A1: x in ((X`) (-) B)`;
    then reconsider x1=x as Point of T;
    not x in (X`) (-) B by A1,XBOOLE_0:def 5;
    then not B+x1 c= X`;
    then B+x1 meets X by SUBSET_1:23;
    then consider y being object such that
A2: y in (B+x1) and
A3: y in X by XBOOLE_0:3;
    reconsider y1=y as Point of T by A2;
    consider b1 being Point of T such that
A4: y = b1+x1 & b1 in B by A2;
    x1 = y1 - b1 & -b1 in B! by A4,Lm2;
    hence thesis by A3;
  end;
  let x be object;
  assume x in X (+) B!;
  then consider x1,b1 being Point of T such that
A5: x=x1+b1 and
A6: x1 in X and
A7: b1 in B!;
  reconsider xx=x as Point of T by A5;
  consider b2 being Point of T such that
A8: b1=-b2 and
A9: b2 in B by A7;
  x=x1-b2 by A5,A8;
  then
A10: xx+b2=x1 by Lm2;
  b2+xx in {pb+xx where pb is Point of T:pb in B}by A9;
  then
A11: B+xx meets X by A6,A10,XBOOLE_0:3;
  not xx in ((X`) (-) B)
  proof
    assume xx in ((X`) (-) B);
    then ex yy being Point of T st xx=yy & B+yy c= X`;
    hence contradiction by A11,SUBSET_1:23;
  end;
  hence thesis by XBOOLE_0:def 5;
end;

theorem Th38:
  (X (-) B)` = X` (+) B!
proof
  thus (X (-) B)` c= X` (+) B!
  proof
    let x be object;
    assume
A1: x in (X (-) B)`;
    then reconsider x1=x as Point of T;
    not x in X (-) B by A1,XBOOLE_0:def 5;
    then not B+x1 c= X;
    then B+x1 meets X` by SUBSET_1:24;
    then consider y being object such that
A2: y in B+x1 and
A3: y in X` by XBOOLE_0:3;
    reconsider y1=y as Point of T by A2;
    consider b1 being Point of T such that
A4: y = b1+x1 & b1 in B by A2;
    x1 = y1 - b1 & -b1 in B! by A4,Lm2;
    hence thesis by A3;
  end;
  let x be object;
  assume x in X` (+) B!;
  then consider x1,b1 being Point of T such that
A5: x=x1+b1 and
A6: x1 in X` and
A7: b1 in B!;
  reconsider xx=x as Point of T by A5;
  consider q being Point of T such that
A8: b1=-q and
A9: q in B by A7;
  xx=x1-q by A5,A8;
  then
A10: xx+q=x1 by Lm2;
  q+xx in {q1+xx where q1 is Point of T:q1 in B}by A9;
  then
A11: B+xx meets X` by A6,A10,XBOOLE_0:3;
  not xx in (X (-) B)
  proof
    assume xx in (X (-) B);
    then ex yy being Point of T st xx=yy & B+yy c= X;
    hence contradiction by A11,SUBSET_1:24;
  end;
  hence thesis by XBOOLE_0:def 5;
end;

begin
:: 2. The definition of Adjunction Opening and Closing and
::    their Algebraic Properties
:: Adjunction Opening

definition
  let T be non empty addLoopStr,X,B be Subset of T;
  func X (O) B -> Subset of T equals
  (X (-) B) (+) B;
  coherence;
end;

:: Adjunction Closing

definition
  let T be non empty addLoopStr,X,B be Subset of T;
  func X (o) B -> Subset of T equals
  (X (+) B) (-) B;
  coherence;
end;

theorem
  (X` (O) B!)` = X (o) B
proof
  (X` (O) B!)` =(((X` (-) B!)` (-) B)`)` by Th37
    .=X (+) (B!)! (-) B by Th37
    .=X (+) B (-) B by Th1;
  hence thesis;
end;

theorem
  (X` (o) B!)` = X (O) B
proof
  (X` (o) B!)` =(X` (+) B!)` (+) (B!)! by Th38
    .=(X` (+) B!)` (+) B by Th1
    .=(X (-) B)`` (+) B by Th38;
  hence thesis;
end;

theorem Th41:
  X (O) B c= X & X c= X (o) B
proof
  thus X (O) B c= X
  proof
    let x be object;
    assume x in X (O) B;
    then consider y1,y2 being Point of T such that
A1: x=y1+y2 and
A2: y1 in X (-) B and
A3: y2 in B;
    consider y being Point of T such that
A4: y1=y and
A5: B+y c= X by A2;
    x in B+y by A1,A3,A4;
    hence thesis by A5;
  end;
  thus thesis by Th20;
end;

theorem Th42:
  X (O) X = X
proof
  thus X (O) X c= X by Th41;
  let x be object;
  assume
A1: x in X;
  then reconsider x1=x as Point of T;
  X+0.T c= X by Th21;
  then 0.T in X (-) X;
  then x1+0.T in (X (-) X) (+) X by A1;
  hence thesis;
end;

theorem
  (X (O) B) (-) B c= X (-) B & (X (O) B) (+) B c= X (+) B
proof
  X (O) B c= X by Th41;
  hence thesis by Th9;
end;

theorem
  X (-) B c= (X (o) B) (-) B & X (+) B c= (X (o) B) (+) B
proof
  X c= X (o) B by Th41;
  hence thesis by Th9;
end;

theorem Th45:
  X c= Y implies X (O) B c= Y (O) B & X (o) B c= Y (o) B
proof
  assume
A1: X c= Y;
  thus X (O) B c= Y (O) B
  proof
    let x be object;
    assume x in X (O) B;
    then consider x2,b2 being Point of T such that
A2: x=x2+b2 and
A3: x2 in X (-) B and
A4: b2 in B;
    consider y being Point of T such that
A5: x2=y and
A6: B+y c= X by A3;
    B+y c= Y by A1,A6;
    then x2 in {y1 where y1 is Point of T:B+y1 c= Y}by A5;
    hence thesis by A2,A4;
  end;
  let x be object;
  assume x in X (o) B;
  then consider x2 being Point of T such that
A7: x=x2 and
A8: B+x2 c= X (+) B;
  X (+) B c= Y (+) B by A1,Th9;
  then B+x2 c= Y (+) B by A8;
  hence thesis by A7;
end;

theorem Th46:
  (X+p) (O) Y = (X (O) Y)+p
proof
  thus (X+p) (O) Y = ((X (-) Y)+p) (+) Y by Th14
    .= (X (O) Y)+p by Th15;
end;

theorem
  (X+p) (o) Y = (X (o) Y)+p
proof
  thus (X+p) (o) Y = ((X (+) Y)+p) (-) Y by Th15
    .= (X (o) Y)+p by Th14;
end;

theorem
  C c= B implies X (O) B c= (X (-) C) (+) B
proof
  assume
A1: C c= B;
  let x be object;
  assume x in X (O) B;
  then consider x1,b1 being Point of T such that
A2: x=x1+b1 and
A3: x1 in X (-) B and
A4: b1 in B;
  consider x2 being Point of T such that
A5: x1=x2 and
A6: B+x2 c= X by A3;
  C+x2 c= B+x2 by A1,Th3;
  then C+x2 c= X by A6;
  then x1 in X (-) C by A5;
  hence thesis by A2,A4;
end;

theorem
  B c= C implies X (o) B c= (X (+) C) (-) B
proof
  assume B c= C;
  then
A1: X (+) B c= X (+) C by Th10;
  let x be object;
  assume x in X (o) B;
  then consider x2 being Point of T such that
A2: x=x2 and
A3: B+x2 c= X (+) B;
  B+x2 c= X (+) C by A3,A1;
  hence thesis by A2;
end;

theorem Th50:
  X (+) Y = (X (o) Y) (+) Y & X (-) Y = (X (O) Y) (-) Y
proof
  (X (o) Y) (+) Y =(X (+) Y) (O) Y;
  then
A1: (X (o) Y) (+) Y c= X (+) Y by Th41;
  X c= X (o) Y by Th41;
  then X (+) Y c= (X (o) Y) (+) Y by Th9;
  hence X (+) Y = (X (o) Y) (+) Y by A1;
  (X (O) Y) (-) Y = (X (-) Y) (o) Y;
  hence X (-) Y c= (X (O) Y) (-) Y by Th41;
  X (O) Y c= X by Th41;
  hence thesis by Th9;
end;

theorem
  X (+) Y = (X (+) Y) (O) Y & X (-) Y = (X (-) Y) (o) Y
proof
  (X (+) Y) (O) Y =(X (o) Y) (+) Y;
  hence X (+) Y = (X (+) Y) (O) Y by Th50;
  (X (-) Y) (o) Y =(X (O) Y) (-) Y;
  hence thesis by Th50;
end;

theorem
  (X (O) B) (O) B = X (O) B
proof
  thus (X (O) B) (O) B c= X (O) B by Th41;
  let x be object;
  assume x in X (O) B;
  then consider x1,b1 being Point of T such that
A1: x=x1+b1 and
A2: x1 in X (-) B and
A3: b1 in B;
  consider x2 being Point of T such that
A4: x1=x2 and
A5: B+x2 c= X by A2;
  (B+x2) (O) B c= X (O) B by A5,Th45;
  then (B (O) B)+x2 c= X (O) B by Th46;
  then B+x2 c= X (O) B by Th42;
  then x1 in {x4 where x4 is Point of T:B+x4 c= X (O) B}by A4;
  hence thesis by A1,A3;
end;

theorem
  (X (o) B) (o) B = X (o) B by Th50;

theorem
  X (O) B c= (X \/ Y) (O) B
proof
  X c= X \/ Y by XBOOLE_1:7;
  hence thesis by Th45;
end;

theorem
  B = B (O) B1 implies X (O) B c= X (O) B1
proof
  assume
A1: B = B (O) B1;
  let x be object;
  assume x in X (O) B;
  then consider x1,b1 being Point of T such that
A2: x=x1+b1 and
A3: x1 in X (-) B and
A4: b1 in B;
  consider x2 being Point of T such that
A5: x1=x2 & B+x2 c= X by A3;
  consider x3,b2 being Point of T such that
A6: b1=x3+b2 and
A7: x3 in B (-) B1 and
A8: b2 in B1 by A1,A4;
  consider x4 being Point of T such that
A9: x3=x4 and
A10: B1+x4 c= B by A7;
  B1+x4+x2 c= B+x2 by A10,Th3;
  then B1+x3+x1 c= X by A5,A9;
  then B1+(x3+x1) c= X by Th16;
  then x1+x3 in X (-) B1;
  then x1+x3+b2 in (X (-) B1) (+) B1 by A8;
  hence thesis by A2,A6,RLVECT_1:def 3;
end;

begin
:: 3.The definition of Scaling transformation and its Algebraic Properties
:: Scaling transformation

definition
  let t be Real, T be non empty RLSStruct,A be Subset of T;
  func t(.)A -> Subset of T equals
  {t*a where a is Point of T : a in A};
  coherence
  proof
    now
      let x be object;
      assume x in {t*a where a is Point of T:a in A};
      then ex q being Point of T st x = t*q & q in A;
      hence x in the carrier of T;
    end;
    hence thesis by TARSKI:def 3;
  end;
end;

reserve t,s,r1 for Real;

theorem
  for X being Subset of T st X = {} holds 0(.)X = {}
proof
  let X be Subset of T;
  assume
A1: X = {};
  now
    given x being object such that
A2: x in 0(.)X;
    ex a being Point of T st x = 0 * a & a in X by A2;
    hence contradiction by A1;
  end;
  hence thesis by XBOOLE_0:def 1;
end;

reserve n for Element of NAT;
reserve X,Y,B1,B2 for Subset of TOP-REAL n;
reserve x,y for Point of TOP-REAL n;

theorem
  for X being non empty Subset of TOP-REAL n holds 0(.)X = {0.TOP-REAL n}
proof
  set T = TOP-REAL n;
  let X be non empty Subset of TOP-REAL n;
  thus 0(.)X c= {0.T}
  proof
    let x be object;
    assume x in 0(.)X;
    then ex a being Point of T st x=0 * a & a in X;
    then x = 0.T by RLVECT_1:10;
    hence thesis by ZFMISC_1:31;
  end;
  let x be object;
  set d = the Element of X;
  reconsider d1=d as Point of T;
  assume x in {0.T};
  then {x} c= {0.T} by ZFMISC_1:31;
  then x = 0.T by ZFMISC_1:18;
  then x = 0 * d1 by RLVECT_1:10;
  hence thesis;
end;

theorem Th58:
  1(.)X = X
proof
  thus 1(.)X c= X
  proof
    let x be object;
    assume x in 1(.)X;
    then ex z being Point of TOP-REAL n st x=1*z & z in X;
    hence thesis by RLVECT_1:def 8;
  end;
  let x be object;
  assume
A1: x in X;
  then reconsider x1=x as Point of TOP-REAL n;
  x1=1*x1 by RLVECT_1:def 8;
  hence thesis by A1;
end;

theorem
  2(.)X c= X (+) X
proof
  let x be object;
  assume x in 2(.)X;
  then consider z being Point of TOP-REAL n such that
A1: x=2*z and
A2: z in X;
  x = (1+1)*z by A1
    .= 1*z+1*z by RLVECT_1:def 6
    .= z + 1*z by RLVECT_1:def 8
    .= z + z by RLVECT_1:def 8;
  hence thesis by A2;
end;

theorem Th60:
  (t*s)(.)X = t(.)(s(.)X)
proof
  thus (t*s)(.)X c= t(.)(s(.)X)
  proof
    let x be object;
    assume x in (t*s)(.)X;
    then consider z being Point of TOP-REAL n such that
A1: x = (t*s) * z & z in X;
    x = t*(s*z) & s*z in s(.)X by A1,RLVECT_1:def 7;
    hence thesis;
  end;
  let x be object;
  assume x in t(.)(s(.)X);
  then consider z being Point of TOP-REAL n such that
A2: x = t * z and
A3: z in s(.)X;
  consider z1 being Point of TOP-REAL n such that
A4: z = s * z1 and
A5: z1 in X by A3;
  x = (t*s)*z1 by A2,A4,RLVECT_1:def 7;
  hence thesis by A5;
end;

theorem Th61:
  X c= Y implies t(.)X c= t(.)Y
proof
  assume
A1: X c= Y;
  let x be object;
  assume x in t(.)X;
  then ex a being Point of TOP-REAL n st x = t*a & a in X;
  hence thesis by A1;
end;

theorem Th62:
  t(.)(X+x) = t(.)X+t*x
proof
  thus t(.)(X+x) c= t(.)X+t*x
  proof
    let b be object;
    assume b in t(.)(X+x);
    then consider a being Point of TOP-REAL n such that
A1: b = t*a and
A2: a in X+x;
    consider x1 being Point of TOP-REAL n such that
A3: a=x1+x and
A4: x1 in X by A2;
A5: t*x1 in t(.)X by A4;
    b=t*x1+t*x by A1,A3,RLVECT_1:def 5;
    hence thesis by A5;
  end;
  let b be object;
  assume b in t(.)X+t*x;
  then consider x1 being Point of TOP-REAL n such that
A6: b = x1+t*x and
A7: x1 in t(.)X;
  consider a being Point of TOP-REAL n such that
A8: x1=t*a and
A9: a in X by A7;
A10: a+x in X+x by A9;
  b=t*(a+x) by A6,A8,RLVECT_1:def 5;
  hence thesis by A10;
end;

theorem Th63:
  t(.)(X (+) Y) = t(.)X (+) t(.)Y
proof
  thus t(.)(X (+) Y) c= t(.)X (+) t(.)Y
  proof
    let b be object;
    assume b in t(.)(X (+) Y);
    then consider a being Point of TOP-REAL n such that
A1: b = t*a and
A2: a in X (+) Y;
    consider x,y being Point of TOP-REAL n such that
A3: a=x+y and
A4: x in X & y in Y by A2;
A5: t*x in t(.)X & t*y in t(.)Y by A4;
    b=t*x+t*y by A1,A3,RLVECT_1:def 5;
    hence thesis by A5;
  end;
  let b be object;
  assume b in t(.)X (+) t(.)Y;
  then consider x,y being Point of TOP-REAL n such that
A6: b = x+y and
A7: x in t(.)X and
A8: y in t(.)Y;
  consider y1 being Point of TOP-REAL n such that
A9: y=t*y1 and
A10: y1 in Y by A8;
  consider x1 being Point of TOP-REAL n such that
A11: x=t*x1 and
A12: x1 in X by A7;
A13: x1+y1 in X (+) Y by A12,A10;
  b=t*(x1+y1) by A6,A11,A9,RLVECT_1:def 5;
  hence thesis by A13;
end;

theorem Th64:
  t<>0 implies t(.)(X (-) Y) = t(.)X (-) t(.)Y
proof
  assume
A1: t<>0;
  thus t(.)(X (-) Y) c= t(.)X (-) t(.)Y
  proof
    let b be object;
    assume b in t(.)(X (-) Y);
    then consider a being Point of TOP-REAL n such that
A2: b = t*a and
A3: a in X (-) Y;
    consider x being Point of TOP-REAL n such that
A4: a=x and
A5: Y+x c= X by A3;
    t(.)(Y+x) c= t(.)X by A5,Th61;
    then t(.)Y+t*x c= t(.)X by Th62;
    hence thesis by A2,A4;
  end;
  let b be object;
  assume b in t(.)X (-) t(.)Y;
  then consider x being Point of TOP-REAL n such that
A6: b = x and
A7: t(.)Y+x c= t(.)X;
  (1/t)(.)(t(.)Y+x) c= (1/t)(.)(t(.)X) by A7,Th61;
  then (1/t)(.)(t(.)Y+x) c= (1/t*t)(.)X by Th60;
  then (1/t)(.)(t(.)Y)+(1/t)*x c= (1/t*t)(.)X by Th62;
  then (1/t*t)(.)Y+(1/t)*x c= (1/t*t)(.)X by Th60;
  then 1(.)Y+(1/t)*x c= (1/t*t)(.)X by A1,XCMPLX_1:87;
  then 1(.)Y+(1/t)*x c= 1(.)X by A1,XCMPLX_1:87;
  then Y+(1/t)*x c= 1(.)X by Th58;
  then Y+(1/t)*x c= X by Th58;
  then (1/t)*x in {z where z is Point of TOP-REAL n :Y+z c= X};
  then t*((1/t)*x) in {t*a1 where a1 is Point of TOP-REAL n :a1 in X (-) Y};
  then (1/t*t)*x in t(.)(X (-) Y) by RLVECT_1:def 7;
  then 1*x in t(.)(X (-) Y) by A1,XCMPLX_1:87;
  hence thesis by A6,RLVECT_1:def 8;
end;

theorem
  t<>0 implies t(.)(X (O) Y) = t(.)X (O) t(.)Y
proof
  assume
A1: t<>0;
  t(.)(X (O) Y) =t(.)(X (-) Y) (+) t(.)Y by Th63
    .=t(.)X (-) t(.)Y (+) t(.)Y by A1,Th64;
  hence thesis;
end;

theorem
  t<>0 implies t(.)(X (o) Y) = t(.)X (o) t(.)Y
proof
  assume t<>0;
  then t(.)(X (o) Y) =t(.)(X (+) Y) (-) t(.)Y by Th64
    .=t(.)X (+) t(.)Y (-) t(.)Y by Th63;
  hence thesis;
end;

begin :: 4. The definition of Thinning and Thickening and their
::    Algebraic Properties.
:: "Hit or Miss" Transformation

definition
  let T be non empty RLSStruct,X,B1,B2 be Subset of T;
  func X (*) (B1,B2) -> Subset of T equals
  (X (-) B1) /\ (X` (-) B2);
  coherence;
end;

:: Thickening

definition
  let T be non empty RLSStruct,X,B1,B2 be Subset of T;
  func X (&) (B1,B2) -> Subset of T equals
  X \/ (X (*) (B1,B2));
  coherence;
end;

:: Thinning

definition
  let T be non empty RLSStruct,X,B1,B2 be Subset of T;
  func X (@) (B1,B2) -> Subset of T equals
  X \ (X (*) (B1,B2));
  coherence;
end;

theorem
  B1 = {} implies X (*) (B1,B2) = X` (-) B2
proof
  assume B1 = {};
  then X (*) (B1,B2) = (X` (-) B2) /\ the carrier of TOP-REAL n by Th8;
  hence thesis by XBOOLE_1:28;
end;

theorem
  B2 = {} implies X (*) (B1,B2) = X (-) B1
proof
  assume B2 = {};
  then X (*) (B1,B2) = (X (-) B1)/\(the carrier of TOP-REAL n) by Th8;
  hence thesis by XBOOLE_1:28;
end;

theorem
  0.TOP-REAL n in B1 implies X (*) (B1,B2) c= X
proof
  assume
A1: 0.TOP-REAL n in B1;
  let x be object;
  assume x in X (*) (B1,B2);
  then x in X (-) B1 by XBOOLE_0:def 4;
  then consider y being Point of TOP-REAL n such that
A2: x=y and
A3: B1+y c= X;
  0.TOP-REAL n + y in {z+y where z is Point of TOP-REAL n:z in B1} by A1;
  then x in B1+y by A2;
  hence thesis by A3;
end;

theorem
  0.TOP-REAL n in B2 implies (X (*) (B1,B2)) /\ X = {}
proof
  assume
A1: 0.TOP-REAL n in B2;
  now
    given x being object such that
A2: x in (X (*) (B1,B2)) /\ X;
A3: x in X by A2,XBOOLE_0:def 4;
    x in (X (*) (B1,B2)) by A2,XBOOLE_0:def 4;
    then x in X` (-) B2 by XBOOLE_0:def 4;
    then consider y being Point of TOP-REAL n such that
A4: x=y and
A5: B2+y c= X`;
    0.TOP-REAL n + y in {z+y where z is Point of TOP-REAL n :z in B2} by A1;
    then x in B2+y by A4;
    hence contradiction by A3,A5,XBOOLE_0:def 5;
  end;
  hence thesis by XBOOLE_0:def 1;
end;

theorem
  0.TOP-REAL n in B1 implies X (&) (B1,B2) = X
proof
  assume
A1: 0.TOP-REAL n in B1;
  thus X (&) (B1,B2) c= X
  proof
    let x be object;
    assume
A2: x in X (&) (B1,B2);
    per cases by A2,XBOOLE_0:def 3;
    suppose
      x in X;
      hence thesis;
    end;
    suppose
      x in X (*) (B1,B2);
      then x in X (-) B1 by XBOOLE_0:def 4;
      then consider y being Point of TOP-REAL n such that
A3:   x=y and
A4:   B1+y c= X;
      0.TOP-REAL n + y in {z+y where z is Point of TOP-REAL n:z in B1} by A1;
      then x in B1+y by A3;
      hence thesis by A4;
    end;
  end;
  thus thesis by XBOOLE_1:7;
end;

theorem
  0.TOP-REAL n in B2 implies X (@) (B1,B2) = X
proof
  assume
A1: 0.TOP-REAL n in B2;
  thus X (@) (B1,B2) c= X
  by XBOOLE_0:def 5;
  let x be object;
  assume
A2: x in X;
  not x in (X (*) (B1,B2))
  proof
    assume x in (X (*) (B1,B2));
    then x in X` (-) B2 by XBOOLE_0:def 4;
    then consider y being Point of TOP-REAL n such that
A3: x=y and
A4: B2+y c= X`;
    0.TOP-REAL n + y in {z+y where z is Point of TOP-REAL n:z in B2} by A1;
    then x in B2+y by A3;
    hence contradiction by A2,A4,XBOOLE_0:def 5;
  end;
  hence thesis by A2,XBOOLE_0:def 5;
end;

theorem
  X (@) (B2,B1) = (X` (&) (B1,B2))`
proof
  (X` (&) (B1,B2))` =((X \ ((X` (-) B1) /\ ((X`)` (-) B2)))`)` by SUBSET_1:14
    .=X \ (X (*) (B2,B1));
  hence thesis;
end;

begin :: 5. Properties of Erosion, Dilation, Adjunction Opening,
::    Adjunction Closing on Convex sets

theorem Th74:
  for V being RealLinearSpace, B being Subset of V holds
  B is convex iff
  for x,y be Point of V,r be Real st 0 <= r & r <= 1 & x in B &
  y in B holds r*x + (1-r)*y in B
proof
  let V be RealLinearSpace, B be Subset of V;
  thus B is convex implies for x,y be Point of V,r be Real st 0 <= r &
  r <= 1 & x in B & y in B holds r*x + (1-r)*y in B
  proof
    assume
A1: B is convex;
    for x,y be Point of V,r be Real st 0 <= r & r <= 1 & x in B & y
    in B holds r*x + (1-r)*y in B
    proof
      let x,y be Point of V,r be Real;
      assume that
A2:   0 <= r & r <= 1 and
A3:   x in B & y in B;
      (1-r)*y + r*x in {(1-r1)*y+r1*x where r1 is Real:0<=r1&r1<=1}
        by A2;
      then
A4:   (1-r)*y + r*x in LSeg(x,y) by RLTOPSP1:def 2;
      LSeg(x,y) c= B by A1,A3,JORDAN1:def 1;
      hence thesis by A4;
    end;
    hence thesis;
  end;
  (for x,y be Point of V,r be Real st 0 <= r & r <= 1 & x in B & y
  in B holds r*x + (1-r)*y in B) implies B is convex
  proof
    assume
A5: for x,y be Point of V,r be Real st 0 <= r & r <= 1 & x in
    B & y in B holds r*x + (1-r)*y in B;
    for x,y being Point of V st x in B & y in B holds LSeg(x,y) c= B
    proof
      let x,y be Point of V;
      assume
A6:   x in B & y in B;
      let p be object;
      assume p in LSeg(x,y);
      then p in {(1-r1) * y + r1*x where r1 is Real:0<=r1&r1<=1} by
RLTOPSP1:def 2;
      then ex r1 being Real
           st p = (1-r1) * y + r1 * x & 0<=r1 & r1<=1;
      hence thesis by A5,A6;
    end;
    hence thesis by RLTOPSP1:22;
  end;
  hence thesis;
end;

definition
  let V be RealLinearSpace, B be Subset of V;
  redefine attr B is convex means  :: redefines convex (RLTOPSP1, redefinition) → convex (CONVEX1, definition)

  for x,y be Point of V,r be Real st
  0 <= r & r <= 1 & x in B & y in B holds r*x + (1-r)*y in B;
  compatibility by Th74;
end;

reserve n for Element of NAT;
reserve X,B for Subset of TOP-REAL n;

theorem
  X is convex implies X! is convex
proof
  assume
A1: X is convex;
  for x,y be Point of TOP-REAL n,r be Real st 0 <= r & r <= 1 & x
  in X! & y in X! holds r*x + (1-r)*y in X!
  proof
    let x,y be Point of TOP-REAL n,r be Real;
    assume that
A2: 0 <= r & r <= 1 and
A3: x in X! and
A4: y in X!;
    consider x2 being Point of TOP-REAL n such that
A5: y=-x2 and
A6: x2 in X by A4;
    consider x1 being Point of TOP-REAL n such that
A7: x=-x1 and
A8: x1 in X by A3;
    r*x1 + (1-r)*x2 in X by A1,A2,A8,A6;
    then -(r*x1 + (1-r)*x2) in X!;
    then -(r*x1) - ((1-r)*x2) in X! by RLVECT_1:30;
    then r*(-x1) + -((1-r)*x2) in X! by RLVECT_1:25;
    hence thesis by A7,A5,RLVECT_1:25;
  end;
  hence thesis;
end;

theorem Th76:
  X is convex & B is convex implies X (+) B is convex & X (-) B is convex
proof
  assume that
A1: X is convex and
A2: B is convex;
  for x,y be Point of TOP-REAL n,r be Real st 0 <= r & r <= 1 & x
  in X (+) B & y in X (+) B holds r*x + (1-r)*y in X (+) B
  proof
    let x,y be Point of TOP-REAL n,r be Real;
    assume that
A3: 0 <= r & r <= 1 and
A4: x in X (+) B and
A5: y in X (+) B;
    consider x2,b2 being Point of TOP-REAL n such that
A6: y=x2+b2 and
A7: x2 in X & b2 in B by A5;
    consider x1,b1 being Point of TOP-REAL n such that
A8: x=x1+b1 and
A9: x1 in X & b1 in B by A4;
    r*x1 + (1-r)*x2 in X & r*b1 + (1-r)*b2 in B by A1,A2,A3,A9,A7;
    then
    (r*x1 + (1-r)*x2)+(r*b1 + (1-r)*b2) in {x3+b3 where x3,b3 is Point of
    TOP-REAL n:x3 in X&b3 in B};
    then (r*x1 + (1-r)*x2)+r*b1 + (1-r)*b2 in X (+) B by RLVECT_1:def 3;
    then r*x1 + r*b1+(1-r)*x2 + (1-r)*b2 in X (+) B by RLVECT_1:def 3;
    then (r*x1 + r*b1)+((1-r)*x2 + (1-r)*b2) in X (+) B by RLVECT_1:def 3;
    then r*(x1 + b1)+((1-r)*x2 + (1-r)*b2) in X (+) B by RLVECT_1:def 5;
    hence thesis by A8,A6,RLVECT_1:def 5;
  end;
  hence X (+) B is convex;
  for x,y be Point of TOP-REAL n,r be Real st 0 <= r & r <= 1 & x
  in X (-) B & y in X (-) B holds r*x + (1-r)*y in X (-) B
  proof
    let x,y be Point of TOP-REAL n,r be Real;
    assume that
A10: 0 <= r & r <= 1 and
A11: x in X (-) B & y in X (-) B;
A12: (ex x1 being Point of TOP-REAL n st x=x1 & B+x1 c= X )& ex y1 being
    Point of TOP-REAL n st y=y1 & B+y1 c= X by A11;
    B+(r*x + (1-r)*y) c= X
    proof
      let b1 be object;
      assume b1 in B+(r*x + (1-r)*y);
      then consider b being Point of TOP-REAL n such that
A13:  b1=b+(r*x + (1-r)*y) and
A14:  b in B;
      b+x in B+x & b+y in {b2+y where b2 is Point of TOP-REAL n:b2 in B}
      by A14;
      then r*(b+x) + (1-r)*(b+y) in X by A1,A10,A12;
      then r*b+r*x + (1-r)*(b+y) in X by RLVECT_1:def 5;
      then r*b+r*x + ((1-r)*b+(1-r)*y) in X by RLVECT_1:def 5;
      then r*b+r*x + (1-r)*b+(1-r)*y in X by RLVECT_1:def 3;
      then r*b+r*x + (1*b-r*b)+(1-r)*y in X by RLVECT_1:35;
      then r*b+r*x + 1*b-r*b+(1-r)*y in X by RLVECT_1:def 3;
      then r*x+1*b + r*b-r*b+(1-r)*y in X by RLVECT_1:def 3;
      then r*x+1*b +(1-r)*y in X by RLVECT_4:1;
      then 1*b +(r*x+(1-r)*y) in X by RLVECT_1:def 3;
      hence thesis by A13,RLVECT_1:def 8;
    end;
    hence thesis;
  end;
  hence thesis;
end;

theorem
  X is convex & B is convex implies X (O) B is convex & X (o) B is convex
proof
  assume that
A1: X is convex and
A2: B is convex;
  X (-) B is convex by A1,A2,Th76;
  hence X (O) B is convex by A2,Th76;
  X (+) B is convex by A1,A2,Th76;
  hence thesis by A2,Th76;
end;

theorem
  B is convex & 0 < t & 0 < s implies (s+t)(.)B = s(.)B (+) t(.)B
proof
  assume that
A1: B is convex and
A2: 0 < t & 0 < s;
  thus (s+t)(.)B c= s(.)B (+) t(.)B
  proof
    let x be object;
    assume x in (s+t)(.)B;
    then consider b being Point of TOP-REAL n such that
A3: x=(s+t)*b and
A4: b in B;
A5: t*b in t(.)B by A4;
    x = s*b +t*b & s*b in s(.)B by A3,A4,RLVECT_1:def 6;
    hence thesis by A5;
  end;
  let x be object;
  assume x in s(.)B (+) t(.)B;
  then consider s1,s2 being Point of TOP-REAL n such that
A6: x=s1+s2 and
A7: s1 in s(.)B and
A8: s2 in t(.)B;
  consider b2 being Point of TOP-REAL n such that
A9: s2=t*b2 and
A10: b2 in B by A8;
  consider b1 being Point of TOP-REAL n such that
A11: s1=s*b1 and
A12: b1 in B by A7;
  s/(s+t) < (s+t)/(s+t) by A2,XREAL_1:29,74;
  then s/(s+t) < 1 by A2,XCMPLX_1:60;
  then (s/(s+t))*b1 +(1-s/(s+t))*b2 in B by A1,A2,A12,A10;
  then (s+t)*((s/(s+t))*b1 +(1-s/(s+t))*b2) in {(s+t)*zz where zz is Point of
  TOP-REAL n: zz in B};
  then (s+t)*((s/(s+t))*b1) +(s+t)*((1-s/(s+t))*b2) in (s+t)(.)B by
RLVECT_1:def 5;
  then (s+t)*(s/(s+t))*b1 +(s+t)*((1-s/(s+t))*b2) in (s+t)(.)B by
RLVECT_1:def 7;
  then (s+t)*(s/(s+t))*b1 +(s+t)*(1-s/(s+t))*b2 in (s+t)(.)B by RLVECT_1:def 7;
  then s*b1 +(s+t)*(1-s/(s+t))*b2 in (s+t)(.)B by A2,XCMPLX_1:87;
  then s*b1 +(s+t)*((s+t)/(s+t)-s/(s+t))*b2 in (s+t)(.)B by A2,XCMPLX_1:60;
  then s*b1 +(s+t)*((s+t-s)/(s+t))*b2 in (s+t)(.)B by XCMPLX_1:120;
  hence thesis by A2,A6,A11,A9,XCMPLX_1:87;
end;