:: Continuous, Stable, and Linear Maps of Coherence Spaces
::  by Grzegorz Bancerek
::
:: Received August 30, 1995
:: Copyright (c) 1995-2012 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 XBOOLE_0, FUNCT_1, SUBSET_1, TARSKI, COH_SP, FINSET_1, RELAT_1,
      CLASSES1, ZFMISC_1, FINSUB_1, NUMBERS, CARD_1, ARYTM_3, ARYTM_1,
      MSSUBFAM, FUNCOP_1, PBOOLE, MCART_1, CARD_3, XBOOLEAN, FINSEQ_1,
      LATTICES, EQREL_1, COHSP_1;
 notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1,
      XTUPLE_0, SUBSET_1, CARD_1, NUMBERS,
      REAL_1, NAT_1, MCART_1, RELAT_1, FUNCT_1, FINSEQ_1, FINSET_1, FINSUB_1,
      CLASSES1, COH_SP, PBOOLE, CARD_3, PARTFUN1, FUNCT_2, FUNCOP_1;
 constructors FINSUB_1, REAL_1, NAT_1, CARD_3, PBOOLE, BORSUK_1, COH_SP,
      XTUPLE_0;
 registrations XBOOLE_0, SUBSET_1, RELSET_1, PARTFUN1, FINSET_1, FINSUB_1,
      XREAL_0, NAT_1, FINSEQ_1, ORDINAL1, CARD_1, RELAT_1, XTUPLE_0;
 requirements NUMERALS, BOOLE, SUBSET;
 definitions XBOOLE_0, TARSKI, RELAT_1, COH_SP, CLASSES1, FINSUB_1, XTUPLE_0;
 theorems TARSKI, ENUMSET1, ZFMISC_1, RELAT_1, COH_SP, FUNCT_1, FUNCT_2,
      FINSEQ_1, FINSET_1, FINSUB_1, FUNCOP_1, MCART_1, CARD_1, CLASSES1,
      CARD_2, CARD_3, FUNCT_5, CARD_5, RELSET_1, XBOOLE_0, XBOOLE_1, XCMPLX_1,
      PARTFUN1, XTUPLE_0;
 schemes NAT_1, SUBSET_1, FUNCT_1, FINSET_1, XBOOLE_0, CARD_2;

begin :: Directed Sets

Lm1: for X,Y be non empty set for f be Function of X,Y for x be Element of X
holds for y being set st y in f.x holds y in union Y by TARSKI:def 4;

definition
  let X be set;
  redefine attr X is binary_complete means
  :Def1:
  for A being set st for a,b
  being set st a in A & b in A holds a \/ b in X holds union A in X;
  compatibility
  proof
    thus X is binary_complete implies for A being set st for a,b being set st
    a in A & b in A holds a \/ b in X holds union A in X
    proof
      assume
A1:   for A being set st A c= X & for a,b being set st a in A & b in A
      holds a \/ b in X holds union A in X;
      let A be set;
      assume
A2:   for a,b being set st a in A & b in A holds a \/ b in X;
      A c= X
      proof
        let x be set;
        assume x in A;
        then x \/ x in X by A2;
        hence thesis;
      end;
      hence thesis by A1,A2;
    end;
    assume for A being set st for a,b being set st a in A & b in A holds a \/
    b in X holds union A in X;
    hence for A being set st A c= X & for a,b being set st a in A & b in A
    holds a \/ b in X holds union A in X;
  end;
end;

registration
  cluster finite for Coherence_Space;
  existence by COH_SP:3;
end;

definition
  let X be set;
  func FlatCoh X -> set equals
  CohSp id X;
  correctness;
  func Sub_of_Fin X -> Subset of X means
  : Def3:
  for x being set holds x in it iff x in X & x is finite;
  existence
  proof
    defpred P[set] means $1 is finite;
    thus ex W being Subset of X st for x be set holds x in W iff x in X & P[x]
    from SUBSET_1:sch 1;
  end;
  correctness
  proof
    let X1,X2 be Subset of X;
    assume
A1: not thesis;
    then consider x being set such that
A2: not (x in X1 iff x in X2) by TARSKI:1;
    x in X2 iff not (x in X & x is finite) by A1,A2;
    hence thesis by A1;
  end;
end;

theorem Th1:
  for X,x being set holds x in FlatCoh X iff x = {} or ex y being
  set st x = {y} & y in X
proof
  let X,x be set;
  hereby
    assume
A1: x in FlatCoh X;
    assume x <> {};
    then reconsider y = x as non empty set;
    set z = the Element of y;
    reconsider z as set;
    take z;
    thus x = {z}
    proof
      hereby
        let c be set;
        assume c in x;
        then [z,c] in id X by A1,COH_SP:def 3;
        then c = z by RELAT_1:def 10;
        hence c in {z} by TARSKI:def 1;
      end;
      thus thesis by ZFMISC_1:31;
    end;
    [z,z] in id X by A1,COH_SP:def 3;
    hence z in X by RELAT_1:def 10;
  end;
A2: now
    given a being set such that
A3: x = {a} and
A4: a in X;
    let y,z be set;
    assume y in x & z in x;
    then y = a & z = a by A3,TARSKI:def 1;
    hence [y,z] in id X by A4,RELAT_1:def 10;
  end;
  assume x = {} or ex y being set st x = {y} & y in X;
  hence thesis by A2,COH_SP:1,def 3;
end;

theorem Th2:
  for X being set holds union FlatCoh X = X
proof
  let X be set;
  hereby
    let x be set;
    assume x in union FlatCoh X;
    then consider y being set such that
A1: x in y and
A2: y in FlatCoh X by TARSKI:def 4;
    ex z being set st y = {z} & z in X by A1,A2,Th1;
    hence x in X by A1,TARSKI:def 1;
  end;
  let x be set;
  assume x in X;
  then x in {x} & {x} in FlatCoh X by Th1,TARSKI:def 1;
  hence thesis by TARSKI:def 4;
end;

theorem
  for X being finite subset-closed set holds Sub_of_Fin X = X
proof
  let X be finite subset-closed set;
  thus Sub_of_Fin X c= X;
  let x be set;
  assume
A1: x in X;
  bool x c= X
  proof
    let y be set;
    assume y in bool x;
    hence thesis by A1,CLASSES1:def 1;
  end;
  then x is finite;
  hence thesis by A1,Def3;
end;

registration
  cluster {{}} -> subset-closed binary_complete;
  coherence by COH_SP:3;
  let X be set;
  cluster bool X -> subset-closed binary_complete;
  coherence by COH_SP:2;
  cluster FlatCoh X -> non empty subset-closed binary_complete;
  coherence;
end;

registration
  let C be non empty subset-closed set;
  cluster Sub_of_Fin C -> non empty subset-closed;
  coherence
  proof
    set c = the Element of C;
    {} c= c by XBOOLE_1:2;
    then {} in C by CLASSES1:def 1;
    hence Sub_of_Fin C is non empty by Def3;
    let a,b be set;
    assume
A1: a in Sub_of_Fin C;
    then
A2: a is finite by Def3;
    assume
A3: b c= a;
    then b in C by A1,CLASSES1:def 1;
    hence thesis by A2,A3,Def3;
  end;
end;

theorem
  Web {{}} = {}
proof
  union {{}} = {} by ZFMISC_1:25;
  hence thesis;
end;

scheme
  MinimalElementwrtIncl { a, A() -> set, P[set] }: ex a being set st a in A()
  & P[a] & for b being set st b in A() & P[b] & b c= a holds b = a
provided
A1: a() in A() & P[a()] and
A2: a() is finite
proof
  reconsider a = a() as finite set by A2;
  defpred p[set] means $1 c= a() & P[$1];
  consider X being set such that
A3: for x being set holds x in X iff x in A() & p[x] from XBOOLE_0:sch 1;
A4: bool a is finite & X c= bool a
  proof
    thus bool a is finite;
    let x be set;
    assume x in X;
    then x c= a by A3;
    hence thesis;
  end;
  defpred P[set,set] means $1 c= $2;
A5: for x,y being set st P[x,y] & P[y,x] holds x = y by XBOOLE_0:def 10;
A6: for x,y,z being set st P[x,y] & P[y,z] holds P[x,z] by XBOOLE_1:1;
  reconsider X as finite set by A4;
A7: X <> {} by A1,A3;
  consider x being set such that
A8: x in X & for y being set st y in X & y <> x holds not P[y,x] from
  CARD_2:sch 1(A7,A5,A6);
  take x;
  thus x in A() & P[x] by A3,A8;
  let b be set;
  assume that
A9: b in A() & P[b] and
A10: b c= x;
  x c= a by A3,A8;
  then b c= a by A10,XBOOLE_1:1;
  then b in X by A3,A9;
  hence thesis by A8,A10;
end;

registration
  let C be Coherence_Space;
  cluster finite for Element of C;
  existence
  proof
    reconsider E = {} as Element of C by COH_SP:1;
    take E;
    thus thesis;
  end;
end;

definition
  let X be set;
  attr X is c=directed means
  for Y being finite Subset of X ex a being set st union Y c= a & a in X;
  attr X is c=filtered means
  for Y being finite Subset of X ex a being set st
  (for y being set st y in Y holds a c= y) & a in X;
end;

registration
  cluster c=directed -> non empty for set;
  coherence
  proof
    let X be set;
    assume
    for Y being finite Subset of X ex a being set st union Y c= a & a in X;
    then ex a being set st union {}X c= a & a in X;
    hence thesis;
  end;
  cluster c=filtered -> non empty for set;
  coherence
  proof
    let X be set;
    assume for Y being finite Subset of X ex a being set st (for y being set
    st y in Y holds a c= y) & a in X;
    then
    ex a being set st (for y being set st y in {}X holds a c= y) & a in X;
    hence thesis;
  end;
end;

theorem Th5:
  for X being set st X is c=directed for a,b being set st a in X &
  b in X ex c being set st a \/ b c= c & c in X
proof
  let X be set;
  assume
A1: for Y being finite Subset of X ex a being set st union Y c= a & a in X;
  let a,b be set;
  assume a in X & b in X;
  then
A2: {a,b} is finite Subset of X by ZFMISC_1:32;
  union {a,b} = a \/ b by ZFMISC_1:75;
  hence thesis by A1,A2;
end;

theorem Th6:
  for X being non empty set st for a,b being set st a in X & b in X
  ex c being set st a \/ b c= c & c in X holds X is c=directed
proof
  let X be non empty set such that
A1: for a,b being set st a in X & b in X ex c being set st a \/ b c= c &
  c in X;
  set a = the Element of X;
  defpred P[set] means ex a being set st union $1 c= a & a in X;
  let Y be finite Subset of X;
A2: now
    let x,B be set;
    assume that
A3: x in Y and
    B c= Y;
    assume P[B];
    then consider a being set such that
A4: union B c= a and
A5: a in X;
    consider c being set such that
A6: a \/ x c= c & c in X by A1,A3,A5;
    thus P[B \/ {x}]
    proof
      take c;
      union (B \/ {x}) = (union B) \/ union {x} by ZFMISC_1:78
        .= union B \/ x by ZFMISC_1:25;
      then union (B \/ {x}) c= a \/ x by A4,XBOOLE_1:9;
      hence thesis by A6,XBOOLE_1:1;
    end;
  end;
  union {} c= a by XBOOLE_1:2,ZFMISC_1:2;
  then
A7: P[ {}];
A8: Y is finite;
  thus P[Y] from FINSET_1:sch 2(A8,A7,A2);
end;

theorem
  for X being set st X is c=filtered for a,b being set st a in X & b in
  X ex c being set st c c= a /\ b & c in X
proof
  let X be set;
  assume
A1: for Y being finite Subset of X ex a being set st (for y being set st
  y in Y holds a c= y) & a in X;
  let a,b be set;
  assume a in X & b in X;
  then {a,b} c= X by ZFMISC_1:32;
  then consider c being set such that
A2: for y being set st y in {a,b} holds c c= y and
A3: c in X by A1;
  take c;
  b in {a,b} by TARSKI:def 2;
  then
A4: c c= b by A2;
  a in {a,b} by TARSKI:def 2;
  then c c= a by A2;
  hence thesis by A3,A4,XBOOLE_1:19;
end;

theorem Th8:
  for X being non empty set st for a,b being set st a in X & b in X
  ex c being set st c c= a /\ b & c in X holds X is c=filtered
proof
  let X be non empty set such that
A1: for a,b being set st a in X & b in X ex c being set st c c= a /\ b &
  c in X;
  set a = the Element of X;
  defpred P[set] means ex a being set st (for y being set st y in $1 holds a
  c= y) & a in X;
  let Y be finite Subset of X;
A2: now
    let x,B be set;
    assume that
A3: x in Y and
    B c= Y;
    assume P[B];
    then consider a being set such that
A4: for y being set st y in B holds a c= y and
A5: a in X;
    consider c being set such that
A6: c c= a /\ x and
A7: c in X by A1,A3,A5;
A8: a /\ x c= a & a /\ x c= x by XBOOLE_1:17;
    thus P[B \/ {x}]
    proof
      take c;
      hereby
        let y be set;
        assume y in B \/ {x};
        then y in B or y in {x} by XBOOLE_0:def 3;
        then a c= y & c c= a or y = x & c c= x by A4,A6,A8,TARSKI:def 1
,XBOOLE_1:1;
        hence c c= y by XBOOLE_1:1;
      end;
      thus thesis by A7;
    end;
  end;
  for y being set st y in {} holds a c= y;
  then
A9: P[ {}];
A10: Y is finite;
  thus P[Y] from FINSET_1:sch 2(A10,A9,A2);
end;

theorem Th9:
  for x being set holds {x} is c=directed c=filtered
proof
  let x be set;
  set X = {x};
  hereby
    let Y be finite Subset of X;
    take x;
    union Y c= union X by ZFMISC_1:77;
    hence union Y c= x & x in X by TARSKI:def 1,ZFMISC_1:25;
  end;
  let Y be finite Subset of X;
  take x;
  thus for y be set st y in Y holds x c= y by TARSKI:def 1;
  thus thesis by TARSKI:def 1;
end;

Lm2: now
  let x, y be set;
  thus union {x,y,x \/ y} = union ({x,y} \/ {x \/ y}) by ENUMSET1:3
    .= union {x,y} \/ union {x \/ y} by ZFMISC_1:78
    .= x \/ y \/ union {x \/ y} by ZFMISC_1:75
    .= x \/ y \/ (x \/ y) by ZFMISC_1:25
    .= x \/ y;
end;

theorem
  for x,y being set holds {x,y,x \/ y} is c=directed
proof
  let x,y be set;
  set X = {x,y,x \/ y};
  let A be finite Subset of X;
  take a = x \/ y;
  union X = a by Lm2;
  hence union A c= a by ZFMISC_1:77;
  thus thesis by ENUMSET1:def 1;
end;

theorem
  for x,y being set holds {x,y,x /\ y} is c=filtered
proof
  let x,y be set;
  let A be finite Subset of {x,y,x /\ y};
  take a = x /\ y;
  hereby
    let b be set;
    assume b in A;
    then b = x or b = y or b = x /\ y by ENUMSET1:def 1;
    hence a c= b by XBOOLE_1:17;
  end;
  thus thesis by ENUMSET1:def 1;
end;

registration
  cluster c=directed c=filtered finite for set;
  existence
  proof
    take {{}};
    thus thesis by Th9;
  end;
end;

registration
  let C be non empty set;
  cluster c=directed c=filtered finite for Subset of C;
  existence
  proof
    set x = the Element of C;
    {x} is Subset of C & {x} is c=directed c=filtered finite by Th9,ZFMISC_1:31
;
    hence thesis;
  end;
end;

theorem Th12:
  for X being set holds Fin X is c=directed c=filtered
proof
  let X be set;
  now
    let a,b be set;
    assume
A1: a in Fin X & b in Fin X;
    take c = a \/ b;
    thus a \/ b c= c;
    a c= X & b c= X by A1,FINSUB_1:def 5;
    then a \/ b c= X by XBOOLE_1:8;
    hence c in Fin X by A1,FINSUB_1:def 5;
  end;
  hence Fin X is c=directed by Th6;
  now
    reconsider c = {} as set;
    let a,b be set;
    assume that
    a in Fin X and
    b in Fin X;
    take c;
    thus c c= a /\ b by XBOOLE_1:2;
    thus c in Fin X by FINSUB_1:7;
  end;
  hence thesis by Th8;
end;

registration
  let X be set;
  cluster Fin X -> c=directed c=filtered;
  coherence by Th12;
end;

Lm3: now
  let C be subset-closed non empty set;
  let a be Element of C;
  thus Fin a c= C
  proof
    let x be set;
    assume x in Fin a;
    then x c= a by FINSUB_1:def 5;
    hence thesis by CLASSES1:def 1;
  end;
end;

registration
  let C be subset-closed non empty set;
  cluster preBoolean non empty for Subset of C;
  existence
  proof
    set a = the Element of C;
    reconsider b = Fin a as Subset of C by Lm3;
    take b;
    thus thesis;
  end;
end;

definition
  let C be subset-closed non empty set;
  let a be Element of C;
  redefine func Fin a -> preBoolean non empty Subset of C;
  coherence
  proof
    Fin a c= C
    proof
      let x be set;
      assume x in Fin a;
      then x c= a by FINSUB_1:def 5;
      hence thesis by CLASSES1:def 1;
    end;
    hence thesis;
  end;
end;

theorem Th13:
  for X being non empty set, Y being set st X is c=directed & Y c=
  union X & Y is finite ex Z being set st Z in X & Y c= Z
proof
  let X be non empty set, Y be set;
  set x = the Element of X;
  defpred P[Element of NAT] means for Y being set st Y c= union X & Y is
  finite & card Y = $1 ex Z being set st Z in X & Y c= Z;
  assume
A1: X is c=directed;
A2: now
    let n be Element of NAT;
    assume
A3: P[n];
    thus P[n+1]
    proof
      let Y be set;
      assume that
A4:   Y c= union X and
A5:   Y is finite and
A6:   card Y = n+1;
      reconsider Y9 = Y as non empty set by A6;
      set y = the Element of Y9;
A7:   Y\{y} c= union X by A4,XBOOLE_1:1;
      y in Y;
      then consider Z9 being set such that
A8:   y in Z9 and
A9:   Z9 in X by A4,TARSKI:def 4;
A10:  n+1-1 = n by XCMPLX_1:26;
      {y} c= Y & card {y} = 1 by CARD_1:30,ZFMISC_1:31;
      then card (Y\{y}) = n by A5,A6,A10,CARD_2:44;
      then consider Z being set such that
A11:  Z in X and
A12:  Y\{y} c= Z by A3,A5,A7;
      consider V being set such that
A13:  Z \/ Z9 c= V and
A14:  V in X by A1,A11,A9,Th5;
      take V;
      thus V in X by A14;
      thus Y c= V
      proof
        let x be set;
A15:    x in {y} or not x in {y};
        assume x in Y;
        then x = y or x in Y\{y} by A15,TARSKI:def 1,XBOOLE_0:def 5;
        then x in Z \/ Z9 by A12,A8,XBOOLE_0:def 3;
        hence thesis by A13;
      end;
    end;
  end;
A16: P[ 0 ]
  proof
    let Y be set;
    assume that
    Y c= union X and
    Y is finite and
A17: card Y = 0;
    Y = {} by A17;
    then Y c= x by XBOOLE_1:2;
    hence thesis;
  end;
A18: for n being Element of NAT holds P[n] from NAT_1:sch 1(A16,A2);
  assume that
A19: Y c= union X and
A20: Y is finite;
  reconsider Y9 = Y as finite set by A20;
  card Y = card Y9;
  hence thesis by A18,A19;
end;

notation
  let X be set;
  synonym X is multiplicative for X is cap-closed;
end;

definition
  let X be set;

  attr X is d.union-closed means
  :Def6:
  for A being Subset of X st A is c=directed holds union A in X;
end;

registration
  cluster subset-closed -> multiplicative for set;
  coherence
  proof
    let C be set such that
A1: C is subset-closed;
    let x,y be set;
    x /\ y c= x by XBOOLE_1:17;
    hence thesis by A1,CLASSES1:def 1;
  end;
end;

theorem Th14:
  for C being Coherence_Space, A being c=directed Subset of C
  holds union A in C
proof
  let C be Coherence_Space, A be c=directed Subset of C;
  now
    let a,b be set;
    assume a in A & b in A;
    then ex c being set st a \/ b c= c & c in A by Th5;
    hence a \/ b in C by CLASSES1:def 1;
  end;
  hence thesis by Def1;
end;

registration
  cluster -> d.union-closed for Coherence_Space;
  coherence
  proof
    let C be Coherence_Space;
    let A be Subset of C;
    thus thesis by Th14;
  end;
end;

registration
  cluster multiplicative d.union-closed for Coherence_Space;
  existence
  proof
    set C = the Coherence_Space;
    take C;
    thus thesis;
  end;
end;

definition
  let C be d.union-closed non empty set, A be c=directed Subset of C;
  redefine func union A -> Element of C;
  coherence by Def6;
end;

definition
  let X, Y be set;
  pred X includes_lattice_of Y means
  for a,b being set st a in Y & b in Y holds a /\ b in X & a \/ b in X;
end;

theorem
  for X being non empty set st X includes_lattice_of X holds X is
  c=directed c=filtered
proof
  let X be non empty set such that
A1: for a,b being set st a in X & b in X holds a /\ b in X & a \/ b in X;
  for a,b being set st a in X & b in X ex c being set st a \/ b c= c & c
  in X by A1;
  hence X is c=directed by Th6;
  for a,b being set st a in X & b in X ex c being set st c c= a /\ b & c
  in X by A1;
  hence thesis by Th8;
end;

definition
  let X, x, y be set;
  pred X includes_lattice_of x, y means
  X includes_lattice_of {x, y};
end;

theorem Th16:
  for X,x,y being set holds X includes_lattice_of x, y iff x in X
  & y in X & x /\ y in X & x \/ y in X
proof
  let X,x,y be set;
  thus X includes_lattice_of x, y implies x in X & y in X & x /\ y in X & x \/
  y in X
  proof
A1: x \/ x = x & y \/ y = y;
A2: x in {x,y} & y in {x,y} by TARSKI:def 2;
    assume for a,b being set st a in {x,y} & b in {x,y} holds a /\ b in X & a
    \/ b in X;
    hence thesis by A2,A1;
  end;
  assume
A3: x in X & y in X & x /\ y in X & x \/ y in X;
  let a,b be set;
  assume that
A4: a in {x,y} and
A5: b in {x,y};
A6: b = x or b = y by A5,TARSKI:def 2;
  a = x or a = y by A4,TARSKI:def 2;
  hence thesis by A3,A6;
end;

begin :: Continuous, Stable, and Linear Functions

definition
  let f be Function;
  attr f is union-distributive means
  : Def9:
  for A being Subset of dom f st
  union A in dom f holds f.union A = union (f.:A);
  attr f is d.union-distributive means
  : Def10:
  for A being Subset of dom f st
  A is c=directed & union A in dom f holds f.union A = union (f.:A);
end;

definition
  let f be Function;
  attr f is c=-monotone means
  : Def11:
  for a, b being set st a in dom f & b in dom f & a c= b holds f.a c= f.b;
  attr f is cap-distributive means
  : Def12:
  for a,b being set st dom f
  includes_lattice_of a, b holds f.(a/\b) = f.a /\ f.b;
end;

registration
  cluster d.union-distributive -> c=-monotone for Function;
  coherence
  proof
    let f be Function;
    assume
A1: for A being Subset of dom f st A is c=directed & union A in dom f
    holds f.union A = union (f.:A);
    let a, b be set;
    assume that
A2: a in dom f and
A3: b in dom f and
A4: a c= b;
    reconsider A = {a,b} as Subset of dom f by A2,A3,ZFMISC_1:32;
A5: A is c=directed
    proof
      let Y be finite Subset of A;
      take b;
      union Y c= union A by ZFMISC_1:77;
      then union Y c= a \/ b by ZFMISC_1:75;
      hence thesis by A4,TARSKI:def 2,XBOOLE_1:12;
    end;
    a in A by TARSKI:def 2;
    then
A6: f.a in f.:A by FUNCT_1:def 6;
    union A = a \/ b by ZFMISC_1:75
      .= b by A4,XBOOLE_1:12;
    then union (f.:A) = f.b by A1,A3,A5;
    hence thesis by A6,ZFMISC_1:74;
  end;
  cluster union-distributive -> d.union-distributive for Function;
  coherence
  proof
    let f be Function;
    assume
A7: for A being Subset of dom f st union A in dom f holds f.union A =
    union (f.:A);
    let A be Subset of dom f;
    thus thesis by A7;
  end;
end;

theorem
  for f being Function st f is union-distributive for x,y being set st x
  in dom f & y in dom f & x \/ y in dom f holds f.(x \/ y) = (f.x) \/ (f.y)
proof
  let f be Function such that
A1: f is union-distributive;
  let x,y be set;
  set X = {x,y};
  assume that
A2: x in dom f & y in dom f and
A3: x \/ y in dom f;
A4: union X = x \/ y by ZFMISC_1:75;
  X c= dom f by A2,ZFMISC_1:32;
  hence f.(x \/ y) = union (f.:X) by A1,A3,A4,Def9
    .= union {f.x,f.y} by A2,FUNCT_1:60
    .= (f.x) \/ (f.y) by ZFMISC_1:75;
end;

theorem Th18:
  for f being Function st f is union-distributive holds f.{} = {}
proof
  let f be Function such that
A1: for A being Subset of dom f st union A in dom f holds f.union A =
  union (f.:A);
A2: {} c= dom f & f.:{} = {} by XBOOLE_1:2;
  not {} in dom f implies f.{} = {} by FUNCT_1:def 2;
  hence thesis by A1,A2,ZFMISC_1:2;
end;

registration
  let C1,C2 be Coherence_Space;
  cluster union-distributive cap-distributive for Function of C1, C2;
  existence
  proof
    reconsider a = {} as Element of C2 by COH_SP:1;
    take f = C1 --> a;
A1: dom f = C1 by FUNCOP_1:13;
    thus f is union-distributive
    proof
      let A be Subset of dom f;
      assume union A in dom f;
      then
A2:   f.union A = {} by A1,FUNCOP_1:7;
      f.:A c= {{}}
      proof
        let x be set;
        assume x in f.:A;
        then ex y being set st y in dom f & y in A & x = f.y by FUNCT_1:def 6;
        then x = {} by A1,FUNCOP_1:7;
        hence thesis by TARSKI:def 1;
      end;
      then
A3:   union (f.:A) c= union {{}} by ZFMISC_1:77;
      union {{}} = {} by ZFMISC_1:25;
      hence thesis by A2,A3;
    end;
    let a,b be set;
    assume
A4: dom f includes_lattice_of a, b;
    then a in dom f by Th16;
    then
A5: f.a = {} by A1,FUNCOP_1:7;
    a /\ b in dom f by A4,Th16;
    hence thesis by A1,A5,FUNCOP_1:7;
  end;
end;

registration
  let C be Coherence_Space;
  cluster union-distributive cap-distributive for ManySortedSet of C;
  existence
  proof
    set f = the union-distributive cap-distributive Function of C, C;
    dom f = C by FUNCT_2:52;
    then reconsider f as ManySortedSet of C by PARTFUN1:def 2;
    take f;
    thus thesis;
  end;
end;

::definition
:: cluster union-distributive cap-distributive Function;
::end;

definition
  let f be Function;
  attr f is U-continuous means
  : Def13:
  dom f is d.union-closed & f is d.union-distributive;
end;

definition
  let f be Function;
  attr f is U-stable means
  : Def14:
  dom f is multiplicative & f is U-continuous cap-distributive;
end;

definition
  let f be Function;
  attr f is U-linear means
  : Def15:
  f is U-stable union-distributive;
end;

registration
  cluster U-continuous -> d.union-distributive for Function;
  coherence by Def13;
  cluster U-stable -> cap-distributive U-continuous for Function;
  coherence by Def14;
  cluster U-linear -> union-distributive U-stable for Function;
  coherence by Def15;
end;

registration
  let X be d.union-closed set;
  cluster d.union-distributive -> U-continuous for ManySortedSet of X;
  coherence
  proof
    let f be ManySortedSet of X;
    dom f = X by PARTFUN1:def 2;
    hence thesis by Def13;
  end;
end;

registration
  let X be multiplicative set;
  cluster U-continuous cap-distributive -> U-stable for ManySortedSet of X;
  coherence
  proof
    let f be ManySortedSet of X;
    dom f = X by PARTFUN1:def 2;
    hence thesis by Def14;
  end;
end;

registration
  cluster U-stable union-distributive -> U-linear for Function;
  coherence by Def15;
end;

registration
  cluster U-linear for Function;
  existence
  proof
    set C = the Coherence_Space;
    set f = the union-distributive cap-distributive ManySortedSet of C;
    take f;
    thus thesis;
  end;
  let C be Coherence_Space;
  cluster U-linear for ManySortedSet of C;
  existence
  proof
    set f = the union-distributive cap-distributive ManySortedSet of C;
    take f;
    thus thesis;
  end;
  let B be Coherence_Space;
  cluster U-linear for Function of B,C;
  existence
  proof
    set f = the union-distributive cap-distributive Function of B,C;
    take f;
    dom f = B by FUNCT_2:def 1;
    then reconsider
    f as union-distributive cap-distributive ManySortedSet of B by
PARTFUN1:def 2;
    f is U-linear;
    hence thesis;
  end;
end;

registration
  let f be U-continuous Function;
  cluster dom f -> d.union-closed;
  coherence by Def13;
end;

registration
  let f be U-stable Function;
  cluster dom f -> multiplicative;
  coherence by Def14;
end;

theorem Th19:
  for X being set holds union Fin X = X
proof
  let X be set;
  union Fin X c= union bool X by FINSUB_1:13,ZFMISC_1:77;
  hence union Fin X c= X by ZFMISC_1:81;
  let x be set;
  assume x in X;
  then {x} c= X by ZFMISC_1:31;
  then
A1: {x} in Fin X by FINSUB_1:def 5;
  x in {x} by TARSKI:def 1;
  hence thesis by A1,TARSKI:def 4;
end;

theorem Th20:
  for f being U-continuous Function st dom f is subset-closed for
  a being set st a in dom f holds f.a = union (f.:Fin a)
proof
  let f be U-continuous Function such that
A1: dom f is subset-closed;
  let a be set;
  assume
A2: a in dom f;
  then reconsider
  C = dom f as d.union-closed subset-closed non empty set by A1;
  reconsider a as Element of C by A2;
  f.a = f.union Fin a by Th19;
  hence thesis by Def10;
end;

theorem Th21:
  for f being Function st dom f is subset-closed holds f is
  U-continuous iff dom f is d.union-closed & f is c=-monotone & for a, y being
set st a in dom f & y in f.a ex b being set st b is finite & b c= a & y in f.b
proof
  let f be Function such that
A1: dom f is subset-closed;
  hereby
    assume
A2: f is U-continuous;
    hence dom f is d.union-closed & f is c=-monotone;
    reconsider C = dom f as d.union-closed subset-closed set by A1,A2;
    let a, y be set;
    assume that
A3: a in dom f and
A4: y in f.a;
    reconsider A = {b where b is Subset of a: b is finite} as set;
A5: A is c=directed
    proof
      let Y be finite Subset of A;
      take union Y;
      now
        let x be set;
        assume x in Y;
        then x in A;
        then ex c being Subset of a st x = c & c is finite;
        hence x c= a;
      end;
      then
A6:   union Y c= a by ZFMISC_1:76;
      now
        let b be set;
        assume b in Y;
        then b in A;
        then ex c being Subset of a st b = c & c is finite;
        hence b is finite;
      end;
      then union Y is finite by FINSET_1:7;
      hence thesis by A6;
    end;
A7: union A = a
    proof
      thus union A c= a
      proof
        let x be set;
        assume x in union A;
        then consider b being set such that
A8:     x in b and
A9:     b in A by TARSKI:def 4;
        ex c being Subset of a st b = c & c is finite by A9;
        hence thesis by A8;
      end;
      let x be set;
      assume x in a;
      then {x} c= a by ZFMISC_1:31;
      then x in {x} & {x} in A by TARSKI:def 1;
      hence thesis by TARSKI:def 4;
    end;
A10: A c= C
    proof
      let x be set;
      assume x in A;
      then ex b being Subset of a st x = b & b is finite;
      hence thesis by A3,CLASSES1:def 1;
    end;
    then union A in C by A5,Def6;
    then f.union A = union (f.:A) by A2,A5,A10,Def10;
    then consider B being set such that
A11: y in B and
A12: B in f.:A by A4,A7,TARSKI:def 4;
    consider b being set such that
    b in dom f and
A13: b in A and
A14: B = f.b by A12,FUNCT_1:def 6;
    take b;
    ex c being Subset of a st b = c & c is finite by A13;
    hence b is finite & b c= a & y in f.b by A11,A14;
  end;
  assume dom f is d.union-closed;
  then reconsider C = dom f as d.union-closed set;
  assume that
A15: for a,b being set st a in dom f & b in dom f & a c= b holds f.a c= f.b and
A16: for a, y being set st a in dom f & y in f.a ex b being set st b is
  finite & b c= a & y in f.b;
  C is d.union-closed;
  hence dom f is d.union-closed;
  thus f is d.union-distributive
  proof
    let A be Subset of dom f;
    assume that
A17: A is c=directed and
A18: union A in dom f;
    reconsider A9 = A as Subset of C;
    thus f.union A c= union (f.:A)
    proof
      let x be set;
      assume x in f.union A;
      then consider b being set such that
A19:  b is finite & b c= union A9 and
A20:  x in f.b by A16,A18;
      consider c being set such that
A21:  c in A and
A22:  b c= c by A17,A19,Th13;
      b in C by A1,A21,A22,CLASSES1:def 1;
      then
A23:  f.b c= f.c by A15,A21,A22;
      f.c in f.:A by A21,FUNCT_1:def 6;
      hence thesis by A20,A23,TARSKI:def 4;
    end;
    let x be set;
    assume x in union (f.:A);
    then consider B be set such that
A24: x in B and
A25: B in f.:A by TARSKI:def 4;
    ex b being set st b in dom f & b in A & B = f.b by A25,FUNCT_1:def 6;
    then B c= f.union A9 by A15,A18,ZFMISC_1:74;
    hence thesis by A24;
  end;
end;

theorem Th22:
  for f being Function st dom f is subset-closed d.union-closed
holds f is U-stable iff f is c=-monotone & for a, y being set st a in dom f & y
in f.a ex b being set st b is finite & b c= a & y in f.b & for c being set st c
  c= a & y in f.c holds b c= c
proof
  let f be Function such that
A1: dom f is subset-closed d.union-closed;
  reconsider C = dom f as subset-closed d.union-closed set by A1;
  hereby
    assume f is U-stable;
    then reconsider f9 = f as U-stable Function;
    dom f9 is multiplicative;
    hence f is c=-monotone;
    defpred P[set,set] means $1 c= $2;
    let a, y be set;
    set C = dom f9;
    assume that
A2: a in dom f and
A3: y in f.a;
    consider b being set such that
A4: b is finite and
A5: b c= a and
A6: y in f9.b by A1,A2,A3,Th21;
    b c= b;
    then b in {c where c is Subset of b: y in f.c} by A6;
    then reconsider A = {c where c is Subset of b: y in f.c} as non empty set;
A7: bool b is finite & A c= bool b
    proof
      thus bool b is finite by A4;
      let x be set;
      assume x in A;
      then ex c being Subset of b st x = c & y in f.c;
      hence thesis;
    end;
A8: for x,y,z being set st P[x,y] & P[y,z] holds P[x,z] by XBOOLE_1:1;
A9: for x,y being set st P[x,y] & P[y,x] holds x = y by XBOOLE_0:def 10;
    reconsider A as finite non empty set by A7;
A10: A <> {};
    consider c being set such that
A11: c in A & for y being set st y in A & y <> c holds not P[y,c] from
    CARD_2:sch 1(A10,A9,A8);
    ex d being Subset of b st c = d & y in f.d by A11;
    then reconsider c9 = c as Subset of b;
    reconsider c9 as finite Subset of b by A4;
    take c;
A12: ex d being Subset of b st c = d & y in f.d by A11;
    hence
A13: c is finite & c c= a & y in f.c by A4,A5,XBOOLE_1:1;
    then
A14: c9 in C by A1,A2,CLASSES1:def 1;
    let d be set;
    assume that
A15: d c= a and
A16: y in f.d;
A17: d in C by A1,A2,A15,CLASSES1:def 1;
    c \/ d c= a by A13,A15,XBOOLE_1:8;
    then
A18: c \/ d in dom f by A1,A2,CLASSES1:def 1;
A19: c /\ d c= c9 by XBOOLE_1:17;
    then c /\ d in dom f by A1,A14,CLASSES1:def 1;
    then dom f includes_lattice_of c, d by A14,A17,A18,Th16;
    then f.(c /\ d) = f.c /\ f.d by A14,Def12;
    then
A20: y in f.(c /\ d) by A12,A16,XBOOLE_0:def 4;
    c /\ d is finite Subset of b by A19,XBOOLE_1:1;
    then c /\ d c= d & c /\ d in A by A20,XBOOLE_1:17;
    hence c c= d by A11,XBOOLE_1:17;
  end;
  assume that
A21: f is c=-monotone and
A22: for a, y being set st a in dom f & y in f.a ex b being set st b is
finite & b c= a & y in f.b & for c being set st c c= a & y in f.c holds b c= c;
  C is subset-closed set;
  hence dom f is multiplicative;
  now
    let a, y be set;
    assume a in dom f & y in f.a;
    then ex b being set st b is finite & b c= a & y in f.b & for c being set
    st c c= a & y in f.c holds b c= c by A22;
    hence ex b being set st b is finite & b c= a & y in f.b;
  end;
  hence f is U-continuous by A1,A21,Th21;
  thus f is cap-distributive
  proof
    let a,b be set;
A23: a /\ b c= b by XBOOLE_1:17;
    assume
A24: dom f includes_lattice_of a, b;
    then
A25: a/\b in dom f by Th16;
    b in dom f by A24,Th16;
    then
A26: f.(a /\ b) c= f.b by A21,A25,A23,Def11;
A27: a in dom f by A24,Th16;
    a /\ b c= a by XBOOLE_1:17;
    then f.(a /\ b) c= f.a by A21,A27,A25,Def11;
    hence f.(a /\ b) c= f.a /\ f.b by A26,XBOOLE_1:19;
    let x be set;
    assume
A28: x in f.a /\ f.b;
    then
A29: x in f.a by XBOOLE_0:def 4;
A30: a \/ b in dom f by A24,Th16;
    a c= a \/ b by XBOOLE_1:7;
    then f.a c= f.(a \/ b) by A21,A27,A30,Def11;
    then consider c being set such that
    c is finite and
    c c= a \/ b and
A31: x in f.c and
A32: for d being set st d c= a \/ b & x in f.d holds c c= d by A22,A30,A29;
A33: c c= a by A29,A32,XBOOLE_1:7;
    x in f.b by A28,XBOOLE_0:def 4;
    then c c= b by A32,XBOOLE_1:7;
    then
A34: c c= a/\b by A33,XBOOLE_1:19;
    C = dom f;
    then c in dom f by A27,A33,CLASSES1:def 1;
    then f.c c= f.(a/\b) by A21,A25,A34,Def11;
    hence thesis by A31;
  end;
end;

theorem Th23:
  for f being Function st dom f is subset-closed d.union-closed
holds f is U-linear iff f is c=-monotone & for a, y being set st a in dom f & y
in f.a ex x being set st x in a & y in f.{x} & for b being set st b c= a & y in
  f.b holds x in b
proof
  let f be Function;
  assume
A1: dom f is subset-closed d.union-closed;
  then reconsider C = dom f as subset-closed d.union-closed set;
  hereby
A2: {} is Subset of dom f by XBOOLE_1:2;
    assume
A3: f is U-linear;
    hence f is c=-monotone;
    let a, y be set;
    assume that
A4: a in dom f and
A5: y in f.a;
    consider b being set such that
    b is finite and
A6: b c= a and
A7: y in f.b and
A8: for c being set st c c= a & y in f.c holds b c= c by A1,A3,A4,A5,Th22;
A9: dom f = C;
    {} c= a by XBOOLE_1:2;
    then {} in dom f by A4,A9,CLASSES1:def 1;
    then f.{} = union (f.:{}) by A3,A2,Def9,ZFMISC_1:2
      .= {} by ZFMISC_1:2;
    then reconsider b as non empty set by A7;
    reconsider A = {{x} where x is Element of b: not contradiction} as set;
A10: b in dom f by A4,A6,A9,CLASSES1:def 1;
A11: A c= dom f
    proof
      let X be set;
      assume X in A;
      then ex x being Element of b st X = {x};
      then X c= b by ZFMISC_1:31;
      hence thesis by A9,A10,CLASSES1:def 1;
    end;
    now
      let X be set;
      assume X in A;
      then ex x being Element of b st X = {x};
      hence X c= b by ZFMISC_1:31;
    end;
    then union A c= b by ZFMISC_1:76;
    then
A12: union A in dom f by A9,A10,CLASSES1:def 1;
    reconsider A as Subset of dom f by A11;
    b c= union A
    proof
      let x be set;
      assume x in b;
      then {x} in A;
      then {x} c= union A by ZFMISC_1:74;
      hence thesis by ZFMISC_1:31;
    end;
    then
A13: f.b c= f.union A by A3,A10,A12,Def11;
    f.union A = union (f.:A) by A3,A12,Def9;
    then consider Y being set such that
A14: y in Y and
A15: Y in f.:A by A7,A13,TARSKI:def 4;
    consider X being set such that
    X in dom f and
A16: X in A and
A17: Y = f.X by A15,FUNCT_1:def 6;
    consider x being Element of b such that
A18: X = {x} by A16;
    reconsider x as set;
    take x;
    x in b;
    hence x in a & y in f.{x} by A6,A14,A17,A18;
    let c be set;
    assume c c= a & y in f.c;
    then x in b & b c= c by A8;
    hence x in c;
  end;
  assume that
A19: f is c=-monotone and
A20: for a, y being set st a in dom f & y in f.a ex x being set st x in
  a & y in f.{x} & for b being set st b c= a & y in f.b holds x in b;
  now
    let a, y be set;
    assume a in dom f & y in f.a;
    then consider x being set such that
A21: x in a & y in f.{x} and
A22: for b being set st b c= a & y in f.b holds x in b by A20;
    reconsider b = {x} as set;
    take b;
    thus b is finite & b c= a & y in f.b by A21,ZFMISC_1:31;
    let c be set;
    assume c c= a & y in f.c;
    then x in c by A22;
    hence b c= c by ZFMISC_1:31;
  end;
  hence f is U-stable by A1,A19,Th22;
  thus f is union-distributive
  proof
    let A be Subset of dom f such that
A23: union A in dom f;
    thus f.union A c= union (f.:A)
    proof
      let y be set;
      assume y in f.union A;
      then consider x being set such that
A24:  x in union A and
A25:  y in f.{x} and
      for b being set st b c= union A & y in f.b holds x in b by A20,A23;
      consider a being set such that
A26:  x in a and
A27:  a in A by A24,TARSKI:def 4;
A28:  {x} c= a by A26,ZFMISC_1:31;
      then {x} in C by A27,CLASSES1:def 1;
      then
A29:  f.{x} c= f.a by A19,A27,A28,Def11;
      f.a in f.:A by A27,FUNCT_1:def 6;
      hence thesis by A25,A29,TARSKI:def 4;
    end;
    now
      let X be set;
      assume X in f.:A;
      then consider a being set such that
A30:  a in dom f and
A31:  a in A and
A32:  X = f.a by FUNCT_1:def 6;
      a c= union A by A31,ZFMISC_1:74;
      hence X c= f.union A by A19,A23,A30,A32,Def11;
    end;
    hence thesis by ZFMISC_1:76;
  end;
end;

begin :: Graph of Continuous Function

definition
  let f be Function;
  func graph f -> set means
  : Def16:
  for x being set holds x in it iff ex y
  being finite set, z being set st x = [y,z] & y in dom f & z in f.y;
  existence
  proof
    defpred P[set] means ex y being finite set, z being set st $1 = [y,z] & y
    in dom f & z in f.y;
    consider X being set such that
A1: for x being set holds x in X iff x in [:dom f, union rng f:] & P[x
    ] from XBOOLE_0:sch 1;
    take X;
    let x be set;
    now
      given y being finite set, z being set such that
A2:   x = [y,z] and
A3:   y in dom f and
A4:   z in f.y;
      f.y in rng f by A3,FUNCT_1:def 3;
      then z in union rng f by A4,TARSKI:def 4;
      hence x in [:dom f, union rng f:] by A2,A3,ZFMISC_1:87;
    end;
    hence thesis by A1;
  end;
  uniqueness
  proof
    let X1, X2 be set;
    assume
A5: not thesis;
    then consider x being set such that
A6: not (x in X1 iff x in X2) by TARSKI:1;
    x in X2 iff not ex y being finite set, z being set st x = [y,z] & y
    in dom f & z in f.y by A5,A6;
    hence thesis by A5;
  end;
end;

definition
  let C1,C2 be non empty set;
  let f be Function of C1,C2;
  redefine func graph f -> Subset of [:C1, union C2:];
  coherence
  proof
    graph f c= [:C1, union C2:]
    proof
      let x be set;
      assume x in graph f;
      then consider y being finite set, z being set such that
A1:   x = [y,z] and
A2:   y in dom f and
A3:   z in f.y by Def16;
      rng f c= C2 & f.y in rng f by A2,FUNCT_1:def 3,RELAT_1:def 19;
      then dom f = C1 & z in union C2 by A3,FUNCT_2:def 1,TARSKI:def 4;
      hence thesis by A1,A2,ZFMISC_1:87;
    end;
    hence thesis;
  end;
end;

registration
  let f be Function;
  cluster graph f -> Relation-like;
  coherence
  proof
    let x be set;
    assume x in graph f;
    then
    ex y being finite set, z being set st x = [y,z] & y in dom f & z in f
    .y by Def16;
    hence thesis;
  end;
end;

theorem Th24:
  for f being Function, x,y being set holds [x,y] in graph f iff x
  is finite & x in dom f & y in f.x
proof
  let f be Function, x,y be set;
  now
    given y9 being finite set, z being set such that
A1: [x,y] = [y9,z] and
A2: y9 in dom f & z in f.y9;
    x = y9 by A1,XTUPLE_0:1;
    hence x is finite & x in dom f & y in f.x by A1,A2,XTUPLE_0:1;
  end;
  hence thesis by Def16;
end;

theorem Th25:
  for f being c=-monotone Function for a,b being set st b in dom f
& a c= b & b is finite for y being set st [a,y] in graph f holds [b,y] in graph
  f
proof
  let f be c=-monotone Function;
  let a,b be set such that
A1: b in dom f and
A2: a c= b and
A3: b is finite;
  let y be set;
  assume
A4: [a,y] in graph f;
  then a in dom f by Th24;
  then
A5: f.a c= f.b by A1,A2,Def11;
  y in f.a by A4,Th24;
  hence thesis by A1,A3,A5,Th24;
end;

theorem Th26:
  for C1, C2 being Coherence_Space for f being Function of C1,C2
for a being Element of C1 for y1,y2 being set st [a,y1] in graph f & [a,y2] in
  graph f holds {y1,y2} in C2
proof
  let C1, C2 be Coherence_Space;
  let f be Function of C1,C2;
  let a be Element of C1, y1,y2 be set;
  assume [a,y1] in graph f & [a,y2] in graph f;
  then y1 in f.a & y2 in f.a by Th24;
  then {y1,y2} c= f.a by ZFMISC_1:32;
  hence thesis by CLASSES1:def 1;
end;

theorem
  for C1, C2 being Coherence_Space for f being c=-monotone Function of
C1,C2 for a,b being Element of C1 st a \/ b in C1 for y1,y2 being set st [a,y1]
  in graph f & [b,y2] in graph f holds {y1,y2} in C2
proof
  let C1, C2 be Coherence_Space;
  let f be c=-monotone Function of C1,C2;
  let a,b be Element of C1 such that
A1: a \/ b in C1;
  let y1,y2 be set;
  assume
A2: [a,y1] in graph f & [b,y2] in graph f;
  then a is finite & b is finite by Th24;
  then reconsider c = a \/ b as finite Element of C1 by A1;
  dom f = C1 by FUNCT_2:def 1;
  then [c,y1] in graph f & [c,y2] in graph f by A2,Th25,XBOOLE_1:7;
  hence thesis by Th26;
end;

theorem Th28:
  for C1, C2 being Coherence_Space for f,g being U-continuous
  Function of C1,C2 st graph f = graph g holds f = g
proof
  let C1, C2 be Coherence_Space;
  let f,g be U-continuous Function of C1,C2;
A1: dom f = C1 by FUNCT_2:def 1;
A2: dom g = C1 by FUNCT_2:def 1;
A3: now
    let x be finite Element of C1;
    let f,g be U-continuous Function of C1,C2;
A4: dom f = C1 by FUNCT_2:def 1;
    assume
A5: graph f = graph g;
    thus f.x c= g.x
    proof
      let z be set;
      assume z in f.x;
      then [x,z] in graph f by A4,Th24;
      hence thesis by A5,Th24;
    end;
  end;
A6: now
    let a be Element of C1;
    let f,g be U-continuous Function of C1,C2;
A7: dom g = C1 by FUNCT_2:def 1;
    assume
A8: graph f = graph g;
    thus f.:Fin a c= g.:Fin a
    proof
      let y be set;
      assume y in f.:Fin a;
      then consider x being set such that
      x in dom f and
A9:   x in Fin a and
A10:  y = f.x by FUNCT_1:def 6;
      f.x c= g.x & g.x c= f.x by A3,A8,A9;
      then f.x = g.x by XBOOLE_0:def 10;
      hence thesis by A7,A9,A10,FUNCT_1:def 6;
    end;
  end;
  assume
A11: graph f = graph g;
  now
    let a be Element of C1;
    f.:Fin a c= g.:Fin a & g.:Fin a c= f.:Fin a by A11,A6;
    then
A12: f.:Fin a = g.:Fin a by XBOOLE_0:def 10;
    thus f.a = union (f.:Fin a) by A1,Th20
      .= g.a by A2,A12,Th20;
  end;
  hence thesis by FUNCT_2:63;
end;

Lm4: for C1, C2 being Coherence_Space for X being Subset of [:C1, union C2:]
st (for x being set st x in X holds x`1 is finite) & (for a,b being finite
Element of C1 st a c= b for y being set st [a,y] in X holds [b,y] in X) & (for
a being finite Element of C1 for y1,y2 being set st [a,y1] in X & [a,y2] in X
holds {y1,y2} in C2) ex f being U-continuous Function of C1,C2 st X = graph f &
for a being Element of C1 holds f.a = X.:Fin a
proof
  let C1, C2 be Coherence_Space;
  let X be Subset of [:C1, union C2:] such that
A1: for x being set st x in X holds x`1 is finite and
A2: for a,b being finite Element of C1 st a c= b for y being set st [a,y
  ] in X holds [b,y] in X and
A3: for a being finite Element of C1 for y1,y2 being set st [a,y1] in X
  & [a,y2] in X holds {y1,y2} in C2;
  deffunc f(set) = X.:Fin $1;
  consider f being Function such that
A4: dom f = C1 & for a being set st a in C1 holds f.a = f(a) from
  FUNCT_1:sch 3;
A5: rng f c= C2
  proof
    let x be set;
    assume x in rng f;
    then consider a being set such that
A6: a in dom f and
A7: x = f.a by FUNCT_1:def 3;
    reconsider a as Element of C1 by A4,A6;
A8: x = X.:Fin a by A4,A7;
    now
      let z,y be set;
      assume z in x;
      then consider z1 being set such that
A9:   [z1,z] in X and
A10:  z1 in Fin a by A8,RELAT_1:def 13;
      assume y in x;
      then consider y1 being set such that
A11:  [y1,y] in X and
A12:  y1 in Fin a by A8,RELAT_1:def 13;
      reconsider z1, y1 as finite Element of C1 by A10,A12;
      z1 \/ y1 in Fin a by A10,A12,FINSUB_1:1;
      then reconsider b = z1 \/ y1 as finite Element of C1;
A13:  [b,y] in X by A2,A11,XBOOLE_1:7;
      [b,z] in X by A2,A9,XBOOLE_1:7;
      hence {z,y} in C2 by A3,A13;
    end;
    hence thesis by COH_SP:6;
  end;
A14: now
    let a, y be set;
    assume that
A15: a in dom f and
A16: y in f.a;
    y in X.:Fin a by A4,A15,A16;
    then consider x being set such that
A17: [x,y] in X and
A18: x in Fin a by RELAT_1:def 13;
    x c= a by A18,FINSUB_1:def 5;
    then x in C1 by A4,A15,CLASSES1:def 1;
    then
A19: f.x = X.:Fin x by A4;
    take x;
    x in Fin x by A18,FINSUB_1:def 5;
    hence x is finite & x c= a & y in f.x by A17,A18,A19,FINSUB_1:def 5
,RELAT_1:def 13;
  end;
  f is c=-monotone
  proof
    let a,b be set;
    assume that
A20: a in dom f & b in dom f and
A21: a c= b;
    reconsider a, b as Element of C1 by A4,A20;
    Fin a c= Fin b by A21,FINSUB_1:10;
    then
A22: X.:Fin a c= X.:Fin b by RELAT_1:123;
    f.a = X.:Fin a by A4;
    hence thesis by A4,A22;
  end;
  then reconsider f as U-continuous Function of C1, C2 by A4,A5,A14,Th21,
FUNCT_2:def 1,RELSET_1:4;
  take f;
  thus X = graph f
  proof
    let a,b be set;
    hereby
      assume
A23:  [a,b] in X;
      [a,b]`1 = a;
      then reconsider a9 = a as finite Element of C1 by A1,A23,ZFMISC_1:87;
      a9 in Fin a by FINSUB_1:def 5;
      then
A24:  b in X.:Fin a by A23,RELAT_1:def 13;
      f.a9 = X.:Fin a by A4;
      hence [a,b] in graph f by A4,A24,Th24;
    end;
    assume
A25: [a,b] in graph f;
    then reconsider a as finite Element of C1 by A4,Th24;
A26: f.a = X.:Fin a by A4;
    b in f.a by A25,Th24;
    then consider x being set such that
A27: [x,b] in X and
A28: x in Fin a by A26,RELAT_1:def 13;
    x c= a by A28,FINSUB_1:def 5;
    hence thesis by A2,A27,A28;
  end;
  thus thesis by A4;
end;

theorem
  for C1, C2 being Coherence_Space for X being Subset of [:C1, union C2
  :] st (for x being set st x in X holds x`1 is finite) & (for a,b being finite
Element of C1 st a c= b for y being set st [a,y] in X holds [b,y] in X) & (for
  a being finite Element of C1 for y1,y2 being set st [a,y1] in X & [a,y2] in X
  holds {y1,y2} in C2) ex f being U-continuous Function of C1,C2 st X = graph f
proof
  let C1, C2 be Coherence_Space;
  let X be Subset of [:C1, union C2:];
  assume
A1: not thesis;
  then ex f being U-continuous Function of C1,C2 st X = graph f & for a being
  Element of C1 holds f.a = X.:Fin a by Lm4;
  hence thesis by A1;
end;

theorem
  for C1, C2 being Coherence_Space for f being U-continuous Function of
  C1,C2 for a being Element of C1 holds f.a = (graph f).:Fin a
proof
  let C1, C2 be Coherence_Space;
  let f be U-continuous Function of C1,C2;
  let a be Element of C1;
  set X = graph f;
A1: now
    let x be set;
    assume x in X;
    then
    ex y being finite set, z being set st x = [y,z] & y in dom f & z in f.
    y by Def16;
    hence x`1 is finite by MCART_1:7;
  end;
  dom f = C1 by FUNCT_2:def 1;
  then
A2: for a,b being finite Element of C1 st a c= b for y being set st [a,y] in
  X holds [b,y] in X by Th25;
  for a being finite Element of C1 for y1,y2 being set st [a,y1] in X & [a
  ,y2] in X holds {y1,y2} in C2 by Th26;
  then consider g being U-continuous Function of C1,C2 such that
A3: X = graph g and
A4: for a being Element of C1 holds g.a = X.:Fin a by A1,A2,Lm4;
  g.a = X.:Fin a by A4;
  hence thesis by A3,Th28;
end;

begin :: Trace of Stable Function

definition
  let f be Function;
  func Trace f -> set means
  : Def17:
  for x being set holds x in it iff ex a, y
being set st x = [a,y] & a in dom f & y in f.a & for b being set st b in dom f
  & b c= a & y in f.b holds a = b;
  existence
  proof
    defpred P[set] means ex a, y being set st $1 = [a,y] & a in dom f & y in f
    .a & for b being set st b in dom f & b c= a & y in f.b holds a = b;
    consider T being set such that
A1: for x being set holds x in T iff x in [:dom f, Union f:] & P[x]
    from XBOOLE_0:sch 1;
    take T;
    let x be set;
    now
      given a, y being set such that
A2:   x = [a,y] and
A3:   a in dom f and
A4:   y in f.a and
      for b being set st b in dom f & b c= a & y in f.b holds a = b;
      y in Union f by A3,A4,CARD_5:2;
      hence x in [:dom f, Union f:] by A2,A3,ZFMISC_1:87;
    end;
    hence thesis by A1;
  end;
  uniqueness
  proof
    let T1, T2 be set;
    assume
A5: not thesis;
    then consider x being set such that
A6: not (x in T1 iff x in T2) by TARSKI:1;
    x in T2 iff not ex a, y being set st x = [a,y] & a in dom f & y in f.a
    & for b being set st b in dom f & b c= a & y in f.b holds a = b by A5,A6;
    hence contradiction by A5;
  end;
end;

theorem Th31:
  for f being Function for a, y being set holds [a,y] in Trace f
  iff a in dom f & y in f.a & for b being set st b in dom f & b c= a & y in f.b
  holds a = b
proof
  let f be Function, a9, y9 be set;
  now
    given a, y being set such that
A1: [a9,y9] = [a,y] and
A2: a in dom f & y in f.a & for b being set st b in dom f & b c= a & y
    in f. b holds a = b;
    a9 = a & y9 = y by A1,XTUPLE_0:1;
    hence a9 in dom f & y9 in f.a9 & for b being set st b in dom f & b c= a9 &
    y9 in f.b holds a9 = b by A2;
  end;
  hence thesis by Def17;
end;

definition
  let C1, C2 be non empty set;
  let f be Function of C1, C2;
  redefine func Trace f -> Subset of [:C1, union C2:];
  coherence
  proof
    Trace f c= [:C1, union C2:]
    proof
      let x be set;
      assume x in Trace f;
      then consider a, y being set such that
A1:   x = [a,y] and
A2:   a in dom f and
A3:   y in f.a and
      for b being set st b in dom f & b c= a & y in f.b holds a = b by Def17;
      rng f c= C2 & f.a in rng f by A2,FUNCT_1:def 3,RELAT_1:def 19;
      then dom f = C1 & y in union C2 by A3,FUNCT_2:def 1,TARSKI:def 4;
      hence thesis by A1,A2,ZFMISC_1:87;
    end;
    hence thesis;
  end;
end;

registration
  let f be Function;
  cluster Trace f -> Relation-like;
  coherence
  proof
    let x be set;
    assume x in Trace f;
    then ex a, y being set st x = [a,y] & a in dom f & y in f.a & for b being
    set st b in dom f & b c= a & y in f.b holds a = b by Def17;
    hence thesis;
  end;
end;

theorem
  for f being U-continuous Function st dom f is subset-closed holds
  Trace f c= graph f
proof
  let f be U-continuous Function such that
A1: dom f is subset-closed;
  let x,z be set;
  assume [x,z] in Trace f;
  then consider a, y being set such that
A2: [x,z] = [a,y] and
A3: a in dom f and
A4: y in f.a and
A5: for b being set st b in dom f & b c= a & y in f.b holds a = b by Def17;
  consider b being set such that
A6: b is finite and
A7: b c= a and
A8: y in f.b by A1,A3,A4,Th21;
  b in dom f by A1,A3,A7,CLASSES1:def 1;
  then a = b by A5,A7,A8;
  hence thesis by A2,A3,A4,A6,Th24;
end;

theorem Th33:
  for f being U-continuous Function st dom f is subset-closed for
  a, y being set st [a,y] in Trace f holds a is finite
proof
  let f be U-continuous Function such that
A1: dom f is subset-closed;
  let a, y be set;
  assume
A2: [a,y] in Trace f;
  then
A3: a in dom f by Th31;
  y in f.a by A2,Th31;
  then consider b be set such that
A4: b is finite and
A5: b c= a and
A6: y in f.b by A1,A3,Th21;
  b in dom f by A1,A3,A5,CLASSES1:def 1;
  hence thesis by A2,A4,A5,A6,Th31;
end;

theorem Th34:
  for C1, C2 being Coherence_Space for f being c=-monotone
Function of C1,C2 for a1,a2 being set st a1 \/ a2 in C1 for y1,y2 being set st
  [a1,y1] in Trace f & [a2,y2] in Trace f holds {y1,y2} in C2
proof
  let C1, C2 be Coherence_Space;
  let f be c=-monotone Function of C1,C2;
A1: dom f = C1 by FUNCT_2:def 1;
  let a1,a2 be set;
  set a = a1 \/ a2;
  assume a in C1;
  then reconsider a as Element of C1;
A2: a2 c= a by XBOOLE_1:7;
  then a2 in C1 by CLASSES1:def 1;
  then
A3: f.a2 c= f.a by A1,A2,Def11;
  let y1,y2 be set;
  assume [a1,y1] in Trace f & [a2,y2] in Trace f;
  then
A4: y1 in f.a1 & y2 in f.a2 by Th31;
A5: a1 c= a by XBOOLE_1:7;
  then a1 in C1 by CLASSES1:def 1;
  then f.a1 c= f.a by A1,A5,Def11;
  then {y1,y2} c= f.a by A3,A4,ZFMISC_1:32;
  hence thesis by CLASSES1:def 1;
end;

theorem Th35:
  for C1, C2 being Coherence_Space for f being cap-distributive
Function of C1,C2 for a1,a2 being set st a1 \/ a2 in C1 for y being set st [a1,
  y] in Trace f & [a2,y] in Trace f holds a1 = a2
proof
  let C1, C2 be Coherence_Space;
  let f be cap-distributive Function of C1,C2;
A1: dom f = C1 by FUNCT_2:def 1;
  let a1,a2 be set;
  set a = a1 \/ a2;
  assume
A2: a in C1;
  a2 c= a by XBOOLE_1:7;
  then
A3: a2 in C1 by A2,CLASSES1:def 1;
  a1 c= a by XBOOLE_1:7;
  then
A4: a1 in C1 by A2,CLASSES1:def 1;
  then reconsider b = a1 /\ a2 as Element of C1 by A3,FINSUB_1:def 2;
  b in C1;
  then
A5: C1 includes_lattice_of a1,a2 by A2,A4,A3,Th16;
  let y be set;
  assume that
A6: [a1,y] in Trace f and
A7: [a2,y] in Trace f;
  y in f.a1 & y in f.a2 by A6,A7,Th31;
  then y in (f.a1) /\ (f.a2) by XBOOLE_0:def 4;
  then
A8: y in f.b by A1,A5,Def12;
  b c= a1 by XBOOLE_1:17;
  then b c= a2 & b = a1 by A1,A6,A8,Th31,XBOOLE_1:17;
  hence thesis by A1,A7,A8,Th31;
end;

theorem Th36:
  for C1, C2 being Coherence_Space for f,g being U-stable Function
  of C1,C2 st Trace f c= Trace g for a being Element of C1 holds f.a c= g.a
proof
  let C1, C2 be Coherence_Space;
  let f,g be U-stable Function of C1,C2;
  assume
A1: Trace f c= Trace g;
  let x be Element of C1;
A2: dom f = C1 by FUNCT_2:def 1;
  let z be set;
  assume z in f.x;
  then consider b being set such that
  b is finite and
A3: b c= x and
A4: z in f.b and
A5: for c being set st c c= x & z in f.c holds b c= c by A2,Th22;
  reconsider b as Element of C1 by A3,CLASSES1:def 1;
  now
    let c be set;
    assume that
    c in dom f and
A6: c c= b and
A7: z in f.c;
    c c= x by A3,A6,XBOOLE_1:1;
    then b c= c by A5,A7;
    hence b = c by A6,XBOOLE_0:def 10;
  end;
  then [b,z] in Trace f by A2,A4,Th31;
  then
A8: z in g.b by A1,Th31;
  dom g = C1 by FUNCT_2:def 1;
  then g.b c= g.x by A3,Def11;
  hence thesis by A8;
end;

theorem Th37:
  for C1, C2 being Coherence_Space for f,g being U-stable Function
  of C1,C2 st Trace f = Trace g holds f = g
proof
  let C1, C2 be Coherence_Space;
  let f,g be U-stable Function of C1,C2;
A1: dom f = C1 by FUNCT_2:def 1;
A2: dom g = C1 by FUNCT_2:def 1;
A3: now
    let a be Element of C1;
    let f,g be U-stable Function of C1,C2;
A4: dom g = C1 by FUNCT_2:def 1;
    assume
A5: Trace f = Trace g;
    thus f.:Fin a c= g.:Fin a
    proof
      let y be set;
      assume y in f.:Fin a;
      then consider x being set such that
      x in dom f and
A6:   x in Fin a and
A7:   y = f.x by FUNCT_1:def 6;
      f.x c= g.x & g.x c= f.x by A5,A6,Th36;
      then f.x = g.x by XBOOLE_0:def 10;
      hence thesis by A4,A6,A7,FUNCT_1:def 6;
    end;
  end;
  assume
A8: Trace f = Trace g;
  now
    let a be Element of C1;
    f.:Fin a c= g.:Fin a & g.:Fin a c= f.:Fin a by A8,A3;
    then
A9: f.:Fin a = g.:Fin a by XBOOLE_0:def 10;
    thus f.a = union (f.:Fin a) by A1,Th20
      .= g.a by A2,A9,Th20;
  end;
  hence thesis by FUNCT_2:63;
end;

Lm5: for C1, C2 being Coherence_Space for X being Subset of [:C1, union C2:]
st (for x being set st x in X holds x`1 is finite) & (for a,b being Element of
C1 st a \/ b in C1 for y1,y2 being set st [a,y1] in X & [b,y2] in X holds {y1,
y2} in C2) & (for a,b being Element of C1 st a \/ b in C1 for y being set st [a
,y] in X & [b,y] in X holds a = b) ex f being U-stable Function of C1,C2 st X =
Trace f & for a being Element of C1 holds f.a = X.:Fin a
proof
  let C1, C2 be Coherence_Space;
  let X be Subset of [:C1, union C2:] such that
A1: for x being set st x in X holds x`1 is finite and
A2: for a,b being Element of C1 st a \/ b in C1 for y1,y2 being set st [
  a,y1] in X & [b,y2] in X holds {y1,y2} in C2 and
A3: for a,b being Element of C1 st a \/ b in C1 for y being set st [a,y]
  in X & [b,y] in X holds a = b;
  deffunc f(set) = X.:Fin $1;
  consider f being Function such that
A4: dom f = C1 & for a being set st a in C1 holds f.a = f(a) from
  FUNCT_1:sch 3;
A5: now
    let a, y be set;
    assume that
A6: a in dom f and
A7: y in f.a;
    reconsider a9 = a as Element of C1 by A4,A6;
    y in X.:Fin a by A4,A6,A7;
    then consider x being set such that
A8: [x,y] in X and
A9: x in Fin a by RELAT_1:def 13;
    x c= a by A9,FINSUB_1:def 5;
    then x in C1 by A4,A6,CLASSES1:def 1;
    then
A10: f.x = X.:Fin x by A4;
    take x;
    x in Fin x by A9,FINSUB_1:def 5;
    hence x is finite & x c= a & y in f.x by A8,A9,A10,FINSUB_1:def 5
,RELAT_1:def 13;
    let c be set;
    assume that
A11: c c= a and
A12: y in f.c;
    c c= a9 by A11;
    then c in dom f by A4,CLASSES1:def 1;
    then y in X.:Fin c by A4,A12;
    then consider z being set such that
A13: [z,y] in X and
A14: z in Fin c by RELAT_1:def 13;
A15: Fin c c= Fin a by A11,FINSUB_1:10;
    then
A16: z in Fin a9 by A14;
    x \/ z in Fin a9 by A9,A14,A15,FINSUB_1:1;
    then x = z by A3,A8,A9,A13,A16;
    hence x c= c by A14,FINSUB_1:def 5;
  end;
A17: rng f c= C2
  proof
    let x be set;
    assume x in rng f;
    then consider a being set such that
A18: a in dom f and
A19: x = f.a by FUNCT_1:def 3;
    reconsider a as Element of C1 by A4,A18;
A20: x = X.:Fin a by A4,A19;
    now
      let z,y be set;
      assume z in x;
      then consider z1 being set such that
A21:  [z1,z] in X and
A22:  z1 in Fin a by A20,RELAT_1:def 13;
      assume y in x;
      then consider y1 being set such that
A23:  [y1,y] in X and
A24:  y1 in Fin a by A20,RELAT_1:def 13;
      z1 \/ y1 in Fin a by A22,A24,FINSUB_1:1;
      hence {z,y} in C2 by A2,A21,A22,A23,A24;
    end;
    hence thesis by COH_SP:6;
  end;
  f is c=-monotone
  proof
    let a,b be set;
    assume that
A25: a in dom f & b in dom f and
A26: a c= b;
    reconsider a, b as Element of C1 by A4,A25;
    Fin a c= Fin b by A26,FINSUB_1:10;
    then
A27: X.:Fin a c= X.:Fin b by RELAT_1:123;
    f.a = X.:Fin a by A4;
    hence thesis by A4,A27;
  end;
  then reconsider f as U-stable Function of C1, C2 by A4,A17,A5,Th22,
FUNCT_2:def 1,RELSET_1:4;
  take f;
  thus X = Trace f
  proof
    let a,b be set;
    hereby
      assume
A28:  [a,b] in X;
      [a,b]`1 = a;
      then reconsider a9 = a as finite Element of C1 by A1,A28,ZFMISC_1:87;
      a9 in Fin a by FINSUB_1:def 5;
      then
A29:  b in X.:Fin a by A28,RELAT_1:def 13;
A30:  now
        let c be set;
        assume that
A31:    c in dom f and
A32:    c c= a9 and
A33:    b in f.c;
        reconsider c9 = c as Element of C1 by A4,A31;
        b in X.:Fin c9 by A4,A33;
        then consider x being set such that
A34:    [x,b] in X and
A35:    x in Fin c9 by RELAT_1:def 13;
A36:    x c= c by A35,FINSUB_1:def 5;
        then x \/ a9 = a9 by A32,XBOOLE_1:1,12;
        then x = a by A3,A28,A34,A35;
        hence a9 = c by A32,A36,XBOOLE_0:def 10;
      end;
      f.a9 = X.:Fin a by A4;
      hence [a,b] in Trace f by A4,A29,A30,Th31;
    end;
    assume
A37: [a,b] in Trace f;
    then a in dom f & b in f.a by Th31;
    then b in X.:Fin a by A4;
    then consider x being set such that
A38: [x,b] in X and
A39: x in Fin a by RELAT_1:def 13;
    reconsider a as Element of C1 by A4,A37,Th31;
    x in Fin a by A39;
    then reconsider x as finite Element of C1;
    x in Fin x by FINSUB_1:def 5;
    then b in X.:Fin x by A38,RELAT_1:def 13;
    then
A40: b in f.x by A4;
    x c= a by A39,FINSUB_1:def 5;
    hence thesis by A4,A37,A38,A40,Th31;
  end;
  thus thesis by A4;
end;

theorem Th38:
  for C1, C2 being Coherence_Space for X being Subset of [:C1,
union C2:] st (for x being set st x in X holds x`1 is finite) & (for a,b being
Element of C1 st a \/ b in C1 for y1,y2 being set st [a,y1] in X & [b,y2] in X
holds {y1,y2} in C2) & (for a,b being Element of C1 st a \/ b in C1 for y being
set st [a,y] in X & [b,y] in X holds a = b) ex f being U-stable Function of C1,
  C2 st X = Trace f
proof
  let C1, C2 be Coherence_Space;
  let X be Subset of [:C1, union C2:];
  assume
A1: not thesis;
  then ex f being U-stable Function of C1,C2 st X = Trace f & for a being
  Element of C1 holds f.a = X.:Fin a by Lm5;
  hence thesis by A1;
end;

theorem
  for C1, C2 being Coherence_Space for f being U-stable Function of C1,
  C2 for a being Element of C1 holds f.a = (Trace f).:Fin a
proof
  let C1, C2 be Coherence_Space;
  let f be U-stable Function of C1,C2;
  let a be Element of C1;
  set X = Trace f;
A1: dom f = C1 by FUNCT_2:def 1;
A2: now
    let x be set;
    assume
A3: x in X;
    then consider a, y being set such that
A4: x = [a,y] and
    a in dom f and
    y in f.a and
    for b being set st b in dom f & b c= a & y in f.b holds a = b by Def17;
    a is finite by A1,A3,A4,Th33;
    hence x`1 is finite by A4,MCART_1:7;
  end;
  ( for a,b being Element of C1 st a \/ b in C1 for y1,y2 being set st [a,
  y1] in X & [b,y2] in X holds {y1,y2} in C2)& for a,b being Element of C1 st a
\/ b in C1 for y being set st [a,y] in X & [b,y] in X holds a = b by Th34,Th35;
  then consider g being U-stable Function of C1,C2 such that
A5: X = Trace g and
A6: for a being Element of C1 holds g.a = X.:Fin a by A2,Lm5;
  g.a = X.:Fin a by A6;
  hence thesis by A5,Th37;
end;

theorem Th40:
  for C1,C2 being Coherence_Space, f being U-stable Function of C1
  ,C2 for a being Element of C1, y being set holds y in f.a iff ex b being
  Element of C1 st [b,y] in Trace f & b c= a
proof
  let C1,C2 be Coherence_Space, f be U-stable Function of C1,C2;
  let a be Element of C1, y be set;
A1: dom f = C1 by FUNCT_2:def 1;
  hereby
    assume y in f.a;
    then consider b being set such that
    b is finite and
A2: b c= a and
A3: y in f.b and
A4: for c being set st c c= a & y in f.c holds b c= c by A1,Th22;
    reconsider b as Element of C1 by A2,CLASSES1:def 1;
    take b;
    now
      let c be set;
      assume that
      c in dom f and
A5:   c c= b and
A6:   y in f.c;
      c c= a by A2,A5,XBOOLE_1:1;
      then b c= c by A4,A6;
      hence b = c by A5,XBOOLE_0:def 10;
    end;
    hence [b,y] in Trace f by A1,A3,Th31;
    thus b c= a by A2;
  end;
  given b being Element of C1 such that
A7: [b,y] in Trace f and
A8: b c= a;
A9: y in f.b by A7,Th31;
  f.b c= f.a by A1,A8,Def11;
  hence thesis by A9;
end;

theorem
  for C1, C2 being Coherence_Space ex f being U-stable Function of C1,
  C2 st Trace f = {}
proof
  let C1, C2 be Coherence_Space;
  reconsider X = {} as Subset of [:C1, union C2:] by XBOOLE_1:2;
A1: for a,b being Element of C1 st a \/ b in C1 for y being set st [a,y] in
  X & [b,y] in X holds a = b;
  ( for x being set st x in X holds x`1 is finite)& for a,b being Element
of C1 st a \/ b in C1 for y1,y2 being set st [a, y1] in X & [b,y2] in X holds {
  y1,y2} in C2;
  hence thesis by A1,Th38;
end;

theorem Th42:
  for C1, C2 being Coherence_Space for a being finite Element of
  C1, y being set st y in union C2 ex f being U-stable Function of C1, C2 st
  Trace f = {[a,y]}
proof
  let C1, C2 be Coherence_Space;
  let a be finite Element of C1, y be set;
  assume
A1: y in union C2;
  then [a,y] in [:C1, union C2:] by ZFMISC_1:87;
  then reconsider X = {[a,y]} as Subset of [:C1, union C2:] by ZFMISC_1:31;
A2: now
    let a1,b be Element of C1;
    assume a1 \/ b in C1;
    let y1,y2 be set;
    assume that
A3: [a1,y1] in X and
A4: [b,y2] in X;
    [b,y2] = [a,y] by A4,TARSKI:def 1;
    then
A5: y2 = y by XTUPLE_0:1;
    [a1,y1] = [a,y] by A3,TARSKI:def 1;
    then y1 = y by XTUPLE_0:1;
    then {y1,y2} = {y} by A5,ENUMSET1:29;
    hence {y1,y2} in C2 by A1,COH_SP:4;
  end;
A6: now
    let a1,b be Element of C1;
    assume a1 \/ b in C1;
    let y1 be set;
    assume [a1,y1] in X & [b,y1] in X;
    then [a1,y1] = [a,y] & [b,y1] = [a,y] by TARSKI:def 1;
    hence a1 = b by XTUPLE_0:1;
  end;
  now
    let x be set;
    assume x in X;
    then x = [a,y] by TARSKI:def 1;
    hence x`1 is finite by MCART_1:7;
  end;
  hence thesis by A2,A6,Th38;
end;

theorem
  for C1, C2 being Coherence_Space for a being Element of C1, y being
  set for f being U-stable Function of C1, C2 st Trace f = {[a,y]} for b being
Element of C1 holds (a c= b implies f.b = {y}) & (not a c= b implies f.b = {})
proof
  let C1, C2 be Coherence_Space;
  let a be Element of C1, y be set;
  let f be U-stable Function of C1, C2;
  assume
A1: Trace f = {[a,y]};
  let b be Element of C1;
A2: [a,y] in Trace f by A1,TARSKI:def 1;
  hereby
A3: f.b c= {y}
    proof
      let x be set;
      assume x in f.b;
      then consider c being Element of C1 such that
A4:   [c,x] in Trace f and
      c c= b by Th40;
      [c,x] = [a,y] by A1,A4,TARSKI:def 1;
      then x = y by XTUPLE_0:1;
      hence thesis by TARSKI:def 1;
    end;
    assume a c= b;
    then y in f.b by A2,Th40;
    then {y} c= f.b by ZFMISC_1:31;
    hence f.b = {y} by A3,XBOOLE_0:def 10;
  end;
  assume that
A5: not a c= b and
A6: f.b <> {};
  reconsider B = f.b as non empty set by A6;
  set z = the Element of B;
  consider c being Element of C1 such that
A7: [c,z] in Trace f and
A8: c c= b by Th40;
  [c,z] = [a,y] by A1,A7,TARSKI:def 1;
  hence thesis by A5,A8,XTUPLE_0:1;
end;

theorem Th44:
  for C1, C2 being Coherence_Space for f being U-stable Function
  of C1,C2 for X being Subset of Trace f ex g being U-stable Function of C1, C2
  st Trace g = X
proof
  let C1, C2 be Coherence_Space;
  let f be U-stable Function of C1,C2;
  let X be Subset of Trace f;
A1: for a,b be Element of C1 st a \/ b in C1 for y be set st [a,y] in X & [b
  ,y] in X holds a = b by Th35;
A2: now
    let x be set;
    assume
A3: x in X;
    then consider a, y being set such that
A4: x = [a,y] and
    a in dom f and
    y in f.a and
    for b being set st b in dom f & b c= a & y in f.b holds a = b by Def17;
    dom f = C1 by FUNCT_2:def 1;
    then a is finite by A3,A4,Th33;
    hence x`1 is finite by A4,MCART_1:7;
  end;
  X is Subset of [:C1, union C2:] & for a,b be Element of C1 st a \/ b in
  C1 for y1,y2 be set st [a,y1] in X & [b,y2] in X holds {y1,y2} in C2 by Th34,
XBOOLE_1:1;
  hence thesis by A2,A1,Th38;
end;

theorem Th45:
  for C1, C2 being Coherence_Space for A being set st for x,y
being set st x in A & y in A ex f being U-stable Function of C1,C2 st x \/ y =
  Trace f ex f being U-stable Function of C1,C2 st union A = Trace f
proof
  let C1, C2 be Coherence_Space;
  let A be set such that
A1: for x,y being set st x in A & y in A ex f being U-stable Function of
  C1,C2 st x \/ y = Trace f;
  set X = union A;
A2: now
    let a,b be Element of C1 such that
A3: a \/ b in C1;
    let y1,y2 be set;
    assume [a,y1] in X;
    then consider x1 being set such that
A4: [a,y1] in x1 and
A5: x1 in A by TARSKI:def 4;
    assume [b,y2] in X;
    then consider x2 being set such that
A6: [b,y2] in x2 and
A7: x2 in A by TARSKI:def 4;
A8: x1 c= x1 \/ x2 & x2 c= x1 \/ x2 by XBOOLE_1:7;
    ex f being U-stable Function of C1,C2 st x1 \/ x2 = Trace f by A1,A5,A7;
    hence {y1,y2} in C2 by A3,A4,A6,A8,Th34;
  end;
A9: now
    let a,b be Element of C1 such that
A10: a \/ b in C1;
    let y be set;
    assume [a,y] in X;
    then consider x1 being set such that
A11: [a,y] in x1 and
A12: x1 in A by TARSKI:def 4;
    assume [b,y] in X;
    then consider x2 being set such that
A13: [b,y] in x2 and
A14: x2 in A by TARSKI:def 4;
A15: x1 c= x1 \/ x2 & x2 c= x1 \/ x2 by XBOOLE_1:7;
    ex f being U-stable Function of C1,C2 st x1 \/ x2 = Trace f by A1,A12,A14;
    hence a = b by A10,A11,A13,A15,Th35;
  end;
A16: now
    let x be set;
    assume x in X;
    then consider y being set such that
A17: x in y and
A18: y in A by TARSKI:def 4;
    y \/ y = y;
    then consider f being U-stable Function of C1,C2 such that
A19: y = Trace f by A1,A18;
    consider a, y being set such that
A20: x = [a,y] and
    a in dom f and
    y in f.a and
    for b being set st b in dom f & b c= a & y in f.b holds a = b by A17,A19
,Def17;
    dom f = C1 by FUNCT_2:def 1;
    then a is finite by A17,A19,A20,Th33;
    hence x`1 is finite by A20,MCART_1:7;
  end;
  X c= [:C1, union C2:]
  proof
    let x be set;
    assume x in X;
    then consider y being set such that
A21: x in y and
A22: y in A by TARSKI:def 4;
    y \/ y = y;
    then ex f being U-stable Function of C1,C2 st y = Trace f by A1,A22;
    hence thesis by A21;
  end;
  hence thesis by A16,A2,A9,Th38;
end;

definition
  let C1, C2 be Coherence_Space;
  func StabCoh(C1,C2) -> set means
  : Def18:
  for x being set holds x in it iff
  ex f being U-stable Function of C1,C2 st x = Trace f;
  uniqueness
  proof
    let X1, X2 be set;
    assume
A1: not thesis;
    then consider x being set such that
A2: not (x in X1 iff x in X2) by TARSKI:1;
    x in X2 iff not ex f being U-stable Function of C1,C2 st x = Trace f
    by A1,A2;
    hence thesis by A1;
  end;
  existence
  proof
    defpred P[set] means ex f being U-stable Function of C1,C2 st $1 = Trace f;
    consider X being set such that
A3: for x being set holds x in X iff x in bool [:C1, union C2:] & P[x]
    from XBOOLE_0:sch 1;
    take X;
    let x be set;
    thus thesis by A3;
  end;
end;

registration
  let C1, C2 be Coherence_Space;
  cluster StabCoh(C1,C2) -> non empty subset-closed binary_complete;
  coherence
  proof
    set C = StabCoh(C1,C2);
    set f = the U-stable Function of C1,C2;
    Trace f in C by Def18;
    hence C is non empty;
    thus C is subset-closed
    proof
      let a,b be set;
      assume a in C;
      then
A1:   ex f being U-stable Function of C1,C2 st a = Trace f by Def18;
      assume b c= a;
      then ex g being U-stable Function of C1, C2 st Trace g = b by A1,Th44;
      hence thesis by Def18;
    end;
    let A be set;
    assume
A2: for a,b being set st a in A & b in A holds a \/ b in C;
    now
      let x,y be set;
      assume x in A & y in A;
      then x \/ y in C by A2;
      hence ex f being U-stable Function of C1,C2 st x \/ y = Trace f by Def18;
    end;
    then ex f being U-stable Function of C1,C2 st union A = Trace f by Th45;
    hence thesis by Def18;
  end;
end;

theorem Th46:
  for C1,C2 being Coherence_Space, f being U-stable Function of C1
  ,C2 holds Trace f c= [:Sub_of_Fin C1, union C2:]
proof
  let C1,C2 be Coherence_Space, f be U-stable Function of C1,C2;
  let x1,x2 be set;
  assume
A1: [x1,x2] in Trace f;
  then consider a, y being set such that
A2: [x1,x2] = [a,y] and
A3: a in dom f and
A4: y in f.a and
  for b being set st b in dom f & b c= a & y in f.b holds a = b by Def17;
A5: dom f = C1 by FUNCT_2:def 1;
  then a is finite by A1,A2,Th33;
  then
A6: a in Sub_of_Fin C1 by A3,A5,Def3;
  y in union C2 by A3,A4,A5,Lm1;
  hence thesis by A2,A6,ZFMISC_1:87;
end;

theorem
  for C1,C2 being Coherence_Space holds union StabCoh(C1,C2) = [:
  Sub_of_Fin C1, union C2:]
proof
  let C1,C2 be Coherence_Space;
  thus union StabCoh(C1,C2) c= [:Sub_of_Fin C1, union C2:]
  proof
    let x be set;
    assume x in union StabCoh(C1,C2);
    then consider a being set such that
A1: x in a and
A2: a in StabCoh(C1,C2) by TARSKI:def 4;
    ex f being U-stable Function of C1,C2 st a = Trace f by A2,Def18;
    then a c= [:Sub_of_Fin C1, union C2:] by Th46;
    hence thesis by A1;
  end;
  let x,y be set;
  assume
A3: [x,y] in [:Sub_of_Fin C1, union C2:];
  then
A4:  y in union C2 by ZFMISC_1:87;
A5: x in Sub_of_Fin C1 by A3,ZFMISC_1:87;
  then x is finite by Def3;
  then ex f being U-stable Function of C1,C2 st Trace f = {[x,y]} by A5,A4,Th42
;
  then [x,y] in {[x,y]} & {[x,y]} in StabCoh(C1,C2) by Def18,TARSKI:def 1;
  hence thesis by TARSKI:def 4;
end;

theorem Th48:
  for C1,C2 being Coherence_Space for a,b being finite Element of
C1, y1,y2 being set holds [[a,y1],[b,y2]] in Web StabCoh(C1,C2) iff not a \/ b
in C1 & y1 in union C2 & y2 in union C2 or [y1,y2] in Web C2 & (y1 = y2 implies
  a = b)
proof
  let C1,C2 be Coherence_Space;
  let a,b be finite Element of C1, y1,y2 be set;
  hereby
    assume [[a,y1],[b,y2]] in Web StabCoh(C1,C2);
    then {[a,y1],[b,y2]} in StabCoh(C1,C2) by COH_SP:5;
    then
A1: ex f being U-stable Function of C1,C2 st {[a,y1],[b,y2]} = Trace f by Def18
;
A2: [a,y1] in {[a,y1],[b,y2]} & [b,y2] in {[a,y1],[b,y2]} by TARSKI:def 2;
    assume
A3: a \/ b in C1 or not y1 in union C2 or not y2 in union C2;
    then {y1,y2} in C2 by A1,A2,Th34,ZFMISC_1:87;
    hence [y1,y2] in Web C2 by COH_SP:5;
    thus y1 = y2 implies a = b by A1,A2,A3,Th35,ZFMISC_1:87;
  end;
  assume
A4: not a \/ b in C1 & y1 in union C2 & y2 in union C2 or [y1,y2] in Web
  C2 & (y1 = y2 implies a = b);
  then
A5: y2 in union C2 by ZFMISC_1:87;
  then
A6: [b,y2] in [:C1, union C2:] by ZFMISC_1:87;
A7: y1 in union C2 by A4,ZFMISC_1:87;
  then [a,y1] in [:C1, union C2:] by ZFMISC_1:87;
  then reconsider X = {[a,y1],[b,y2]} as Subset of [:C1, union C2:] by A6,
ZFMISC_1:32;
A8: now
    let a1,b1 be Element of C1;
    assume
A9: a1 \/ b1 in C1;
    let z1,z2 be set;
    assume that
A10: [a1,z1] in X and
A11: [b1,z2] in X;
    [b1,z2] = [a,y1] or [b1,z2] = [b,y2] by A11,TARSKI:def 2;
    then
A12: z2 = y1 & b1 = a or b1 = b & z2 = y2 by XTUPLE_0:1;
    [a1,z1] = [a,y1] or [a1,z1] = [b,y2] by A10,TARSKI:def 2;
    then z1 = y1 & a1 = a or a1 = b & z1 = y2 by XTUPLE_0:1;
    then {z1,z2} = {y1} or {z1,z2} in C2 or {z1,z2} = {y2} by A4,A9,A12,
COH_SP:5,ENUMSET1:29;
    hence {z1,z2} in C2 by A7,A5,COH_SP:4;
  end;
A13: now
    let a1,b1 be Element of C1;
    assume
A14: a1 \/ b1 in C1;
    let y be set;
    assume that
A15: [a1,y] in X and
A16: [b1,y] in X;
    [a1,y] = [a,y1] or [a1,y] = [b,y2] by A15,TARSKI:def 2;
    then
A17: a1 = a & y = y1 or a1 = b & y = y2 by XTUPLE_0:1;
    [b1,y] = [a,y1] or [b1,y] = [b,y2] by A16,TARSKI:def 2;
    hence a1 = b1 by A4,A14,A17,XTUPLE_0:1;
  end;
  now
    let x be set;
    assume x in X;
    then x = [a,y1] or x = [b,y2] by TARSKI:def 2;
    hence x`1 is finite by MCART_1:7;
  end;
  then ex f being U-stable Function of C1,C2 st X = Trace f by A8,A13,Th38;
  then X in StabCoh(C1,C2) by Def18;
  hence thesis by COH_SP:5;
end;

begin :: Trace of Linear Functions

theorem Th49:
  for C1, C2 being Coherence_Space for f being U-stable Function
  of C1,C2 holds f is U-linear iff for a,y being set st [a,y] in Trace f ex x
  being set st a = {x}
proof
  let C1, C2 be Coherence_Space;
  let f be U-stable Function of C1,C2;
A1: dom f = C1 by FUNCT_2:def 1;
  hereby
    assume
A2: f is U-linear;
    let a,y be set;
    assume
A3: [a,y] in Trace f;
    then
A4: a in dom f by Th31;
    y in f.a by A3,Th31;
    then consider x being set such that
A5: x in a and
A6: y in f.{x} and
    for b being set st b c= a & y in f.b holds x in b by A1,A2,A4,Th23;
A7: {x} c= a by A5,ZFMISC_1:31;
    take x;
A8: {x,x} = {x} by ENUMSET1:29;
    {x,x} in C1 by A1,A4,A5,COH_SP:6;
    hence a = {x} by A1,A3,A6,A7,A8,Th31;
  end;
  assume
A9: for a,y being set st [a,y] in Trace f ex x being set st a = {x};
  now
    let a, y be set;
    assume that
A10: a in dom f and
A11: y in f.a;
    consider b being set such that
    b is finite and
A12: b c= a and
A13: y in f.b and
A14: for c being set st c c= a & y in f.c holds b c= c by A1,A10,A11,Th22;
    now
      thus b in dom f by A1,A10,A12,CLASSES1:def 1;
      let c be set;
      assume that
      c in dom f and
A15:  c c= b and
A16:  y in f.c;
      c c= a by A12,A15,XBOOLE_1:1;
      then b c= c by A14,A16;
      hence b = c by A15,XBOOLE_0:def 10;
    end;
    then [b,y] in Trace f by A13,Th31;
    then consider x being set such that
A17: b = {x} by A9;
    take x;
    x in b by A17,TARSKI:def 1;
    hence x in a & y in f.{x} by A12,A13,A17;
    let c be set;
    assume c c= a & y in f.c;
    then b c= c by A14;
    hence x in c by A17,ZFMISC_1:31;
  end;
  hence thesis by A1,Th23;
end;

definition
  let f be Function;
  func LinTrace f -> set means
  : Def19:
  for x being set holds x in it iff ex y
  ,z being set st x = [y,z] & [{y},z] in Trace f;
  uniqueness
  proof
    let X1, X2 be set;
    assume
A1: not thesis;
    then consider x being set such that
A2: not (x in X1 iff x in X2) by TARSKI:1;
    x in X2 iff not ex y,z being set st x = [y,z] & [{y},z] in Trace f by A1,A2
;
    hence thesis by A1;
  end;
  existence
  proof
    defpred P[set] means ex y,z being set st $1 = [y,z] & [{y},z] in Trace f;
    set C1 = dom f, C2 = rng f;
    consider X being set such that
A3: for x being set holds x in X iff x in [:union C1, union C2:] & P[x
    ] from XBOOLE_0:sch 1;
    take X;
    let x be set;
    now
      given y,z being set such that
A4:   x = [y,z] and
A5:   [{y},z] in Trace f;
A6:   {y} in C1 by A5,Th31;
      then
A7:   f.{y} in C2 by FUNCT_1:def 3;
      z in f.{y} by A5,Th31;
      then
A8:   z in union C2 by A7,TARSKI:def 4;
      y in {y} by TARSKI:def 1;
      then y in union C1 by A6,TARSKI:def 4;
      hence x in [:union C1, union C2:] by A4,A8,ZFMISC_1:87;
    end;
    hence thesis by A3;
  end;
end;

theorem Th50:
  for f being Function, x,y being set holds [x,y] in LinTrace f
  iff [{x},y] in Trace f
proof
  let f be Function, x,y be set;
  now
    given v,z being set such that
A1: [x,y] = [v,z] and
A2: [{v},z] in Trace f;
    x = v by A1,XTUPLE_0:1;
    hence [{x},y] in Trace f by A1,A2,XTUPLE_0:1;
  end;
  hence thesis by Def19;
end;

theorem Th51:
  for f being Function st f.{} = {} for x,y being set st {x} in
  dom f & y in f.{x} holds [x,y] in LinTrace f
proof
  let f be Function;
  assume
A1: f.{} = {};
  let x,y be set;
  set a = {x};
  [x,y] in LinTrace f iff [{x},y] in Trace f by Th50;
  then
  [x,y] in LinTrace f iff {x} in dom f & y in f.{x} & for b being set st b
  in dom f & b c= a & y in f.b holds a = b by Th31;
  hence thesis by A1,ZFMISC_1:33;
end;

theorem Th52:
  for f being Function, x,y being set st [x,y] in LinTrace f holds
  {x} in dom f & y in f.{x}
proof
  let f be Function, x,y be set;
  assume [x,y] in LinTrace f;
  then [{x},y] in Trace f by Th50;
  hence thesis by Th31;
end;

definition
  let C1, C2 be non empty set;
  let f be Function of C1, C2;
  redefine func LinTrace f -> Subset of [:union C1, union C2:];
  coherence
  proof
    LinTrace f c= [:union C1, union C2:]
    proof
      let x be set;
      assume x in LinTrace f;
      then consider y,z being set such that
A1:   x = [y,z] and
A2:   [{y},z] in Trace f by Def19;
A3:   y in {y} by TARSKI:def 1;
      dom f = C1 by FUNCT_2:def 1;
      then {y} in C1 by A2,Th31;
      then
A4:   y in union C1 by A3,TARSKI:def 4;
      z in union C2 by A2,ZFMISC_1:87;
      hence thesis by A1,A4,ZFMISC_1:87;
    end;
    hence thesis;
  end;
end;

registration
  let f be Function;
  cluster LinTrace f -> Relation-like;
  coherence
  proof
    let x be set;
    assume x in LinTrace f;
    then ex y,z being set st x = [y,z] & [{y},z] in Trace f by Def19;
    hence thesis;
  end;
end;

definition
  let C1, C2 be Coherence_Space;
  func LinCoh(C1,C2) -> set means
  : Def20:
  for x being set holds x in it iff
  ex f being U-linear Function of C1,C2 st x = LinTrace f;
  uniqueness
  proof
    let X1, X2 be set;
    assume
A1: not thesis;
    then consider x being set such that
A2: not (x in X1 iff x in X2) by TARSKI:1;
    x in X2 iff not ex f being U-linear Function of C1,C2 st x = LinTrace
    f by A1,A2;
    hence thesis by A1;
  end;
  existence
  proof
    defpred P[set] means ex f being U-linear Function of C1,C2 st $1 =
    LinTrace f;
    consider X being set such that
A3: for x being set holds x in X iff x in bool [:union C1, union C2:]
    & P[x] from XBOOLE_0:sch 1;
    take X;
    let x be set;
    thus thesis by A3;
  end;
end;

theorem Th53:
  for C1, C2 being Coherence_Space for f being c=-monotone
Function of C1,C2 for x1,x2 being set st {x1,x2} in C1 for y1,y2 being set st [
  x1,y1] in LinTrace f & [x2,y2] in LinTrace f holds {y1,y2} in C2
proof
  let C1, C2 be Coherence_Space;
  let f be c=-monotone Function of C1,C2;
A1: dom f = C1 by FUNCT_2:def 1;
  let a1,a2 be set;
  assume {a1,a2} in C1;
  then reconsider a = {a1,a2} as Element of C1;
A2: {a2} c= a by ZFMISC_1:7;
  then {a2} in C1 by CLASSES1:def 1;
  then
A3: f.{a2} c= f.a by A1,A2,Def11;
  let y1,y2 be set;
  assume [a1,y1] in LinTrace f & [a2,y2] in LinTrace f;
  then
A4: y1 in f.{a1} & y2 in f.{a2} by Th52;
A5: {a1} c= a by ZFMISC_1:7;
  then {a1} in C1 by CLASSES1:def 1;
  then f.{a1} c= f.a by A1,A5,Def11;
  then {y1,y2} c= f.a by A3,A4,ZFMISC_1:32;
  hence thesis by CLASSES1:def 1;
end;

theorem Th54:
  for C1, C2 being Coherence_Space for f being cap-distributive
Function of C1,C2 for x1,x2 being set st {x1,x2} in C1 for y being set st [x1,y
  ] in LinTrace f & [x2,y] in LinTrace f holds x1 = x2
proof
  let C1, C2 be Coherence_Space;
  let f be cap-distributive Function of C1,C2;
  let a1,a2 be set;
  set a = {a1,a2};
  assume
A1: a in C1;
  let y be set;
A2: a = {a1} \/ {a2} by ENUMSET1:1;
  assume [a1,y] in LinTrace f & [a2,y] in LinTrace f;
  then [{a1},y] in Trace f & [{a2},y] in Trace f by Th50;
  then {a1} = {a2} by A1,A2,Th35;
  hence thesis by ZFMISC_1:3;
end;

theorem Th55:
  for C1, C2 being Coherence_Space for f,g being U-linear Function
  of C1,C2 st LinTrace f = LinTrace g holds f = g
proof
  let C1, C2 be Coherence_Space;
  let f,g be U-linear Function of C1,C2;
  assume
A1: LinTrace f = LinTrace g;
  Trace f = Trace g
  proof
    let a,y be set;
    hereby
      assume
A2:   [a,y] in Trace f;
      then consider x being set such that
A3:   a = {x} by Th49;
      [x,y] in LinTrace f by A2,A3,Th50;
      hence [a,y] in Trace g by A1,A3,Th50;
    end;
    assume
A4: [a,y] in Trace g;
    then consider x being set such that
A5: a = {x} by Th49;
    [x,y] in LinTrace g by A4,A5,Th50;
    hence thesis by A1,A5,Th50;
  end;
  hence thesis by Th37;
end;

Lm6: for C1, C2 being Coherence_Space for X being Subset of [:union C1, union
C2:] st (for a,b being set st {a,b} in C1 for y1,y2 being set st [a,y1] in X &
[b,y2] in X holds {y1,y2} in C2) & (for a,b being set st {a,b} in C1 for y
being set st [a,y] in X & [b,y] in X holds a = b) ex f being U-linear Function
of C1,C2 st X = LinTrace f & for a being Element of C1 holds f.a = X.:a
proof
  let C1, C2 be Coherence_Space;
  let X be Subset of [:union C1, union C2:] such that
A1: for a,b being set st {a,b} in C1 for y1,y2 being set st [a,y1] in X
  & [b,y2] in X holds {y1,y2} in C2 and
A2: for a,b being set st {a,b} in C1 for y being set st [a,y] in X & [b,
  y] in X holds a = b;
  deffunc f(set) = X.:$1;
  consider f being Function such that
A3: dom f = C1 & for a being set st a in C1 holds f.a = f(a) from
  FUNCT_1:sch 3;
A4: now
    let a, y be set;
    assume that
A5: a in dom f and
A6: y in f.a;
    reconsider a9 = a as Element of C1 by A3,A5;
    y in X.:a by A3,A5,A6;
    then consider x being set such that
A7: [x,y] in X and
A8: x in a by RELAT_1:def 13;
    take x;
    {x} c= a by A8,ZFMISC_1:31;
    then {x} in C1 by A3,A5,CLASSES1:def 1;
    then x in {x} & f.{x} = X.:{x} by A3,TARSKI:def 1;
    hence x in a & y in f.{x} by A7,A8,RELAT_1:def 13;
    let c be set;
    assume that
A9: c c= a and
A10: y in f.c;
    c c= a9 by A9;
    then c in dom f by A3,CLASSES1:def 1;
    then y in X.:c by A3,A10;
    then consider z being set such that
A11: [z,y] in X and
A12: z in c by RELAT_1:def 13;
    {x,z} c= a9 by A8,A9,A12,ZFMISC_1:32;
    then {x,z} in C1 by CLASSES1:def 1;
    hence x in c by A2,A7,A11,A12;
  end;
A13: rng f c= C2
  proof
    let x be set;
    assume x in rng f;
    then consider a being set such that
A14: a in dom f and
A15: x = f.a by FUNCT_1:def 3;
    reconsider a as Element of C1 by A3,A14;
A16: x = X.:a by A3,A15;
    now
      let z,y be set;
      assume z in x;
      then consider z1 being set such that
A17:  [z1,z] in X and
A18:  z1 in a by A16,RELAT_1:def 13;
      assume y in x;
      then consider y1 being set such that
A19:  [y1,y] in X and
A20:  y1 in a by A16,RELAT_1:def 13;
      {z1,y1} in C1 by A18,A20,COH_SP:6;
      hence {z,y} in C2 by A1,A17,A19;
    end;
    hence thesis by COH_SP:6;
  end;
  f is c=-monotone
  proof
    let a,b be set;
    assume that
A21: a in dom f & b in dom f and
A22: a c= b;
    reconsider a, b as Element of C1 by A3,A21;
A23: f.a = X.:a by A3;
    X.:a c= X.:b by A22,RELAT_1:123;
    hence thesis by A3,A23;
  end;
  then reconsider f as U-linear Function of C1, C2 by A3,A13,A4,Th23,
FUNCT_2:def 1,RELSET_1:4;
  take f;
  thus X = LinTrace f
  proof
    let a,b be set;
    hereby
      assume
A24:  [a,b] in X;
      then a in union C1 by ZFMISC_1:87;
      then consider a9 being set such that
A25:  a in a9 and
A26:  a9 in C1 by TARSKI:def 4;
      {a} c= a9 by A25,ZFMISC_1:31;
      then reconsider aa = {a} as Element of C1 by A26,CLASSES1:def 1;
A27:  f.aa = X.:aa & f.{} = {} by A3,Th18;
      a in {a} by TARSKI:def 1;
      then b in X.:aa by A24,RELAT_1:def 13;
      hence [a,b] in LinTrace f by A3,A27,Th51;
    end;
    assume
A28: [a,b] in LinTrace f;
    then b in f.{a} by Th52;
    then b in X.:{a} by A3,A28,Th52;
    then ex x being set st [x,b] in X & x in {a} by RELAT_1:def 13;
    hence thesis by TARSKI:def 1;
  end;
  thus thesis by A3;
end;

theorem Th56:
  for C1, C2 being Coherence_Space for X being Subset of [:union
C1, union C2:] st (for a,b being set st {a,b} in C1 for y1,y2 being set st [a,
y1] in X & [b,y2] in X holds {y1,y2} in C2) & (for a,b being set st {a,b} in C1
  for y being set st [a,y] in X & [b,y] in X holds a = b) ex f being U-linear
  Function of C1,C2 st X = LinTrace f
proof
  let C1, C2 be Coherence_Space;
  let X be Subset of [:union C1, union C2:];
  assume
A1: not thesis;
  then ex f being U-linear Function of C1,C2 st X = LinTrace f & for a being
  Element of C1 holds f.a = X.:a by Lm6;
  hence thesis by A1;
end;

theorem
  for C1, C2 being Coherence_Space for f being U-linear Function of C1,
  C2 for a being Element of C1 holds f.a = (LinTrace f).:a
proof
  let C1, C2 be Coherence_Space;
  let f be U-linear Function of C1,C2;
  let a be Element of C1;
  set X = LinTrace f;
  ( for a,b being set st {a,b} in C1 for y1,y2 being set st [a,y1] in X &
[b,y2] in X holds {y1,y2} in C2)& for a,b being set st {a,b} in C1 for y being
  set st [a,y] in X & [b,y] in X holds a = b by Th53,Th54;
  then consider g being U-linear Function of C1,C2 such that
A1: X = LinTrace g and
A2: for a being Element of C1 holds g.a = X.:a by Lm6;
  g.a = X.:a by A2;
  hence thesis by A1,Th55;
end;

theorem
  for C1, C2 being Coherence_Space ex f being U-linear Function of C1,
  C2 st LinTrace f = {}
proof
  let C1, C2 be Coherence_Space;
  reconsider X = {} as Subset of [:union C1, union C2:] by XBOOLE_1:2;
  ( for a,b being set st {a,b} in C1 for y1,y2 being set st [a,y1] in X &
[ b,y2] in X holds {y1,y2} in C2)& for a,b being set st {a,b} in C1 for y being
  set st [a,y] in X & [b,y] in X holds a = b;
  hence thesis by Th56;
end;

theorem Th59:
  for C1, C2 being Coherence_Space for x being set, y being set st
  x in union C1 & y in union C2 ex f being U-linear Function of C1, C2 st
  LinTrace f = {[x,y]}
proof
  let C1, C2 be Coherence_Space;
  let a, y be set;
  assume that
A1: a in union C1 and
A2: y in union C2;
  [a,y] in [:union C1, union C2:] by A1,A2,ZFMISC_1:87;
  then reconsider X = {[a,y]} as Subset of [:union C1, union C2:] by
ZFMISC_1:31;
A3: now
    let a1,b be set;
    assume {a1,b} in C1;
    let y1,y2 be set;
    assume that
A4: [a1,y1] in X and
A5: [b,y2] in X;
    [b,y2] = [a,y] by A5,TARSKI:def 1;
    then
A6: y2 = y by XTUPLE_0:1;
    [a1,y1] = [a,y] by A4,TARSKI:def 1;
    then y1 = y by XTUPLE_0:1;
    then {y1,y2} = {y} by A6,ENUMSET1:29;
    hence {y1,y2} in C2 by A2,COH_SP:4;
  end;
  now
    let a1,b be set;
    assume {a1,b} in C1;
    let y1 be set;
    assume [a1,y1] in X & [b,y1] in X;
    then [a1,y1] = [a,y] & [b,y1] = [a,y] by TARSKI:def 1;
    hence a1 = b by XTUPLE_0:1;
  end;
  hence thesis by A3,Th56;
end;

theorem
  for C1, C2 being Coherence_Space for x being set, y being set st x in
union C1 for f being U-linear Function of C1, C2 st LinTrace f = {[x,y]} for a
being Element of C1 holds (x in a implies f.a = {y}) & (not x in a implies f.a
  = {})
proof
  let C1, C2 be Coherence_Space;
  let a, y be set;
  assume a in union C1;
  then reconsider a9 = {a} as Element of C1 by COH_SP:4;
  let f be U-linear Function of C1, C2;
  assume
A1: LinTrace f = {[a,y]};
  let b be Element of C1;
  [a,y] in LinTrace f by A1,TARSKI:def 1;
  then
A2: y in f.{a} by Th52;
  hereby
A3: f.b c= {y}
    proof
      let x be set;
      assume x in f.b;
      then consider c being Element of C1 such that
A4:   [c,x] in Trace f and
      c c= b by Th40;
      consider d being set such that
A5:   c = {d} by A4,Th49;
      [d,x] in LinTrace f by A4,A5,Th50;
      then [d,x] = [a,y] by A1,TARSKI:def 1;
      then x = y by XTUPLE_0:1;
      hence thesis by TARSKI:def 1;
    end;
    assume a in b;
    then
A6: a9 c= b by ZFMISC_1:31;
    dom f = C1 by FUNCT_2:def 1;
    then f.a9 c= f.b by A6,Def11;
    then {y} c= f.b by A2,ZFMISC_1:31;
    hence f.b = {y} by A3,XBOOLE_0:def 10;
  end;
  assume that
A7: not a in b and
A8: f.b <> {};
  reconsider B = f.b as non empty set by A8;
  set z = the Element of B;
  consider c being Element of C1 such that
A9: [c,z] in Trace f and
A10: c c= b by Th40;
  consider d being set such that
A11: c = {d} by A9,Th49;
  d in c by A11,TARSKI:def 1;
  then
A12: d in b by A10;
  [d,z] in LinTrace f by A9,A11,Th50;
  then [d,z] = [a,y] by A1,TARSKI:def 1;
  hence thesis by A7,A12,XTUPLE_0:1;
end;

theorem Th61:
  for C1, C2 being Coherence_Space for f being U-linear Function
  of C1,C2 for X being Subset of LinTrace f ex g being U-linear Function of C1,
  C2 st LinTrace g = X
proof
  let C1, C2 be Coherence_Space;
  let f be U-linear Function of C1,C2;
  let X be Subset of LinTrace f;
A1: for a,b be set st {a,b} in C1 for y be set st [a,y] in X & [b,y] in X
  holds a = b by Th54;
  X is Subset of [:union C1, union C2:] & for a,b be set st {a,b} in C1
  for y1,y2 be set st [a,y1] in X & [b,y2] in X holds {y1,y2} in C2 by Th53,
XBOOLE_1:1;
  hence thesis by A1,Th56;
end;

theorem Th62:
  for C1, C2 being Coherence_Space for A being set st for x,y
being set st x in A & y in A ex f being U-linear Function of C1,C2 st x \/ y =
  LinTrace f ex f being U-linear Function of C1,C2 st union A = LinTrace f
proof
  let C1, C2 be Coherence_Space;
  let A be set such that
A1: for x,y being set st x in A & y in A ex f being U-linear Function of
  C1,C2 st x \/ y = LinTrace f;
  set X = union A;
A2: now
    let a,b be set such that
A3: {a,b} in C1;
    let y1,y2 be set;
    assume [a,y1] in X;
    then consider x1 being set such that
A4: [a,y1] in x1 and
A5: x1 in A by TARSKI:def 4;
    assume [b,y2] in X;
    then consider x2 being set such that
A6: [b,y2] in x2 and
A7: x2 in A by TARSKI:def 4;
A8: x1 c= x1 \/ x2 & x2 c= x1 \/ x2 by XBOOLE_1:7;
    ex f being U-linear Function of C1,C2 st x1 \/ x2 = LinTrace f by A1,A5,A7;
    hence {y1,y2} in C2 by A3,A4,A6,A8,Th53;
  end;
A9: now
    let a,b be set such that
A10: {a,b} in C1;
    let y be set;
    assume [a,y] in X;
    then consider x1 being set such that
A11: [a,y] in x1 and
A12: x1 in A by TARSKI:def 4;
    assume [b,y] in X;
    then consider x2 being set such that
A13: [b,y] in x2 and
A14: x2 in A by TARSKI:def 4;
A15: x1 c= x1 \/ x2 & x2 c= x1 \/ x2 by XBOOLE_1:7;
    ex f being U-linear Function of C1,C2 st x1 \/ x2 = LinTrace f by A1,A12
,A14;
    hence a = b by A10,A11,A13,A15,Th54;
  end;
  X c= [:union C1, union C2:]
  proof
    let x be set;
    assume x in X;
    then consider y being set such that
A16: x in y and
A17: y in A by TARSKI:def 4;
    y \/ y = y;
    then ex f being U-linear Function of C1,C2 st y = LinTrace f by A1,A17;
    hence thesis by A16;
  end;
  hence thesis by A2,A9,Th56;
end;

registration
  let C1, C2 be Coherence_Space;
  cluster LinCoh(C1,C2) -> non empty subset-closed binary_complete;
  coherence
  proof
    set C = LinCoh(C1,C2);
    set f = the U-linear Function of C1,C2;
    LinTrace f in C by Def20;
    hence C is non empty;
    thus C is subset-closed
    proof
      let a,b be set;
      assume a in C;
      then
A1:   ex f being U-linear Function of C1,C2 st a = LinTrace f by Def20;
      assume b c= a;
      then ex g being U-linear Function of C1, C2 st LinTrace g = b by A1,Th61;
      hence thesis by Def20;
    end;
    let A be set;
    assume
A2: for a,b being set st a in A & b in A holds a \/ b in C;
    now
      let x,y be set;
      assume x in A & y in A;
      then x \/ y in C by A2;
      hence ex f being U-linear Function of C1,C2 st x \/ y = LinTrace f by
Def20;
    end;
    then ex f being U-linear Function of C1,C2 st union A = LinTrace f by Th62;
    hence thesis by Def20;
  end;
end;

theorem
  for C1,C2 being Coherence_Space holds union LinCoh(C1,C2) = [:union C1
  , union C2:]
proof
  let C1,C2 be Coherence_Space;
  thus union LinCoh(C1,C2) c= [:union C1, union C2:]
  proof
    let x be set;
    assume x in union LinCoh(C1,C2);
    then consider a being set such that
A1: x in a and
A2: a in LinCoh(C1,C2) by TARSKI:def 4;
    ex f being U-linear Function of C1,C2 st a = LinTrace f by A2,Def20;
    hence thesis by A1;
  end;
  let x,y be set;
  assume
A3: [x,y] in [:union C1, union C2:];
  then
A4: y in union C2 by ZFMISC_1:87;
  x in union C1 by A3,ZFMISC_1:87;
  then ex f being U-linear Function of C1,C2 st LinTrace f = {[x,y]} by A4,Th59
;
  then [x,y] in {[x,y]} & {[x,y]} in LinCoh(C1,C2) by Def20,TARSKI:def 1;
  hence thesis by TARSKI:def 4;
end;

theorem
  for C1,C2 being Coherence_Space for x1,x2 being set, y1,y2 being set
  holds [[x1,y1],[x2,y2]] in Web LinCoh(C1,C2) iff x1 in union C1 & x2 in union
C1 & (not [x1,x2] in Web C1 & y1 in union C2 & y2 in union C2 or [y1,y2] in Web
  C2 & (y1 = y2 implies x1 = x2))
proof
  let C1,C2 be Coherence_Space;
  let x1,x2,y1,y2 be set;
  hereby
    assume [[x1,y1],[x2,y2]] in Web LinCoh(C1,C2);
    then {[x1,y1],[x2,y2]} in LinCoh(C1,C2) by COH_SP:5;
    then consider f being U-linear Function of C1,C2 such that
A1: {[x1,y1],[x2,y2]} = LinTrace f by Def20;
    [x1,y1] in LinTrace f by A1,TARSKI:def 2;
    then
A2: [{x1},y1] in Trace f by Th50;
    then
A3: {x1} in dom f by Th31;
    [x2,y2] in LinTrace f by A1,TARSKI:def 2;
    then
A4: [{x2},y2] in Trace f by Th50;
    then
A5: {x2} in dom f by Th31;
A6: x1 in {x1} & x2 in { x2} by TARSKI:def 1;
A7: Trace f in StabCoh(C1,C2) by Def18;
A8: dom f = C1 by FUNCT_2:def 1;
    {[{x1},y1],[{x2},y2]} c= Trace f by A2,A4,ZFMISC_1:32;
    then {[{x1},y1],[{x2},y2]} in StabCoh(C1,C2) by A7,CLASSES1:def 1;
    then [[{x1},y1],[{x2},y2]] in Web StabCoh(C1,C2) by COH_SP:5;
    then not {x1}\/{x2} in C1 & y1 in union C2 & y2 in union C2 or [y1,y2] in
    Web C2 & (y1 = y2 implies {x1} = {x2}) by A3,A5,A8,Th48;
    then
    not {x1,x2} in C1 & y1 in union C2 & y2 in union C2 or [y1,y2] in Web
    C2 & (y1 = y2 implies x1 = x2) by ENUMSET1:1,ZFMISC_1:3;
    hence x1 in union C1 & x2 in union C1 & (not [x1,x2] in Web C1 & y1 in
union C2 & y2 in union C2 or [y1,y2] in Web C2 & (y1 = y2 implies x1 = x2)) by
A3,A5,A8,A6,COH_SP:5,TARSKI:def 4;
  end;
  assume x1 in union C1 & x2 in union C1;
  then reconsider a = {x1}, b = {x2} as Element of C1 by COH_SP:4;
  assume not [x1,x2] in Web C1 & y1 in union C2 & y2 in union C2 or [y1,y2]
  in Web C2 & (y1 = y2 implies x1 = x2);
  then not {x1,x2} in C1 & y1 in union C2 & y2 in union C2 or [y1,y2] in Web
  C2 & (y1 = y2 implies a = b) by COH_SP:5;
  then
  not a \/ b in C1 & y1 in union C2 & y2 in union C2 or [y1,y2] in Web C2
  & (y1 = y2 implies a = b) by ENUMSET1:1;
  then [[a,y1],[b,y2]] in Web StabCoh(C1,C2) by Th48;
  then {[a,y1],[b,y2]} in StabCoh(C1,C2) by COH_SP:5;
  then consider f being U-stable Function of C1,C2 such that
A9: {[a,y1],[b,y2]} = Trace f by Def18;
  now
    let a1,y be set;
    assume [a1,y] in Trace f;
    then [a1,y] = [a,y1] or [a1,y] = [b,y2] by A9,TARSKI:def 2;
    then a1 = {x1} or a1 = {x2} by XTUPLE_0:1;
    hence ex x being set st a1 = {x};
  end;
  then f is U-linear by Th49;
  then
A10: LinTrace f in LinCoh(C1,C2) by Def20;
  {[x1,y1],[x2,y2]} c= LinTrace f
  proof
    let x,y be set;
    assume [x,y] in {[x1,y1],[x2,y2]};
    then
    [x,y] = [x1,y1] & [a,y1] in Trace f
     or [x,y] = [x2,y2] & [b,y2] in Trace f by A9,TARSKI:def 2;
    hence thesis by Th50;
  end;
  then {[x1,y1],[x2,y2]} in LinCoh(C1,C2) by A10,CLASSES1:def 1;
  hence thesis by COH_SP:5;
end;

begin :: Negation of Coherence Spaces

definition
  let C be Coherence_Space;
  func 'not' C -> set equals
  {a where a is Subset of union C: for b being
  Element of C ex x being set st a /\ b c= {x}};
  correctness;
end;

theorem Th65:
  for C being Coherence_Space, x being set holds x in 'not' C iff
  x c= union C & for a being Element of C ex z being set st x /\ a c= {z}
proof
  let C be Coherence_Space, x be set;
  x in 'not' C iff ex X being Subset of union C st x = X & for a being
  Element of C ex z being set st X /\ a c= {z};
  hence thesis;
end;

registration
  let C be Coherence_Space;
  cluster 'not' C -> non empty subset-closed binary_complete;
  coherence
  proof
    reconsider a = {} as Subset of union C by XBOOLE_1:2;
    now
      let b be Element of C;
      take x={};
      thus a /\ b c= {x} by XBOOLE_1:2;
    end;
    then a in 'not' C;
    hence 'not' C is non empty;
    hereby
      let a, b be set;
      assume a in 'not' C;
      then consider aa being Subset of union C such that
A1:   a = aa and
A2:   for b being Element of C ex x being set st aa /\ b c= {x};
      assume
A3:   b c= a;
      then reconsider bb = b as Subset of union C by A1,XBOOLE_1:1;
      now
        let c be Element of C;
        consider x being set such that
A4:     aa /\ c c= {x} by A2;
        take x;
        b /\ c c= a /\ c by A3,XBOOLE_1:26;
        hence bb /\ c c= {x} by A1,A4,XBOOLE_1:1;
      end;
      hence b in 'not' C;
    end;
    let A be set such that
A5: for a,b being set st a in A & b in A holds a \/ b in 'not' C;
    A c= bool union C
    proof
      let x be set;
      assume x in A;
      then x \/ x in 'not' C by A5;
      then
      ex a being Subset of union C st x = a & for b being Element of C ex
      x being set st a /\ b c= {x};
      hence thesis;
    end;
    then union A c= union bool union C by ZFMISC_1:77;
    then reconsider a = union A as Subset of union C by ZFMISC_1:81;
    now
      let c be Element of C;
      per cases;
      suppose
A6:     a /\ c = {};
        take x={};
        thus a /\ c c= {x} by A6,XBOOLE_1:2;
      end;
      suppose
        a /\ c <> {};
        then reconsider X = a /\ c as non empty set;
        set x = the Element of X;
        reconsider y = x as set;
        take y;
        thus a /\ c c= {y}
        proof
          let z be set;
          assume
A7:       z in a /\ c;
          then
A8:       z in c by XBOOLE_0:def 4;
          x in a by XBOOLE_0:def 4;
          then consider w being set such that
A9:       x in w and
A10:      w in A by TARSKI:def 4;
          z in a by A7,XBOOLE_0:def 4;
          then consider v being set such that
A11:      z in v and
A12:      v in A by TARSKI:def 4;
          w \/ v in 'not' C by A5,A12,A10;
          then consider aa being Subset of union C such that
A13:      w \/ v = aa and
A14:      for b being Element of C ex x being set st aa /\ b c= {x};
          consider t being set such that
A15:      aa /\ c c= {t} by A14;
          x in c & x in aa by A9,A13,XBOOLE_0:def 3,def 4;
          then
A16:      x in aa /\ c by XBOOLE_0:def 4;
          z in aa by A11,A13,XBOOLE_0:def 3;
          then z in aa /\ c by A8,XBOOLE_0:def 4;
          then z in {t} by A15;
          hence thesis by A15,A16,TARSKI:def 1;
        end;
      end;
    end;
    hence thesis;
  end;
end;

theorem Th66:
  for C being Coherence_Space holds union 'not' C = union C
proof
  let C be Coherence_Space;
  hereby
    let x be set;
    assume x in union 'not' C;
    then consider a being set such that
A1: x in a and
A2: a in 'not' C by TARSKI:def 4;
    a c= union C by A2,Th65;
    hence x in union C by A1;
  end;
  let x be set;
  assume x in union C;
  then
A3: {x} c= union C by ZFMISC_1:31;
  for a being Element of C ex z being set st {x} /\ a c= {z} by XBOOLE_1:17;
  then x in {x} & {x} in 'not' C by A3,ZFMISC_1:31;
  hence thesis by TARSKI:def 4;
end;

theorem Th67:
  for C being Coherence_Space, x,y being set st x <> y & {x,y} in
  C holds not {x,y} in 'not' C
proof
  let C be Coherence_Space, x,y be set;
  assume that
A1: x <> y and
A2: {x,y} in C & {x,y} in 'not' C;
  consider z being set such that
A3: {x,y} /\ {x,y} c= {z} by A2,Th65;
  x = z by A3,ZFMISC_1:20;
  hence contradiction by A1,A3,ZFMISC_1:20;
end;

theorem Th68:
  for C being Coherence_Space, x,y being set st {x,y} c= union C &
  not {x,y} in C holds {x,y} in 'not' C
proof
  let C be Coherence_Space, x,y be set;
  assume that
A1: {x,y} c= union C and
A2: not {x,y} in C;
  now
    let a be Element of C;
    x in a or not x in a;
    then consider z being set such that
A3: x in a & z = x or not x in a & z = y;
    take z;
    thus {x,y} /\ a c= {z}
    proof
      let v be set;
      assume
A4:   v in {x,y} /\ a;
      then
A5:   v in {x,y} by XBOOLE_0:def 4;
A6:   v in a by A4,XBOOLE_0:def 4;
      per cases by A5,TARSKI:def 2;
      suppose
        v = x;
        hence thesis by A3,A4,TARSKI:def 1,XBOOLE_0:def 4;
      end;
      suppose
A7:     v = y;
        then x in a implies {x,y} c= a by A6,ZFMISC_1:32;
        hence thesis by A2,A3,A7,CLASSES1:def 1,TARSKI:def 1;
      end;
    end;
  end;
  hence thesis by A1;
end;

theorem
  for C being Coherence_Space for x,y being set holds [x,y] in Web 'not'
  C iff x in union C & y in union C & (x = y or not [x,y] in Web C)
proof
  let C be Coherence_Space, x,y be set;
A1: {x,y} c= union C & not {x,y} in C implies {x,y} in 'not' C by Th68;
A2: union 'not' C = union C by Th66;
  x <> y & {x,y} in C implies not {x,y} in 'not' C by Th67;
  hence [x,y] in Web 'not' C implies x in union C & y in union C & (x = y or
  not [x,y] in Web C) by A2,COH_SP:5,ZFMISC_1:87;
  assume that
A3: x in union C and
A4: y in union C and
A5: x = y or not [x,y] in Web C;
  x = y & {x} in 'not' C & {x} = {x,y} or not {x,y} in C by A2,A3,A5,COH_SP:4,5
,ENUMSET1:29;
  hence thesis by A1,A3,A4,COH_SP:5,ZFMISC_1:32;
end;

Lm7: for C being Coherence_Space holds 'not' 'not' C c= C
proof
  let C be Coherence_Space;
  let x be set;
  assume x in 'not' 'not' C;
  then consider a being Subset of union 'not' C such that
A1: x = a and
A2: for b being Element of 'not' C ex x being set st a /\ b c= {x};
A3: union 'not' C = union C by Th66;
  now
    let x,y be set;
    assume that
A4: x in a and
A5: y in a and
A6: not {x,y} in C;
    {x,y} c= union C by A3,A4,A5,ZFMISC_1:32;
    then {x,y} in 'not' C by A6,Th68;
    then consider z being set such that
A7: a /\ {x,y} c= {z} by A2;
    y in {x,y} by TARSKI:def 2;
    then y in a/\{x,y} by A5,XBOOLE_0:def 4;
    then
A8: y = z by A7,TARSKI:def 1;
    x in {x,y} by TARSKI:def 2;
    then x in a/\{x,y} by A4,XBOOLE_0:def 4;
    then x = z by A7,TARSKI:def 1;
    then {x,y} = {x} by A8,ENUMSET1:29;
    hence contradiction by A3,A4,A6,COH_SP:4;
  end;
  hence thesis by A1,COH_SP:6;
end;

theorem Th70:
  for C being Coherence_Space holds 'not' 'not' C = C
proof
  let C be Coherence_Space;
  thus 'not' 'not' C c= C by Lm7;
  let a be set;
  assume
A1: a in C;
A2: union C = union 'not' C & union 'not' C = union 'not' 'not' C by Th66;
  now
    let x,y be set;
    assume that
A3: x in a and
A4: y in a;
A5: x in union C by A1,A3,TARSKI:def 4;
    {x,y} c= a by A3,A4,ZFMISC_1:32;
    then {x,y} in C by A1,CLASSES1:def 1;
    then
A6: x <> y implies not {x,y} in 'not' C by Th67;
    y in union C by A1,A4,TARSKI:def 4;
    then
A7: {x,y} c= union C by A5,ZFMISC_1:32;
    {x,x} = {x} by ENUMSET1:29;
    hence {x,y} in 'not' 'not' C by A2,A5,A7,A6,Th68,COH_SP:4;
  end;
  hence thesis by COH_SP:6;
end;

theorem
  'not' {{}} = {{}}
proof
  union 'not' {{}} = union {{}} by Th66
    .= {} by ZFMISC_1:25;
  hence 'not' {{}} c= {{}} by ZFMISC_1:1,82;
  {} in 'not' {{}} by COH_SP:1;
  hence thesis by ZFMISC_1:31;
end;

theorem
  for X being set holds 'not' FlatCoh X = bool X & 'not' bool X = FlatCoh X
proof
  let X be set;
  thus 'not' FlatCoh X = bool X
  proof
    hereby
      let x be set;
      assume x in 'not' FlatCoh X;
      then x c= union FlatCoh X by Th65;
      then x c= X by Th2;
      hence x in bool X;
    end;
    let x be set;
A1: now
      let a be Element of FlatCoh X;
      per cases by Th1;
      suppose
        a = {};
        then x /\ a c= {0} by XBOOLE_1:2;
        hence ex z being set st x /\ a c= {z};
      end;
      suppose
        ex z being set st a = {z} & z in X;
        then consider z being set such that
A2:     a = {z} and
        z in X;
        take z;
        thus x /\ a c= {z} by A2,XBOOLE_1:17;
      end;
    end;
    assume x in bool X;
    then x c= X;
    then x c= union FlatCoh X by Th2;
    hence thesis by A1;
  end;
  hence thesis by Th70;
end;

begin :: Product and Coproduct on Coherence Spaces

definition
  let x,y be set;
  func x U+ y -> set equals
  Union disjoin <*x,y*>;
  correctness;
end;

theorem Th73:
  for x,y being set holds x U+ y = [:x,{1}:] \/ [:y,{2}:]
proof
  let x,y be set;
  len <*x,y*> = 2 by FINSEQ_1:44;
  then
A1: dom <*x,y*> = {1,2} by FINSEQ_1:2,def 3;
  now
    let z be set;
A2: z`2 in {1,2} iff z`2 = 1 or z`2 = 2 by TARSKI:def 2;
A3: z in [:x,{1}:] iff z`1 in x & z`2 = 1 & z = [z`1,z`2] by MCART_1:13,21
,ZFMISC_1:106;
A4: z in [:y,{2}:] iff z`1 in y & z`2 = 2 & z = [z`1,z`2] by MCART_1:13,21
,ZFMISC_1:106;
    z in x U+ y iff z`2 in {1,2} & z`1 in <*x,y*>.(z`2) & z = [z`1,z`2] by A1,
CARD_3:22;
    hence z in x U+ y iff z in [:x,{1}:] \/ [:y,{2}:] by A2,A3,A4,FINSEQ_1:44
,XBOOLE_0:def 3;
  end;
  hence thesis by TARSKI:1;
end;

theorem Th74:
  for x being set holds x U+ {} = [:x,{1}:] & {} U+ x = [:x,{2}:]
proof
  let x be set;
  thus x U+ {} = [:x,{1}:] \/ [:{},{2}:] by Th73
    .= [:x,{1}:] \/ {} by ZFMISC_1:90
    .= [:x,{1}:];
  thus {} U+ x = [:{},{1}:] \/ [:x,{2}:] by Th73
    .= {} \/ [:x,{2}:] by ZFMISC_1:90
    .= [:x,{2}:];
end;

theorem Th75:
  for x,y,z being set st z in x U+ y holds z = [z`1,z`2] & (z`2 =
  1 & z`1 in x or z`2 = 2 & z`1 in y)
proof
  let x,y,z be set;
  assume z in x U+ y;
  then z in [:x,{1}:] \/ [:y,{2}:] by Th73;
  then z in [:x,{1}:] or z in [:y,{2}:] by XBOOLE_0:def 3;
  hence thesis by MCART_1:13,21;
end;

theorem Th76:
  for x,y,z being set holds [z,1] in x U+ y iff z in x
proof
  let x,y,z be set;
  x U+ y = [:x,{1}:] \/ [:y,{2}:] by Th73;
  then
  [z,1] in x U+ y iff [z,1] in [:x,{1}:] or [z,1] in [:y,{2}:] & 1 <> 2 by
XBOOLE_0:def 3;
  hence thesis by ZFMISC_1:106;
end;

theorem Th77:
  for x,y,z being set holds [z,2] in x U+ y iff z in y
proof
  let x,y,z be set;
  x U+ y = [:x,{1}:] \/ [:y,{2}:] by Th73;
  then
  [z,2] in x U+ y iff [z,2] in [:x,{1}:] & 1 <> 2 or [z,2] in [:y,{2}:] by
XBOOLE_0:def 3;
  hence thesis by ZFMISC_1:106;
end;

theorem Th78:
  for x1,y1, x2,y2 being set holds x1 U+ y1 c= x2 U+ y2 iff x1 c= x2 & y1 c= y2
proof
  let x1,y1, x2,y2 be set;
  hereby
    assume
A1: x1 U+ y1 c= x2 U+ y2;
    thus x1 c= x2
    proof
      let a be set;
      assume a in x1;
      then [a,1] in x1 U+ y1 by Th76;
      hence thesis by A1,Th76;
    end;
    thus y1 c= y2
    proof
      let a be set;
      assume a in y1;
      then [a,2] in x1 U+ y1 by Th77;
      hence thesis by A1,Th77;
    end;
  end;
  assume
A2: x1 c= x2 & y1 c= y2;
  let a be set;
  assume
A3: a in x1 U+ y1;
  then
A4: a`2 = 1 & a`1 in x1 or a`2 = 2 & a`1 in y1 by Th75;
  a = [a`1,a`2] by A3,Th75;
  hence thesis by A2,A4,Th76,Th77;
end;

theorem Th79:
  for x,y, z being set st z c= x U+ y ex x1,y1 being set st z = x1
  U+ y1 & x1 c= x & y1 c= y
proof
  let x,y,z be set;
  assume
A1: z c= x U+ y;
  take x1 = proj1 (z /\ [:x,{1}:]), y1 = proj1 (z /\ [:y,{2}:]);
A2: x U+ y = [:x,{1}:] \/ [:y,{2}:] by Th73;
  thus z = x1 U+ y1
  proof
    hereby
      let a be set;
      assume
A3:   a in z;
      then
A4:   a = [a`1,a`2] by A1,Th75;
      a in [:x,{1}:] or a in [:y,{2}:] by A1,A2,A3,XBOOLE_0:def 3;
      then
      a in z /\ [:x,{1}:] & a`2 = 1 or a in z /\ [:y,{2}:] & a`2 = 2 by A3,A4,
XBOOLE_0:def 4,ZFMISC_1:106;
      then a`1 in x1 & a`2 = 1 or a`1 in y1 & a`2 = 2
              by A4,XTUPLE_0:def 12;
      hence a in x1 U+ y1 by A4,Th76,Th77;
    end;
    let a be set;
    assume
A5: a in x1 U+ y1;
    then
A6: a = [a`1,a`2] by Th75;
    per cases by A5,Th75;
    suppose
A7:   a`2 = 1 & a`1 in x1;
      then consider b being set such that
A8:   [a`1,b] in z /\ [:x,{1}:] by XTUPLE_0:def 12;
      [a`1,b] in z & [a`1,b] in [:x,{1}:] by A8,XBOOLE_0:def 4;
      hence thesis by A6,A7,ZFMISC_1:106;
    end;
    suppose
A9:   a`2 = 2 & a`1 in y1;
      then consider b being set such that
A10:  [a`1,b] in z /\ [:y,{2}:] by XTUPLE_0:def 12;
      [a`1,b] in z & [a`1,b] in [:y,{2}:] by A10,XBOOLE_0:def 4;
      hence thesis by A6,A9,ZFMISC_1:106;
    end;
  end;
  z /\ [:y,{2}:] c= [:y,{2}:] by XBOOLE_1:17;
  then
A11: y1 c= proj1 [:y,{2}:] by XTUPLE_0:8;
  z /\ [:x,{1}:] c= [:x,{1}:] by XBOOLE_1:17;
  then x1 c= proj1 [:x,{1}:] by XTUPLE_0:8;
  hence thesis by A11,FUNCT_5:9;
end;

theorem Th80:
  for x1,y1, x2,y2 being set holds x1 U+ y1 = x2 U+ y2 iff x1 = x2 & y1 = y2
proof
  let x1,y1, x2,y2 be set;
A1: x1 U+ y1 c= x2 U+ y2 iff x1 c= x2 & y1 c= y2 by Th78;
  x2 U+ y2 c= x1 U+ y1 iff x2 c= x1 & y2 c= y1 by Th78;
  hence thesis by A1,XBOOLE_0:def 10;
end;

theorem Th81:
  for x1,y1, x2,y2 being set holds x1 U+ y1 \/ x2 U+ y2 = (x1 \/
  x2) U+ (y1 \/ y2)
proof
  let x1,y1, x2,y2 be set;
  set X1 = [:x1,{1}:], X2 = [:x2,{1}:];
  set Y1 = [:y1,{2}:], Y2 = [:y2,{2}:];
  set X = [:x1 \/ x2, {1}:], Y = [:y1 \/ y2, {2}:];
A1: X = X1 \/ X2 by ZFMISC_1:97;
A2: (x1 \/ x2) U+ (y1 \/ y2) = X \/ Y & Y = Y1 \/ Y2 by Th73,ZFMISC_1:97;
  x1 U+ y1 = X1 \/ Y1 & x2 U+ y2 = X2 \/ Y2 by Th73;
  hence x1 U+ y1 \/ x2 U+ y2 = X1 \/ Y1 \/ X2 \/ Y2 by XBOOLE_1:4
    .= X \/ Y1 \/ Y2 by A1,XBOOLE_1:4
    .= (x1 \/ x2) U+ (y1 \/ y2) by A2,XBOOLE_1:4;
end;

theorem Th82:
  for x1,y1, x2,y2 being set holds (x1 U+ y1) /\ (x2 U+ y2) = (x1
  /\ x2) U+ (y1 /\ y2)
proof
  let x1,y1, x2,y2 be set;
  set X1 = [:x1,{1}:], X2 = [:x2,{1}:];
  set Y1 = [:y1,{2}:], Y2 = [:y2,{2}:];
  set X = [:x1 /\ x2, {1}:], Y = [:y1 /\ y2, {2}:];
A1: X = X1 /\ X2 by ZFMISC_1:99;
A2: {1} misses {2} by ZFMISC_1:11;
  then Y1 misses X2 by ZFMISC_1:104;
  then
A3: Y = Y1 /\ Y2 & Y1 /\ X2 = {} by XBOOLE_0:def 7,ZFMISC_1:99;
  X1 misses Y2 by A2,ZFMISC_1:104;
  then
A4: X1 /\ Y2 = {} by XBOOLE_0:def 7;
  x1 U+ y1 = X1 \/ Y1 & x2 U+ y2 = X2 \/ Y2 by Th73;
  hence (x1 U+ y1) /\ (x2 U+ y2) = ((X1 \/ Y1) /\ X2) \/ ((X1 \/ Y1) /\ Y2) by
XBOOLE_1:23
    .= (X \/ Y1 /\ X2) \/ ((X1 \/ Y1) /\ Y2) by A1,XBOOLE_1:23
    .= X \/ (X1 /\ Y2 \/ Y) by A3,XBOOLE_1:23
    .= (x1 /\ x2) U+ (y1 /\ y2) by A4,Th73;
end;

definition
  let C1, C2 be Coherence_Space;
  func C1 "/\" C2 -> set equals
  {a U+ b where a is Element of C1, b is Element
  of C2: not contradiction};
  correctness;
  func C1 "\/" C2 -> set equals
  {a U+ {} where a is Element of C1: not
  contradiction} \/ {{} U+ b where b is Element of C2: not contradiction};
  correctness;
end;

theorem Th83:
  for C1,C2 being Coherence_Space for x being set holds x in C1
  "/\" C2 iff ex a being Element of C1, b being Element of C2 st x = a U+ b;

theorem Th84:
  for C1,C2 being Coherence_Space for x,y being set holds x U+ y
  in C1 "/\" C2 iff x in C1 & y in C2
proof
  let C1,C2 be Coherence_Space, x,y be set;
  now
    given a being Element of C1, b being Element of C2 such that
A1: x U+ y = a U+ b;
    take a,b;
    thus x = a & y = b by A1,Th80;
  end;
  hence thesis;
end;

theorem Th85:
  for C1,C2 being Coherence_Space holds union (C1 "/\" C2) = (
  union C1) U+ (union C2)
proof
  let C1,C2 be Coherence_Space;
  thus union (C1 "/\" C2) c= (union C1) U+ (union C2)
  proof
    let x be set;
    assume x in union (C1 "/\" C2);
    then consider a being set such that
A1: x in a and
A2: a in C1 "/\" C2 by TARSKI:def 4;
    consider a1 being Element of C1, a2 being Element of C2 such that
A3: a = a1 U+ a2 by A2;
    a1 c= union C1 & a2 c= union C2 by ZFMISC_1:74;
    then a c= (union C1) U+ (union C2) by A3,Th78;
    hence thesis by A1;
  end;
  let z be set;
  assume
A4: z in (union C1) U+ (union C2);
  then
A5: z = [z`1,z`2] by Th75;
  per cases by A4,Th75;
  suppose
A6: z`2 = 1 & z`1 in union C1;
    set b = the Element of C2;
    consider a being set such that
A7: z`1 in a and
A8: a in C1 by A6,TARSKI:def 4;
    reconsider a as Element of C1 by A8;
A9: a U+ b in C1 "/\" C2;
    z in a U+ b by A5,A6,A7,Th76;
    hence thesis by A9,TARSKI:def 4;
  end;
  suppose
A10: z`2 = 2 & z`1 in union C2;
    set b = the Element of C1;
    consider a being set such that
A11: z`1 in a and
A12: a in C2 by A10,TARSKI:def 4;
    reconsider a as Element of C2 by A12;
A13: b U+ a in C1 "/\" C2;
    z in b U+ a by A5,A10,A11,Th77;
    hence thesis by A13,TARSKI:def 4;
  end;
end;

theorem Th86:
  for C1,C2 being Coherence_Space for x,y being set holds x U+ y
  in C1 "\/" C2 iff x in C1 & y = {} or x = {} & y in C2
proof
  let C1,C2 be Coherence_Space, x,y be set;
A1: now
    given a being Element of C1 such that
A2: x U+ y = a U+ {};
    x = a by A2,Th80;
    hence x in C1 & y = {} by A2,Th80;
  end;
A3: now
    given a being Element of C2 such that
A4: x U+ y = {} U+ a;
    y = a by A4,Th80;
    hence y in C2 & x = {} by A4,Th80;
  end;
  x U+ y in C1 "\/" C2 iff x U+ y in {a U+ {} where a is Element of C1:
  not contradiction} or x U+ y in {{} U+ b where b is Element of C2: not
  contradiction} by XBOOLE_0:def 3;
  hence thesis by A1,A3;
end;

theorem Th87:
  for C1,C2 being Coherence_Space for x being set st x in C1 "\/"
C2 ex a being Element of C1, b being Element of C2 st x = a U+ b & (a = {} or b
  = {})
proof
  let C1,C2 be Coherence_Space, x be set;
  assume x in C1 "\/" C2;
  then x in {a U+ {} where a is Element of C1: not contradiction} or x in {{}
  U+ b where b is Element of C2: not contradiction} by XBOOLE_0:def 3;
  then
  {} in C2 & (ex a being Element of C1 st x = a U+ {}) or {} in C1 & ex b
  being Element of C2 st x = {} U+ b by COH_SP:1;
  hence thesis;
end;

theorem
  for C1,C2 being Coherence_Space holds union (C1 "\/" C2) = (union C1)
  U+ (union C2)
proof
  let C1,C2 be Coherence_Space;
  thus union (C1 "\/" C2) c= (union C1) U+ (union C2)
  proof
    let x be set;
    assume x in union (C1 "\/" C2);
    then consider a being set such that
A1: x in a and
A2: a in C1 "\/" C2 by TARSKI:def 4;
    consider a1 being Element of C1, a2 being Element of C2 such that
A3: a = a1 U+ a2 and
    a1 = {} or a2 = {} by A2,Th87;
    a1 c= union C1 & a2 c= union C2 by ZFMISC_1:74;
    then a c= (union C1) U+ (union C2) by A3,Th78;
    hence thesis by A1;
  end;
  let z be set;
  assume
A4: z in (union C1) U+ (union C2);
  then
A5: z = [z`1,z`2] by Th75;
  per cases by A4,Th75;
  suppose
A6: z`2 = 1 & z`1 in union C1;
    reconsider b = {} as Element of C2 by COH_SP:1;
    consider a being set such that
A7: z`1 in a and
A8: a in C1 by A6,TARSKI:def 4;
    reconsider a as Element of C1 by A8;
A9: a U+ b in C1 "\/" C2 by Th86;
    z in a U+ b by A5,A6,A7,Th76;
    hence thesis by A9,TARSKI:def 4;
  end;
  suppose
A10: z`2 = 2 & z`1 in union C2;
    reconsider b = {} as Element of C1 by COH_SP:1;
    consider a being set such that
A11: z`1 in a and
A12: a in C2 by A10,TARSKI:def 4;
    reconsider a as Element of C2 by A12;
A13: b U+ a in C1 "\/" C2 by Th86;
    z in b U+ a by A5,A10,A11,Th77;
    hence thesis by A13,TARSKI:def 4;
  end;
end;

registration
  let C1, C2 be Coherence_Space;
  cluster C1 "/\" C2 -> non empty subset-closed binary_complete;
  coherence
  proof
    set a9 = the Element of C1,b9 = the Element of C2;
    a9 U+ b9 in C1 "/\" C2;
    hence C1 "/\" C2 is non empty;
    hereby
      let a, b be set;
      assume a in C1 "/\" C2;
      then consider aa being Element of C1, bb being Element of C2 such that
A1:   a = aa U+ bb;
      assume b c= a;
      then consider x1,y1 being set such that
A2:   b = x1 U+ y1 and
A3:   x1 c= aa & y1 c= bb by A1,Th79;
      x1 in C1 & y1 in C2 by A3,CLASSES1:def 1;
      hence b in C1 "/\" C2 by A2;
    end;
    let A be set such that
A4: for a,b being set st a in A & b in A holds a \/ b in C1 "/\" C2;
    set A2 = {b where b is Element of C2: ex a being Element of C1 st a U+ b
    in A};
    now
      let x,y be set;
      assume x in A2;
      then consider ax being Element of C2 such that
A5:   x = ax and
A6:   ex b being Element of C1 st b U+ ax in A;
      consider bx being Element of C1 such that
A7:   bx U+ ax in A by A6;
      assume y in A2;
      then consider ay being Element of C2 such that
A8:   y = ay and
A9:   ex b being Element of C1 st b U+ ay in A;
      consider by1 being Element of C1 such that
A10:  by1 U+ ay in A by A9;
      (bx U+ ax) \/ (by1 U+ ay) in C1 "/\" C2 by A4,A7,A10;
      then (bx \/ by1) U+ (ax \/ ay) in C1 "/\" C2 by Th81;
      hence x \/ y in C2 by A5,A8,Th84;
    end;
    then
A11: union A2 in C2 by Def1;
    set A1 = {a where a is Element of C1: ex b being Element of C2 st a U+ b
    in A};
A12: (union A1) U+ union A2 = union A
    proof
      hereby
        let x be set;
        assume
A13:    x in (union A1) U+ union A2;
        then
A14:    x = [x`1,x`2] by Th75;
        per cases by A13,Th75;
        suppose
A15:      x`2 = 1 & x`1 in union A1;
          then consider a being set such that
A16:      x`1 in a and
A17:      a in A1 by TARSKI:def 4;
          consider ax being Element of C1 such that
A18:      a = ax and
A19:      ex b being Element of C2 st ax U+ b in A by A17;
          consider bx being Element of C2 such that
A20:      ax U+ bx in A by A19;
          x in ax U+ bx by A14,A15,A16,A18,Th76;
          hence x in union A by A20,TARSKI:def 4;
        end;
        suppose
A21:      x`2 = 2 & x`1 in union A2;
          then consider a being set such that
A22:      x`1 in a and
A23:      a in A2 by TARSKI:def 4;
          consider bx being Element of C2 such that
A24:      a = bx and
A25:      ex a being Element of C1 st a U+ bx in A by A23;
          consider ax being Element of C1 such that
A26:      ax U+ bx in A by A25;
          x in ax U+ bx by A14,A21,A22,A24,Th77;
          hence x in union A by A26,TARSKI:def 4;
        end;
      end;
      let x be set;
      assume x in union A;
      then consider a being set such that
A27:  x in a and
A28:  a in A by TARSKI:def 4;
      a \/ a in C1 "/\" C2 by A4,A28;
      then consider aa being Element of C1, bb being Element of C2 such that
A29:  a = aa U+ bb;
      bb in A2 by A28,A29;
      then
A30:  bb c= union A2 by ZFMISC_1:74;
      aa in A1 by A28,A29;
      then aa c= union A1 by ZFMISC_1:74;
      then aa U+ bb c= (union A1) U+ union A2 by A30,Th78;
      hence thesis by A27,A29;
    end;
    now
      let x,y be set;
      assume x in A1;
      then consider ax being Element of C1 such that
A31:  x = ax and
A32:  ex b being Element of C2 st ax U+ b in A;
      consider bx being Element of C2 such that
A33:  ax U+ bx in A by A32;
      assume y in A1;
      then consider ay being Element of C1 such that
A34:  y = ay and
A35:  ex b being Element of C2 st ay U+ b in A;
      consider by1 being Element of C2 such that
A36:  ay U+ by1 in A by A35;
      (ax U+ bx) \/ (ay U+ by1) in C1 "/\" C2 by A4,A33,A36;
      then (ax \/ ay) U+ (bx \/ by1) in C1 "/\" C2 by Th81;
      hence x \/ y in C1 by A31,A34,Th84;
    end;
    then union A1 in C1 by Def1;
    hence thesis by A11,A12;
  end;
  cluster C1 "\/" C2 -> non empty subset-closed binary_complete;
  coherence
  proof
    set a9 = the Element of C1;
    a9 U+ {} in C1 "\/" C2 by Th86;
    hence C1 "\/" C2 is non empty;
    hereby
      let a, b be set;
      assume a in C1 "\/" C2;
      then consider aa being Element of C1, bb being Element of C2 such that
A37:  a = aa U+ bb and
A38:  aa = {} or bb = {} by Th87;
      assume b c= a;
      then consider x1,y1 being set such that
A39:  b = x1 U+ y1 and
A40:  x1 c= aa & y1 c= bb by A37,Th79;
A41:  x1 in C1 & y1 in C2 by A40,CLASSES1:def 1;
      x1 = {} or y1 = {} by A38,A40;
      hence b in C1 "\/" C2 by A39,A41,Th86;
    end;
    let A be set;
    set A1 = {a where a is Element of C1: ex b being Element of C2 st a U+ b
    in A};
    set A2 = {b where b is Element of C2: ex a being Element of C1 st a U+ b
    in A};
    assume
A42: for a,b being set st a in A & b in A holds a \/ b in C1 "\/" C2;
    now
      let x,y be set;
      assume x in A2;
      then consider ax being Element of C2 such that
A43:  x = ax and
A44:  ex b being Element of C1 st b U+ ax in A;
      consider bx being Element of C1 such that
A45:  bx U+ ax in A by A44;
      assume y in A2;
      then consider ay being Element of C2 such that
A46:  y = ay and
A47:  ex b being Element of C1 st b U+ ay in A;
      consider by1 being Element of C1 such that
A48:  by1 U+ ay in A by A47;
      (bx U+ ax) \/ (by1 U+ ay) in C1 "\/" C2 by A42,A45,A48;
      then (bx \/ by1) U+ (ax \/ ay) in C1 "\/" C2 by Th81;
      then x \/ y in C2 or x \/ y = {} by A43,A46,Th86;
      hence x \/ y in C2 by COH_SP:1;
    end;
    then
A49: union A2 in C2 by Def1;
A50: (union A1) U+ union A2 = union A
    proof
      hereby
        let x be set;
        assume
A51:    x in (union A1) U+ union A2;
        then
A52:    x = [x`1,x`2] by Th75;
        per cases by A51,Th75;
        suppose
A53:      x`2 = 1 & x`1 in union A1;
          then consider a being set such that
A54:      x`1 in a and
A55:      a in A1 by TARSKI:def 4;
          consider ax being Element of C1 such that
A56:      a = ax and
A57:      ex b being Element of C2 st ax U+ b in A by A55;
          consider bx being Element of C2 such that
A58:      ax U+ bx in A by A57;
          x in ax U+ bx by A52,A53,A54,A56,Th76;
          hence x in union A by A58,TARSKI:def 4;
        end;
        suppose
A59:      x`2 = 2 & x`1 in union A2;
          then consider a being set such that
A60:      x`1 in a and
A61:      a in A2 by TARSKI:def 4;
          consider bx being Element of C2 such that
A62:      a = bx and
A63:      ex a being Element of C1 st a U+ bx in A by A61;
          consider ax being Element of C1 such that
A64:      ax U+ bx in A by A63;
          x in ax U+ bx by A52,A59,A60,A62,Th77;
          hence x in union A by A64,TARSKI:def 4;
        end;
      end;
      let x be set;
      assume x in union A;
      then consider a being set such that
A65:  x in a and
A66:  a in A by TARSKI:def 4;
      a \/ a in C1 "\/" C2 by A42,A66;
      then consider aa being Element of C1, bb being Element of C2 such that
A67:  a = aa U+ bb and
      aa = {} or bb = {} by Th87;
      bb in A2 by A66,A67;
      then
A68:  bb c= union A2 by ZFMISC_1:74;
      aa in A1 by A66,A67;
      then aa c= union A1 by ZFMISC_1:74;
      then aa U+ bb c= (union A1) U+ union A2 by A68,Th78;
      hence thesis by A65,A67;
    end;
A69: now
      assume union A1 <> {};
      then reconsider AA = union A1 as non empty set;
      set aa = the Element of AA;
      consider x being set such that
A70:  aa in x and
A71:  x in A1 by TARSKI:def 4;
      consider ax being Element of C1 such that
A72:  x = ax and
A73:  ex b being Element of C2 st ax U+ b in A by A71;
      consider bx being Element of C2 such that
A74:  ax U+ bx in A by A73;
      assume union A2 <> {};
      then reconsider AA = union A2 as non empty set;
      set bb = the Element of AA;
      consider y being set such that
A75:  bb in y and
A76:  y in A2 by TARSKI:def 4;
      consider by1 being Element of C2 such that
A77:  y = by1 and
A78:  ex a being Element of C1 st a U+ by1 in A by A76;
      consider ay being Element of C1 such that
A79:  ay U+ by1 in A by A78;
      (ax U+ bx) \/ (ay U+ by1) in C1 "\/" C2 by A42,A74,A79;
      then (ax \/ ay) U+ (bx \/ by1) in C1 "\/" C2 by Th81;
      hence contradiction by A70,A72,A75,A77,Th86;
    end;
    now
      let x,y be set;
      assume x in A1;
      then consider ax being Element of C1 such that
A80:  x = ax and
A81:  ex b being Element of C2 st ax U+ b in A;
      consider bx being Element of C2 such that
A82:  ax U+ bx in A by A81;
      assume y in A1;
      then consider ay being Element of C1 such that
A83:  y = ay and
A84:  ex b being Element of C2 st ay U+ b in A;
      consider by1 being Element of C2 such that
A85:  ay U+ by1 in A by A84;
      (ax U+ bx) \/ (ay U+ by1) in C1 "\/" C2 by A42,A82,A85;
      then (ax \/ ay) U+ (bx \/ by1) in C1 "\/" C2 by Th81;
      then x \/ y in C1 or x \/ y = {} by A80,A83,Th86;
      hence x \/ y in C1 by COH_SP:1;
    end;
    then union A1 in C1 by Def1;
    hence thesis by A49,A69,A50,Th86;
  end;
end;

reserve C1, C2 for Coherence_Space;

theorem
  for x,y being set holds [[x,1],[y,1]] in Web (C1 "/\" C2) iff [x,y] in Web C1
proof
  let x,y be set;
A1: [[x,1],[y,1]] in Web (C1 "/\" C2) iff {[x,1],[y,1]} in C1 "/\" C2 by
COH_SP:5;
A2: [x,y] in Web C1 iff {x,y} in C1 by COH_SP:5;
A3: [:{x,y},{1}:] = {[x,1],[y,1]} by ZFMISC_1:30;
  {x,y} U+ {} = [:{x,y},{1}:] & {} in C2 by Th74,COH_SP:1;
  hence thesis by A1,A2,A3,Th84;
end;

theorem
  for x,y being set holds [[x,2],[y,2]] in Web (C1 "/\" C2) iff [x,y] in Web C2
proof
  let x,y be set;
A1: [[x,2],[y,2]] in Web (C1 "/\" C2) iff {[x,2],[y,2]} in C1 "/\" C2 by
COH_SP:5;
A2: [x,y] in Web C2 iff {x,y} in C2 by COH_SP:5;
A3: [:{x,y},{2}:] = {[x,2],[y,2]} by ZFMISC_1:30;
  {} U+ {x,y} = [:{x,y},{2}:] & {} in C1 by Th74,COH_SP:1;
  hence thesis by A1,A2,A3,Th84;
end;

theorem
  for x,y being set st x in union C1 & y in union C2 holds [[x,1],[y,2]]
  in Web (C1 "/\" C2) & [[y,2],[x,1]] in Web (C1 "/\" C2)
proof
  let x,y be set;
  assume x in union C1 & y in union C2;
  then {x} in C1 & {y} in C2 by COH_SP:4;
  then {x} U+ {y} in C1 "/\" C2;
  then [:{x},{1}:] \/ [:{y},{2}:] in C1 "/\" C2 by Th73;
  then {[x,1]} \/ [:{y},{2}:] in C1 "/\" C2 by ZFMISC_1:29;
  then {[x,1]} \/ {[y,2]} in C1 "/\" C2 by ZFMISC_1:29;
  then
A1: {[x,1],[y,2]} in C1 "/\" C2 by ENUMSET1:1;
  hence [[x,1],[y,2]] in Web (C1 "/\" C2) by COH_SP:5;
  thus thesis by A1,COH_SP:5;
end;

theorem
  for x,y being set holds [[x,1],[y,1]] in Web (C1 "\/" C2) iff [x,y] in Web C1
proof
  let x,y be set;
A1: [[x,1],[y,1]] in Web (C1 "\/" C2) iff {[x,1],[y,1]} in C1 "\/" C2 by
COH_SP:5;
A2: [x,y] in Web C1 iff {x,y} in C1 by COH_SP:5;
  {x,y} U+ {} = [:{x,y},{1}:] & [:{x,y},{1}:] = {[x,1],[y,1]} by Th74,
ZFMISC_1:30;
  hence thesis by A1,A2,Th86;
end;

theorem
  for x,y being set holds [[x,2],[y,2]] in Web (C1 "\/" C2) iff [x,y] in Web C2
proof
  let x,y be set;
A1: [[x,2],[y,2]] in Web (C1 "\/" C2) iff {[x,2],[y,2]} in C1 "\/" C2 by
COH_SP:5;
A2: [x,y] in Web C2 iff {x,y} in C2 by COH_SP:5;
  {} U+ {x,y} = [:{x,y},{2}:] & [:{x,y},{2}:] = {[x,2],[y,2]} by Th74,
ZFMISC_1:30;
  hence thesis by A1,A2,Th86;
end;

theorem
  for x,y being set holds not [[x,1],[y,2]] in Web (C1 "\/" C2) & not [[
  y,2],[x,1]] in Web (C1 "\/" C2)
proof
  let x,y be set;
A1: {x} U+ {y} = [:{x},{1}:] \/ [:{y},{2}:] by Th73
    .= {[x,1]} \/ [:{y},{2}:] by ZFMISC_1:29
    .= {[x,1]} \/ {[y,2]} by ZFMISC_1:29
    .= {[x,1],[y,2]} by ENUMSET1:1;
A2: not {x} U+ {y} in C1 "\/" C2 by Th86;
  hence not [[x,1],[y,2]] in Web (C1 "\/" C2) by A1,COH_SP:5;
  thus thesis by A2,A1,COH_SP:5;
end;

theorem
  'not' (C1 "/\" C2) = 'not' C1 "\/" 'not' C2
proof
  set C = C1 "/\" C2;
  thus 'not' (C1 "/\" C2) c= 'not' C1 "\/" 'not' C2
  proof
    let x be set;
A1: union C = (union C1) U+ union C2 by Th85;
    assume
A2: x in 'not' (C1 "/\" C2);
    then x c= union C by Th65;
    then consider x1,x2 being set such that
A3: x = x1 U+ x2 and
A4: x1 c= union C1 and
A5: x2 c= union C2 by A1,Th79;
    now
      reconsider b = {} as Element of C2 by COH_SP:1;
      let a be Element of C1;
      a U+ b in C;
      then consider z being set such that
A6:   x /\ (a U+ b) c= {z} by A2,Th65;
      (x1 /\ a)U+(x2 /\ b) c= {z} by A3,A6,Th82;
      then
      [:x1 /\ a,{1}:] c= [:x1 /\ a,{1}:] \/ [:x2 /\ b,{2}:] & [:x1 /\ a,{
      1}:] \/ [:x2 /\ b,{2}:] c= {z} by Th73,XBOOLE_1:7;
      then
A7:   [:x1 /\ a,{1}:] c= {z} by XBOOLE_1:1;
      now
        thus x1 /\ a = {} implies x1 /\ a c= {0} by XBOOLE_1:2;
        assume x1 /\ a <> {};
        then reconsider A = x1 /\ a as non empty set;
        set z1 = the Element of A;
        reconsider zz = z1 as set;
        take zz;
        thus x1 /\ a c= {zz}
        proof
          let y be set;
A8:       1 in {1} by TARSKI:def 1;
          assume y in x1 /\ a;
          then [y,1] in [:x1 /\ a,{1}:] by A8,ZFMISC_1:87;
          then
A9:       [y,1] = z by A7,TARSKI:def 1;
          [z1,1] in [:x1 /\ a,{1}:] by A8,ZFMISC_1:87;
          then [z1,1] = z by A7,TARSKI:def 1;
          then y = z1 by A9,XTUPLE_0:1;
          hence thesis by TARSKI:def 1;
        end;
      end;
      hence ex z being set st x1 /\ a c= {z};
    end;
    then reconsider x1 as Element of 'not' C1 by A4,Th65;
    now
      reconsider a = {} as Element of C1 by COH_SP:1;
      let b be Element of C2;
      a U+ b in C;
      then consider z being set such that
A10:  x /\ (a U+ b) c= {z} by A2,Th65;
      (x1 /\ a)U+(x2 /\ b) c= {z} by A3,A10,Th82;
      then
      [:x2 /\ b,{2}:] c= [:x1 /\ a,{1}:] \/ [:x2 /\ b,{2}:] & [:x1 /\ a,{
      1}:] \/ [:x2 /\ b,{2}:] c= {z} by Th73,XBOOLE_1:7;
      then
A11:  [:x2 /\ b,{2}:] c= {z} by XBOOLE_1:1;
      now
        thus x2 /\ b = {} implies x2 /\ b c= {0} by XBOOLE_1:2;
        assume x2 /\ b <> {};
        then reconsider A = x2 /\ b as non empty set;
        set z1 = the Element of A;
        reconsider zz = z1 as set;
        take zz;
        thus x2 /\ b c= {zz}
        proof
          let y be set;
A12:      2 in {2} by TARSKI:def 1;
          assume y in x2 /\ b;
          then [y,2] in [:x2 /\ b,{2}:] by A12,ZFMISC_1:87;
          then
A13:      [y,2] = z by A11,TARSKI:def 1;
          [z1,2] in [:x2 /\ b,{2}:] by A12,ZFMISC_1:87;
          then [z1,2] = z by A11,TARSKI:def 1;
          then y = z1 by A13,XTUPLE_0:1;
          hence thesis by TARSKI:def 1;
        end;
      end;
      hence ex z being set st x2 /\ b c= {z};
    end;
    then reconsider x2 as Element of 'not' C2 by A5,Th65;
    now
      thus x1 in 'not' C1 & x2 in 'not' C2;
      assume x1 <> {} & x2 <> {};
      then reconsider x1, x2 as non empty set;
      set y1 = the Element of x1,y2 = the Element of x2;
      union 'not' C2 = union C2 by Th66;
      then y2 in union C2 by TARSKI:def 4;
      then
A14:  {y2} in C2 by COH_SP:4;
      union 'not' C1 = union C1 by Th66;
      then y1 in union C1 by TARSKI:def 4;
      then {y1} in C1 by COH_SP:4;
      then {y1} U+ {y2} in C by A14;
      then consider z being set such that
A15:  x /\ ({y1} U+ {y2}) c= {z} by A2,Th65;
A16:  (x1 /\ {y1})U+(x2 /\ {y2}) c= {z} by A3,A15,Th82;
      y2 in {y2} by TARSKI:def 1;
      then y2 in x2 /\ {y2} by XBOOLE_0:def 4;
      then [y2,2] in (x1 /\ {y1})U+(x2 /\ {y2}) by Th77;
      then
A17:  [y2,2] = z by A16,TARSKI:def 1;
      y1 in {y1} by TARSKI:def 1;
      then y1 in x1 /\ {y1} by XBOOLE_0:def 4;
      then [y1,1] in (x1 /\ {y1})U+(x2 /\ {y2}) by Th76;
      then [y1,1] = z by A16,TARSKI:def 1;
      hence contradiction by A17,XTUPLE_0:1;
    end;
    hence thesis by A3,Th86;
  end;
  let x be set;
  assume x in 'not' C1 "\/" 'not' C2;
  then consider
  x1 being Element of 'not' C1, x2 being Element of 'not' C2 such
  that
A18: x = x1 U+ x2 and
A19: x1 = {} or x2 = {} by Th87;
A20: for a being Element of C ex z being set st x /\ a c= {z}
  proof
    let a be Element of C;
    consider a1 being Element of C1, a2 being Element of C2 such that
A21: a = a1 U+ a2 by Th83;
A22: x /\ a = (x1/\a1)U+(x2/\a2) by A18,A21,Th82;
    consider z2 being set such that
A23: x2/\a2 c= {z2} by Th65;
    consider z1 being set such that
A24: x1/\a1 c= {z1} by Th65;
    x1 = {} or x1 <> {};
    then consider z being set such that
A25: z = [z2,2] & x1 = {} or z = [z1,1] & x1 <> {};
    take z;
    let y be set;
    assume
A26: y in x/\a;
    then
A27: y = [y`1,y`2] by A22,Th75;
A28: y`2 = 1 & y`1 in x1/\a1 or y`2 = 2 & y`1 in x2/\ a2 by A22,A26,Th75;
    per cases by A25;
    suppose
A29:  z = [z2,2] & x1 = {};
      then y`1 = z2 by A23,A28,TARSKI:def 1;
      hence thesis by A27,A28,A29,TARSKI:def 1;
    end;
    suppose
A30:  z = [z1,1] & x1 <> {};
      then y`1 = z1 by A19,A24,A28,TARSKI:def 1;
      hence thesis by A19,A27,A28,A30,TARSKI:def 1;
    end;
  end;
  x2 c= union 'not' C2 by ZFMISC_1:74;
  then
A31: x2 c= union C2 by Th66;
  x1 c= union 'not' C1 by ZFMISC_1:74;
  then x1 c= union C1 by Th66;
  then x c= (union C1)U+union C2 by A18,A31,Th78;
  then x c= union C by Th85;
  hence thesis by A20;
end;

definition
  let C1,C2 be Coherence_Space;
  func C1 [*] C2 -> set equals
  union {bool [:a,b:] where a is Element of C1, b
  is Element of C2: not contradiction};
  correctness;
end;

theorem Th96:
  for C1,C2 being Coherence_Space, x being set holds x in C1 [*]
  C2 iff ex a being Element of C1, b being Element of C2 st x c= [:a,b:]
proof
  let C1,C2 be Coherence_Space, x be set;
  hereby
    assume x in C1[*]C2;
    then consider y being set such that
A1: x in y and
A2: y in {bool [:a,b:] where a is Element of C1, b is Element of C2:
    not contradiction} by TARSKI:def 4;
    consider a being Element of C1, b being Element of C2 such that
A3: y = bool [:a,b:] by A2;
    take a,b;
    thus x c= [:a,b:] by A1,A3;
  end;
  given a9 being Element of C1, b9 being Element of C2 such that
A4: x c= [:a9,b9:];
  bool [:a9,b9:] in {bool [:a,b:] where a is Element of C1, b is Element
  of C2: not contradiction};
  hence thesis by A4,TARSKI:def 4;
end;

registration
  let C1,C2 be Coherence_Space;
  cluster C1 [*] C2 -> non empty;
  coherence
  proof
    set a1 = the Element of C1,a2 = the Element of C2;
    [:a1,a2:] in C1[*]C2 by Th96;
    hence thesis;
  end;
end;

theorem Th97:
  for C1,C2 being Coherence_Space, a being Element of C1 [*] C2
  holds proj1 a in C1 & proj2 a in C2 & a c= [:proj1 a, proj2 a:]
proof
  let C1,C2 be Coherence_Space, a be Element of C1 [*] C2;
  consider a1 being Element of C1, a2 being Element of C2 such that
A1: a c= [:a1,a2:] by Th96;
  proj1 a c= a1 & proj2 a c= a2 by A1,FUNCT_5:11;
  hence proj1 a in C1 & proj2 a in C2 by CLASSES1:def 1;
  let x be set;
  assume
A2: x in a;
  then
A3: x = [x`1,x`2] by A1,MCART_1:21;
  then x`1 in proj1 a & x`2 in proj2 a by A2,XTUPLE_0:def 12,def 13;
  hence thesis by A3,ZFMISC_1:87;
end;

registration
  let C1,C2 be Coherence_Space;
  cluster C1 [*] C2 -> subset-closed binary_complete;
  coherence
  proof
    thus C1[*]C2 is subset-closed
    proof
      let a,b be set;
      assume a in C1[*]C2;
      then consider a1 being Element of C1, a2 being Element of C2 such that
A1:   a c= [:a1,a2:] by Th96;
      assume b c= a;
      then b c= [:a1,a2:] by A1,XBOOLE_1:1;
      hence thesis by Th96;
    end;
    let A be set;
    set A1 = {proj1 a where a is Element of C1[*]C2: a in A};
    set A2 = {proj2 a where a is Element of C1[*]C2: a in A};
    assume
A2: for a,b being set st a in A & b in A holds a \/ b in C1 [*] C2;
    now
      let a1,b1 be set;
      assume a1 in A2;
      then consider a being Element of C1[*]C2 such that
A3:   a1 = proj2 a and
A4:   a in A;
      assume b1 in A2;
      then consider b being Element of C1[*]C2 such that
A5:   b1 = proj2 b and
A6:   b in A;
      a \/ b in C1[*]C2 by A2,A4,A6;
      then proj2 (a \/ b) in C2 by Th97;
      hence a1 \/ b1 in C2 by A3,A5,XTUPLE_0:27;
    end;
    then
A7: union A2 in C2 by Def1;
A8: union A c= [:union A1, union A2:]
    proof
      let x be set;
      assume x in union A;
      then consider a being set such that
A9:   x in a and
A10:  a in A by TARSKI:def 4;
A11:  a \/ a in C1[*]C2 by A2,A10;
      then proj2 a in A2 by A10;
      then
A12:  proj2 a c= union A2 by ZFMISC_1:74;
      a c= [:proj1 a, proj2 a:] by A11,Th97;
      then
A13:  x in [:proj1 a, proj2 a:] by A9;
      proj1 a in A1 by A10,A11;
      then proj1 a c= union A1 by ZFMISC_1:74;
      then [:proj1 a, proj2 a:] c= [:union A1, union A2:] by A12,ZFMISC_1:96;
      hence thesis by A13;
    end;
    now
      let a1,b1 be set;
      assume a1 in A1;
      then consider a being Element of C1[*]C2 such that
A14:  a1 = proj1 a and
A15:  a in A;
      assume b1 in A1;
      then consider b being Element of C1[*]C2 such that
A16:  b1 = proj1 b and
A17:  b in A;
      a \/ b in C1[*]C2 by A2,A15,A17;
      then proj1 (a \/ b) in C1 by Th97;
      hence a1 \/ b1 in C1 by A14,A16,XTUPLE_0:23;
    end;
    then union A1 in C1 by Def1;
    hence thesis by A7,A8,Th96;
  end;
end;

theorem
  for C1,C2 being Coherence_Space holds union (C1 [*] C2) = [:union C1,
  union C2:]
proof
  let C1,C2 be Coherence_Space;
  thus union (C1 [*] C2) c= [:union C1, union C2:]
  proof
    let x be set;
    assume x in union (C1 [*] C2);
    then consider a being set such that
A1: x in a and
A2: a in C1 [*] C2 by TARSKI:def 4;
    consider a1 being Element of C1, a2 being Element of C2 such that
A3: a c= [:a1,a2:] by A2,Th96;
    a1 c= union C1 & a2 c= union C2 by ZFMISC_1:74;
    then [:a1,a2:] c= [:union C1, union C2:] by ZFMISC_1:96;
    then a c= [:union C1, union C2:] by A3,XBOOLE_1:1;
    hence thesis by A1;
  end;
  let x,y be set;
  assume
A4: [x,y] in [:union C1, union C2:];
  then x in union C1 by ZFMISC_1:87;
  then consider a1 being set such that
A5: x in a1 and
A6: a1 in C1 by TARSKI:def 4;
  y in union C2 by A4,ZFMISC_1:87;
  then consider a2 being set such that
A7: y in a2 and
A8: a2 in C2 by TARSKI:def 4;
A9: [:a1,a2:] in C1 [*] C2 by A6,A8,Th96;
  [x,y] in [:a1,a2:] by A5,A7,ZFMISC_1:87;
  hence thesis by A9,TARSKI:def 4;
end;

theorem
  for x1,y1, x2,y2 being set holds [[x1,x2],[y1,y2]] in Web (C1 [*] C2)
  iff [x1,y1] in Web C1 & [x2,y2] in Web C2
proof
  let x1,y1, x2,y2 be set;
A1: {[x1,x2],[y1,y2]} c= [:{x1,y1}, {x2,y2}:]
  proof
    let x,y be set;
    assume [x,y] in {[x1,x2],[y1,y2]};
    then
    [x,y] = [x1,x2] & x1 in {x1,y1} & x2 in {x2,y2}
     or [x,y] = [y1,y2] & y1 in {x1
    ,y1} & y2 in {x2,y2} by TARSKI:def 2;
    hence thesis by ZFMISC_1:87;
  end;
A2: proj1 {[x1,x2],[y1,y2]} = {x1,y1} & proj2 {[x1,x2],[y1,y2]} = {x2,y2} by
FUNCT_5:13;
  hereby
    assume [[x1,x2],[y1,y2]] in Web (C1 [*] C2);
    then {[x1,x2],[y1,y2]} in C1 [*] C2 by COH_SP:5;
    then {x1,y1} in C1 & {x2,y2} in C2 by A2,Th97;
    hence [x1,y1] in Web C1 & [x2,y2] in Web C2 by COH_SP:5;
  end;
  assume [x1,y1] in Web C1 & [x2,y2] in Web C2;
  then {x1,y1} in C1 & {x2,y2} in C2 by COH_SP:5;
  then {[x1,x2],[y1,y2]} in C1 [*] C2 by A1,Th96;
  hence thesis by COH_SP:5;
end;