:: Basic Operations on Preordered Coherent Spaces
::  by Klaus E. Grue and Artur Korni{\l}owicz
::
:: Received August 28, 2007
:: Copyright (c) 2007-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 CARD_1, SUBSET_1, RELAT_1, XBOOLE_0, PARTFUN1, RELAT_2, PRALG_1,
      PBOOLE, RLVECT_2, FUNCT_1, STRUCT_0, ZFMISC_1, TARSKI, ORDERS_2,
      YELLOW16, YELLOW_1, MSUALG_4, EQREL_1, FUNCOP_1, MCART_1, XXREAL_0,
      WAYBEL_3, CARD_3, YELLOW_3, SETFAM_1, PCS_0, AFINSQ_1, FINSEQ_1;
 notations TARSKI, XBOOLE_0,
      XTUPLE_0, SUBSET_1, ZFMISC_1, MCART_1, DOMAIN_1, RELAT_1,
      FUNCT_1, PARTFUN1, RELSET_1, RELAT_2, EQREL_1, CARD_3, PARTIT_2, FUNCT_4,
      NUMBERS, PBOOLE, FUNCOP_1, AFINSQ_1, STRUCT_0, TSEP_1, ORDERS_2, PRALG_1,
      YELLOW_1, WAYBEL_3, YELLOW16, YELLOW_3;
 constructors PRALG_1, PARTIT_2, TSEP_1, YELLOW16, YELLOW_3, DOMAIN_1,
      RELSET_1, FUNCT_4, AFINSQ_1, XTUPLE_0;
 registrations EQREL_1, PARTFUN1, SUBSET_1, XBOOLE_0, WAYBEL_3, RELAT_1,
      TOLER_1, ORDERS_2, PRALG_1, STRUCT_0, YELLOW16, YELLOW_3, RELSET_1,
      FUNCOP_1, AFINSQ_1, RELAT_2, XTUPLE_0;
 requirements BOOLE, SUBSET;
 definitions SUBSET_1, RELAT_1, PARTFUN1, RELAT_2, EQREL_1, CARD_3, ORDERS_2,
      PARTIT_2, STRUCT_0, TSEP_1, PRALG_1, YELLOW_1, WAYBEL_3, TARSKI,
      XBOOLE_0, FUNCOP_1, XTUPLE_0;
 theorems ZFMISC_1, ORDERS_2, RELSET_1, PARTFUN1, RELAT_1, RELAT_2, XBOOLE_0,
      TARSKI, FUNCT_1, PBOOLE, FUNCOP_1, PRALG_1, XBOOLE_1, ORDERS_1, FUNCT_4,
      YELLOW16, YELLOW_0, WAYBEL_8, YELLOW_3, MCART_1, SETFAM_1, AFINSQ_1,
      CARD_1, XTUPLE_0;
 schemes RELSET_1, CLASSES1, RELAT_1;

begin :: Preliminaries

reconsider z = 0, j = 1 as Element of {0,1} by TARSKI:def 2;

definition
  let R1, R2 be set, R be Relation of R1,R2;
  redefine func field R -> Subset of R1 \/ R2;
  coherence by RELSET_1:8;
end;

definition
  let R1, R2, S1, S2 be set;
  let R be Relation of R1,R2;
  let S be Relation of S1,S2;
  redefine func R \/ S -> Relation of R1 \/ S1, R2 \/ S2;
  coherence by ZFMISC_1:119;
end;

registration
  let R1, S1 be set;
  let R being total Relation of R1;
  let S being total Relation of S1;
  cluster R \/ S -> total for Relation of R1 \/ S1;
  coherence
  proof
    dom (R \/ S) = (dom R) \/ dom S by RELAT_1:1
      .= R1 \/ dom S by PARTFUN1:def 2
      .= R1 \/ S1 by PARTFUN1:def 2;
    hence thesis by PARTFUN1:def 2;
  end;
end;

registration
  let R1, S1 be set;
  let R being reflexive Relation of R1;
  let S being reflexive Relation of S1;
  cluster R \/ S -> reflexive for Relation of R1 \/ S1;
  coherence;
end;

registration
  let R1, S1 be set;
  let R being symmetric Relation of R1;
  let S being symmetric Relation of S1;
  cluster R \/ S -> symmetric for Relation of R1 \/ S1;
  coherence;
end;

Lm1: now
  let R1, S1 be set;
  let R be Relation of R1;
  let S be Relation of S1 such that
A1: R1 misses S1;
  let q1, q2 be set such that
A2: [q1,q2] in R \/ S and
A3: q2 in S1;
A4: [q1,q2] in R or [q1,q2] in S by A2,XBOOLE_0:def 3;
  now
    assume [q1,q2] in R;
    then q2 in R1 by ZFMISC_1:87;
    hence contradiction by A1,A3,XBOOLE_0:3;
  end;
  hence [q1,q2] in S & q1 in S1 by A4,ZFMISC_1:87;
end;

theorem Th1:
  for R1, S1 being set, R being transitive (Relation of R1),
  S being transitive Relation of S1 st R1 misses S1 holds R \/ S is transitive
proof
  let R1, S1 be set, R be transitive (Relation of R1),
  S be transitive Relation of S1 such that
A1: R1 misses S1;
  let p1, p2, p3 be set;
  set RS = R \/ S;
  set D = field RS;
  assume that
  p1 in D and p2 in D and
A2: p3 in D and
A3: [p1,p2] in RS and
A4: [p2,p3] in RS;
  per cases by A2,XBOOLE_0:def 3;
  suppose
A5: p3 in R1;
    then p2 in R1 by A1,A4,Lm1;
    then
A6: [p1,p2] in R by A1,A3,Lm1;
    [p2,p3] in R by A1,A4,A5,Lm1;
    then [p1,p3] in R by A6,RELAT_2:31;
    hence thesis by XBOOLE_0:def 3;
  end;
  suppose
A7: p3 in S1;
    then p2 in S1 by A1,A4,Lm1;
    then
A8: [p1,p2] in S by A1,A3,Lm1;
    [p2,p3] in S by A1,A4,A7,Lm1;
    then [p1,p3] in S by A8,RELAT_2:31;
    hence thesis by XBOOLE_0:def 3;
  end;
end;

definition
  let I be non empty set, C be 1-sorted-yielding ManySortedSet of I;
  redefine func Carrier C means
  :Def1:
  for i being Element of I holds it.i = the carrier of C.i;
  compatibility
  proof
    let X be ManySortedSet of I;
    thus X = Carrier C implies
    for i being Element of I holds X.i = the carrier of C.i
    proof
      assume
A1:   X = Carrier C;
      let i be Element of I;
      ex P being 1-sorted st P = C.i & X.i = the carrier of P
      by A1,PRALG_1:def 13;
      hence thesis;
    end;
    assume
A2: for i being Element of I holds X.i = the carrier of C.i;
    for i being set st i in I
    ex P being 1-sorted st P = C.i & X.i = the carrier of P
    proof
      let i be set;
      assume i in I;
      then reconsider i as Element of I;
      take C.i;
      thus thesis by A2;
    end;
    hence thesis by PRALG_1:def 13;
  end;
end;

definition
  let R1, R2, S1, S2 be set;
  let R be Relation of R1,R2, S be Relation of S1,S2;
  defpred P[set,set] means
  ex r1, s1, r2, s2 being set st $1 = [r1,s1] & $2 = [r2,s2] &
  r1 in R1 & s1 in S1 & r2 in R2 & s2 in S2 & ([r1,r2] in R or [s1,s2] in S);
  func [^R,S^] -> Relation of [:R1,S1:],[:R2,S2:] means
  :Def2:
  for x, y being set holds [x,y] in it iff
  ex r1, s1, r2, s2 being set st x = [r1,s1] & y = [r2,s2] &
  r1 in R1 & s1 in S1 & r2 in R2 & s2 in S2 & ([r1,r2] in R or [s1,s2] in S);
  existence
  proof
    consider Q being Relation of [:R1,S1:],[:R2,S2:] such that
A1: for x, y being set holds [x,y] in Q iff x in [:R1,S1:] &
    y in [:R2,S2:] & P[x,y] from RELSET_1:sch 1;
    take Q;
    let x, y be set;
    thus [x,y] in Q implies P[x,y] by A1;
    given r1, s1, r2, s2 being set such that
A2: x = [r1,s1] and
A3: y = [r2,s2] and
A4: r1 in R1 and
A5: s1 in S1 and
A6: r2 in R2 and
A7: s2 in S2 and
A8: [r1,r2] in R or [s1,s2] in S;
A9: x in [:R1,S1:] by A2,A4,A5,ZFMISC_1:87;
    y in [:R2,S2:] by A3,A6,A7,ZFMISC_1:87;
    hence thesis by A1,A2,A3,A4,A5,A6,A7,A8,A9;
  end;
  uniqueness
  proof
    let A, B be Relation of [:R1,S1:],[:R2,S2:] such that
A10: for x, y being set holds [x,y] in A iff P[x,y]and
A11: for x, y being set holds [x,y] in B iff P[x,y];
    thus A = B from RELAT_1:sch 2(A10,A11);
  end;
end;

definition
  let R1, R2, S1, S2 be non empty set;
  let R be Relation of R1,R2, S be Relation of S1,S2;
  redefine func [^R,S^] means
  :Def3:
  for r1 being Element of R1, r2 being Element of R2
  for s1 being Element of S1, s2 being Element of S2 holds
  [[r1,s1],[r2,s2]] in it iff [r1,r2] in R or [s1,s2] in S;
  compatibility
  proof
    let f be Relation of [:R1,S1:],[:R2,S2:];
    thus f = [^R,S^] implies for r1 being Element of R1, r2 being Element of R2
    for s1 being Element of S1, s2 being Element of S2 holds
    [[r1,s1],[r2,s2]] in f iff [r1,r2] in R or [s1,s2] in S
    proof
      assume
A1:   f = [^R,S^];
      let r1 be Element of R1, r2 be Element of R2;
      let s1 be Element of S1, s2 be Element of S2;
      hereby
        assume [[r1,s1],[r2,s2]] in f;
        then consider r19, s19, r29, s29 being set such that
A2:     [r1,s1] = [r19,s19] and
A3:     [r2,s2] = [r29,s29] and
        r19 in R1 and s19 in S1
        and r29 in R2
        and s29 in S2 and
A4:     [r19,r29] in R or [s19,s29] in S by A1,Def2;
A5:     r1 = r19 by A2,XTUPLE_0:1;
        s1 = s19 by A2,XTUPLE_0:1;
        hence [r1,r2] in R or [s1,s2] in S by A3,A4,A5,XTUPLE_0:1;
      end;
      thus thesis by A1,Def2;
    end;
    assume
A6: for r1 being Element of R1, r2 being Element of R2
    for s1 being Element of S1, s2 being Element of S2 holds
    [[r1,s1],[r2,s2]] in f iff [r1,r2] in R or [s1,s2] in S;
    for x, y being set holds [x,y] in f iff [x,y] in [^R,S^]
    proof
      let x, y be set;
      thus [x,y] in f implies [x,y] in [^R,S^]
      proof
        assume
A7:     [x,y] in f;
        then x in dom f by XTUPLE_0:def 12;
        then consider x1, x2 being set such that
A8:     x1 in R1 and
A9:     x2 in S1 and
A10:    x = [x1,x2] by ZFMISC_1:def 2;
        y in rng f by A7,XTUPLE_0:def 13;
        then consider y1, y2 being set such that
A11:    y1 in R2 and
A12:    y2 in S2 and
A13:    y = [y1,y2] by ZFMISC_1:def 2;
        [x1,y1] in R or [x2,y2] in S by A6,A7,A8,A9,A10,A11,A12,A13;
        hence thesis by A8,A9,A10,A11,A12,A13,Def2;
      end;
      assume [x,y] in [^R,S^];
      then ex r1, s1, r2, s2 being set st x = [r1,s1] & y = [r2,s2] &
      r1 in R1 & s1 in S1 & r2 in R2 & s2 in S2 &
      ([r1,r2] in R or [s1,s2] in S) by Def2;
      hence thesis by A6;
    end;
    hence thesis by RELAT_1:def 2;
  end;
end;

registration
  let R1, S1 be set;
  let R be total Relation of R1;
  let S be total Relation of S1;
  cluster [^R,S^] -> total;
  coherence
  proof
    thus dom [^R,S^] c= [:R1,S1:];
    let z be set;
    assume z in [:R1,S1:];
    then consider x, y being set such that
A1: x in R1 and
A2: y in S1 and
A3: z = [x,y] by ZFMISC_1:def 2;
    dom R = R1 by PARTFUN1:def 2;
    then consider a being set such that
A4: [x,a] in R by A1,XTUPLE_0:def 12;
    dom S = S1 by PARTFUN1:def 2;
    then consider b being set such that
A5: [y,b] in S by A2,XTUPLE_0:def 12;
A6: a in R1 by A4,ZFMISC_1:87;
    b in S1 by A5,ZFMISC_1:87;
    then [[x,y],[a,b]] in [^R,S^] by A1,A2,A4,A6,Def2;
    hence thesis by A3,XTUPLE_0:def 12;
  end;
end;

registration
  let R1, S1 be set;
  let R be reflexive Relation of R1;
  let S be reflexive Relation of S1;
  cluster [^R,S^] -> reflexive;
  coherence
  proof
    let x be set;
    assume
A1: x in field [^R,S^];
A2: R is_reflexive_in field R by RELAT_2:def 9;
A3: S is_reflexive_in field S by RELAT_2:def 9;
    per cases by A1,XBOOLE_0:def 3;
    suppose x in dom [^R,S^];
      then consider y being set such that
A4:   [x,y] in [^R,S^] by XTUPLE_0:def 12;
      consider p, q, s, t being set such that
A5:   x = [p,q] and y = [s,t] and
A6:   p in R1 and
A7:   q in S1 and s in R1
      and t in S1 and
A8:   [p,s] in R or [q,t] in S by A4,Def2;
      per cases by A8;
      suppose [p,s] in R;
        then p in field R by RELAT_1:15;
        then [p,p] in R by A2,RELAT_2:def 1;
        hence thesis by A5,A6,A7,Def2;
      end;
      suppose [q,t] in S;
        then q in field S by RELAT_1:15;
        then [q,q] in S by A3,RELAT_2:def 1;
        hence thesis by A5,A6,A7,Def2;
      end;
    end;
    suppose x in rng [^R,S^];
      then consider y being set such that
A9:   [y,x] in [^R,S^] by XTUPLE_0:def 13;
      consider p, q, s, t being set such that
      y = [p,q] and
A10:  x = [s,t] and
      p in R1 and q in S1 and
A11:  s in R1 and
A12:  t in S1 and
A13:  [p,s] in R or [q,t] in S by A9,Def2;
      per cases by A13;
      suppose [p,s] in R;
        then s in field R by RELAT_1:15;
        then [s,s] in R by A2,RELAT_2:def 1;
        hence thesis by A10,A11,A12,Def2;
      end;
      suppose [q,t] in S;
        then t in field S by RELAT_1:15;
        then [t,t] in S by A3,RELAT_2:def 1;
        hence thesis by A10,A11,A12,Def2;
      end;
    end;
  end;
end;

registration
  let R1, S1 be set;
  let R be Relation of R1;
  let S be total reflexive Relation of S1;
  cluster [^R,S^] -> reflexive;
  coherence
  proof
    let x be set;
    assume x in field [^R,S^];
    then consider x1, x2 being set such that
A1: x1 in R1 and
A2: x2 in S1 and
A3: x = [x1,x2] by ZFMISC_1:def 2;
    S1 = field S by ORDERS_1:12;
    then S is_reflexive_in S1 by RELAT_2:def 9;
    then [x2,x2] in S by A2,RELAT_2:def 1;
    hence thesis by A1,A2,A3,Def3;
  end;
end;

registration
  let R1, S1 be set;
  let R be total reflexive Relation of R1;
  let S be Relation of S1;
  cluster [^R,S^] -> reflexive;
  coherence
  proof
    let x be set;
    assume x in field [^R,S^];
    then consider x1, x2 being set such that
A1: x1 in R1 and
A2: x2 in S1 and
A3: x = [x1,x2] by ZFMISC_1:def 2;
    R1 = field R by ORDERS_1:12;
    then R is_reflexive_in R1 by RELAT_2:def 9;
    then [x1,x1] in R by A1,RELAT_2:def 1;
    hence thesis by A1,A2,A3,Def3;
  end;
end;

registration
  let R1, S1 be set;
  let R be symmetric Relation of R1;
  let S be symmetric Relation of S1;
  cluster [^R,S^] -> symmetric;
  coherence
  proof
    let x, y be set;
    assume that x in field [^R,S^] and y in field [^R,S^];
    assume [x,y] in [^R,S^];
    then consider p, q, s, t being set such that
A1: x = [p,q] and
A2: y = [s,t] and
A3: p in R1 and
A4: q in S1 and
A5: s in R1 and
A6: t in S1 and
A7: [p,s] in R or [q,t] in S by Def2;
A8: R is_symmetric_in field R by RELAT_2:def 11;
A9: S is_symmetric_in field S by RELAT_2:def 11;
    per cases by A7;
    suppose
A10:  [p,s] in R;
      then
A11:  p in field R by RELAT_1:15;
      s in field R by A10,RELAT_1:15;
      then [s,p] in R by A8,A10,A11,RELAT_2:def 3;
      hence thesis by A1,A2,A3,A4,A5,A6,Def2;
    end;
    suppose
A12:  [q,t] in S;
      then
A13:  q in field S by RELAT_1:15;
      t in field S by A12,RELAT_1:15;
      then [t,q] in S by A9,A12,A13,RELAT_2:def 3;
      hence thesis by A1,A2,A3,A4,A5,A6,Def2;
    end;
  end;
end;

begin :: Relational Structures

registration
  cluster empty -> total for RelStr;
  coherence
  proof
    let P be RelStr;
    assume the carrier of P is empty;
    hence dom the InternalRel of P = the carrier of P;
  end;
end;

definition
  let R be Relation;
  attr R is transitive-yielding means
  :Def4:
  for S being RelStr st S in rng R holds S is transitive;
end;

registration
  cluster Poset-yielding -> transitive-yielding for Relation;
  coherence
  proof
    let R be Relation;
    assume
A1: R is Poset-yielding;
    let S be RelStr;
    thus thesis by A1,YELLOW16:def 5;
  end;
end;

registration
  cluster Poset-yielding for Function;
  existence
  proof
    set f = the Poset-yielding ManySortedSet of 0;
    take f;
    thus thesis;
  end;
end;

registration
  let I be set;
  cluster Poset-yielding for ManySortedSet of I;
  existence
  proof
    set f = the Poset-yielding ManySortedSet of I;
    take f;
    thus thesis;
  end;
end;

definition
  let I be set, C be RelStr-yielding ManySortedSet of I;
  func pcs-InternalRels C -> ManySortedSet of I means
  :Def5:
  for i being set st i in I
  ex P being RelStr st P = C.i & it.i = the InternalRel of P;
  existence
  proof
    defpred P[set,set] means
    ex R being RelStr st R = C.$1 & $2 = the InternalRel of R;
A1: for i being set st i in I ex j being set st P[i,j]
    proof
      let i be set;
      assume
A2:   i in I;
      then reconsider I as non empty set;
      reconsider B = C as RelStr-yielding ManySortedSet of I;
      reconsider i9 = i as Element of I by A2;
      take the InternalRel of B.i9, B.i9;
      thus thesis;
    end;
    consider M being Function such that
A3: dom M = I and
A4: for i being set st i in I holds P[i,M.i] from CLASSES1:sch 1(A1);
    M is ManySortedSet of I by A3,PARTFUN1:def 2,RELAT_1:def 18;
    hence thesis by A4;
  end;
  uniqueness
  proof
    let X, Y be ManySortedSet of I such that
A5: for j being set st j in I
    ex R being RelStr st R = C.j & X.j = the InternalRel of R and
A6: for j being set st j in I
    ex R being RelStr st R = C.j & Y.j = the InternalRel of R;
    for i being set st i in I holds X.i = Y.i
    proof
      let i be set;
      assume
A7:   i in I;
      then
A8:   ex R being RelStr st R = C.i & X.i = the InternalRel of R by A5;
      ex R being RelStr st R = C.i & Y.i = the InternalRel of R by A6,A7;
      hence thesis by A8;
    end;
    hence thesis by PBOOLE:3;
  end;
end;

definition
  let I be non empty set, C be RelStr-yielding ManySortedSet of I;
  redefine func pcs-InternalRels C means
  :Def6:
  for i being Element of I holds it.i = the InternalRel of C.i;
  compatibility
  proof
    let X be ManySortedSet of I;
    thus X = pcs-InternalRels C implies
    for i being Element of I holds X.i = the InternalRel of C.i
    proof
      assume
A1:   X = pcs-InternalRels C;
      let i be Element of I;
      ex P being RelStr st P = C.i & X.i = the InternalRel of P by A1,Def5;
      hence thesis;
    end;
    assume
A2: for i being Element of I holds X.i = the InternalRel of C.i;
    for i being set st i in I
    ex P being RelStr st P = C.i & X.i = the InternalRel of P
    proof
      let i be set;
      assume i in I;
      then reconsider i as Element of I;
      take C.i;
      thus thesis by A2;
    end;
    hence thesis by Def5;
  end;
end;

registration
  let I be set, C be RelStr-yielding ManySortedSet of I;
  cluster pcs-InternalRels C -> Relation-yielding;
  coherence
  proof
    set IR = pcs-InternalRels C;
    let i be set;
    assume i in dom IR;
    then ex P being RelStr st P = C.i & IR.i = the InternalRel of P by Def5;
    hence thesis;
  end;
end;

registration
  let I be non empty set;
  let C be transitive-yielding RelStr-yielding ManySortedSet of I;
  let i be Element of I;
  cluster C.i -> transitive for RelStr;
  coherence
  proof
    dom C = I by PARTFUN1:def 2;
    then C.i in rng C by FUNCT_1:3;
    hence thesis by Def4;
  end;
end;

begin :: Tolerance Structures

definition
  struct (1-sorted) TolStr (# carrier -> set,
    ToleranceRel -> Relation of the carrier #);
end;

definition
  let P be TolStr;
  let p, q be Element of P;
  pred p (--) q means
  :Def7:
  [p,q] in the ToleranceRel of P;
end;

definition
  let P be TolStr;
  attr P is pcs-tol-total means
  :Def8:
  the ToleranceRel of P is total;
  attr P is pcs-tol-reflexive means
  :Def9:
  the ToleranceRel of P is_reflexive_in the carrier of P;
  attr P is pcs-tol-irreflexive means
  :Def10:
  the ToleranceRel of P is_irreflexive_in the carrier of P;
  attr P is pcs-tol-symmetric means
  :Def11:
  the ToleranceRel of P is_symmetric_in the carrier of P;
end;

definition
  func emptyTolStr -> TolStr equals
  TolStr (# {}, {}({},{}) #);
  coherence;
end;

registration
  cluster emptyTolStr -> empty strict;
  coherence;
end;

theorem Th2:
  for P being TolStr st P is empty holds the TolStr of P = emptyTolStr
proof
  let P be TolStr;
  assume P is empty;
  then the carrier of P = {};
  hence thesis;
end;

registration
  cluster pcs-tol-reflexive -> pcs-tol-total for TolStr;
  coherence
  proof
    let P be TolStr;
    assume P is pcs-tol-reflexive;
    then the ToleranceRel of P is_reflexive_in the carrier of P by Def9;
    then dom the ToleranceRel of P = the carrier of P by ORDERS_1:13;
    hence the ToleranceRel of P is total by PARTFUN1:def 2;
  end;
end;

registration
  cluster empty -> pcs-tol-reflexive pcs-tol-irreflexive pcs-tol-symmetric
    for TolStr;
  coherence
  proof
    let P be TolStr;
    assume
A1: P is empty;
    then the TolStr of P = emptyTolStr by Th2;
    then
A2: the carrier of P = field the ToleranceRel of P;
    hence the ToleranceRel of P is_reflexive_in the carrier of P
    by A1,RELAT_2:def 9;
    thus the ToleranceRel of P is_irreflexive_in the carrier of P
    by A1,A2,RELAT_2:def 10;
    thus the ToleranceRel of P is_symmetric_in the carrier of P
    by A1,A2,RELAT_2:def 11;
  end;
end;

registration
  cluster empty strict for TolStr;
  existence
  proof
    take emptyTolStr;
    thus thesis;
  end;
end;

registration
  let P be pcs-tol-total TolStr;
  cluster the ToleranceRel of P -> total;
  coherence by Def8;
end;

registration
  let P be pcs-tol-reflexive TolStr;
  cluster the ToleranceRel of P -> reflexive;
  coherence
  proof
    set TR = the ToleranceRel of P;
A1: field TR = the carrier of P by ORDERS_1:12;
    TR is_reflexive_in the carrier of P by Def9;
    hence thesis by A1,RELAT_2:def 9;
  end;
end;

registration
  let P be pcs-tol-irreflexive TolStr;
  cluster the ToleranceRel of P -> irreflexive;
  coherence
  proof
    set TR = the ToleranceRel of P;
A1: TR is_irreflexive_in the carrier of P by Def10;
    let x be set;
    assume x in field TR;
    assume
A2: [x,x] in TR;
    then x in dom TR by XTUPLE_0:def 12;
    hence thesis by A1,A2,RELAT_2:def 2;
  end;
end;

registration
  let P be pcs-tol-symmetric TolStr;
  cluster the ToleranceRel of P -> symmetric;
  coherence
  proof
    set TR = the ToleranceRel of P;
A1: TR is_symmetric_in the carrier of P by Def11;
    let x, y be set;
    assume that x in field TR and y in field TR;
    assume
A2: [x,y] in TR;
    then
A3: x in dom TR by XTUPLE_0:def 12;
    y in rng TR by A2,XTUPLE_0:def 13;
    hence thesis by A1,A2,A3,RELAT_2:def 3;
  end;
end;

registration
  let L be pcs-tol-total TolStr;
  cluster the TolStr of L -> pcs-tol-total;
  coherence by Def8;
end;

definition
  let P be pcs-tol-symmetric TolStr;
  let p, q be Element of P;
  redefine pred p (--) q;
  symmetry
  proof
    let x, y be Element of P;
    assume
A1: [x,y] in the ToleranceRel of P;
    then
A2: x in the carrier of P by ZFMISC_1:87;
    the ToleranceRel of P is_symmetric_in the carrier of P by Def11;
    hence [y,x] in the ToleranceRel of P by A1,A2,RELAT_2:def 3;
  end;
end;

registration
  let D be set;
  cluster TolStr(#D,nabla D#) -> pcs-tol-reflexive pcs-tol-symmetric;
  coherence
  proof
    set P = TolStr(#D,nabla D#);
    set TR = the ToleranceRel of P;
A1: field TR = the carrier of P by ORDERS_1:12;
    hence TR is_reflexive_in the carrier of P by RELAT_2:def 9;
    thus TR is_symmetric_in the carrier of P by A1,RELAT_2:def 11;
  end;
end;

registration
  let D be set;
  cluster TolStr(#D,{}(D,D)#) -> pcs-tol-irreflexive pcs-tol-symmetric;
  coherence
  proof
    set P = TolStr(#D,{}(D,D)#);
    thus the ToleranceRel of P is_irreflexive_in the carrier of P
    proof
      let x be set;
      thus thesis;
    end;
    let x be set;
    thus thesis;
  end;
end;

registration
  cluster strict non empty pcs-tol-reflexive pcs-tol-symmetric for TolStr;
  existence
  proof
    take P = TolStr(#{{}},nabla {{}}#);
    thus P is strict;
    thus the carrier of P is non empty;
    thus thesis;
  end;
end;

registration
  cluster strict non empty pcs-tol-irreflexive pcs-tol-symmetric for TolStr;
  existence
  proof
    take P = TolStr(#{{}},{}({{}},{{}})#);
    thus P is strict;
    thus the carrier of P is non empty;
    thus thesis;
  end;
end;

definition
  let R be Relation;
  attr R is TolStr-yielding means
  :Def13:
  for P being set st P in rng R holds P is TolStr;
end;

definition
  let f be Function;
  redefine attr f is TolStr-yielding means
  :Def14:
  for x being set st x in dom f holds f.x is TolStr;
  compatibility
  proof
    hereby
      assume
A1:   f is TolStr-yielding;
      let x be set;
      assume x in dom f;
      then f.x in rng f by FUNCT_1:3;
      hence f.x is TolStr by A1,Def13;
    end;
    assume
A2: for x being set st x in dom f holds f.x is TolStr;
    let P be set;
    assume P in rng f;
    then ex x being set st x in dom f & f.x = P by FUNCT_1:def 3;
    hence thesis by A2;
  end;
end;

definition
  let I be set, f be ManySortedSet of I;
A1: dom f = I by PARTFUN1:def 2;
  redefine attr f is TolStr-yielding means
  for x being set st x in I holds f.x is TolStr;
  compatibility by A1,Def14;
end;

definition
  let R be Relation;
  attr R is pcs-tol-reflexive-yielding means
  :Def16:
  for S being TolStr st S in rng R holds S is pcs-tol-reflexive;
  attr R is pcs-tol-irreflexive-yielding means
  :Def17:
  for S being TolStr st S in rng R holds S is pcs-tol-irreflexive;
  attr R is pcs-tol-symmetric-yielding means
  :Def18:
  for S being TolStr st S in rng R holds S is pcs-tol-symmetric;
end;

registration
  cluster empty -> pcs-tol-reflexive-yielding pcs-tol-irreflexive-yielding
    pcs-tol-symmetric-yielding for Relation;
  coherence
  proof
    let f be Relation;
    assume
A1: f is empty;
    thus f is pcs-tol-reflexive-yielding
    proof
      let i be set;
      thus thesis by A1;
    end;
    thus f is pcs-tol-irreflexive-yielding
    proof
      let i be set;
      thus thesis by A1;
    end;
    let i be set;
    thus thesis by A1;
  end;
end;

registration
  let I be set, P be TolStr;
  cluster I --> P -> TolStr-yielding for ManySortedSet of I;
  coherence
  proof
    I --> P is TolStr-yielding
    proof
      let i be set;
      thus thesis by FUNCOP_1:7;
    end;
    hence thesis;
  end;
end;

registration
  let I be set, P be pcs-tol-reflexive TolStr;
  cluster I --> P -> pcs-tol-reflexive-yielding for ManySortedSet of I;
  coherence
  proof
    set f = I --> P;
    f is pcs-tol-reflexive-yielding
    proof
      let S be TolStr;
      assume S in rng f;
      hence thesis by TARSKI:def 1;
    end;
    hence thesis;
  end;
end;

registration
  let I be set, P be pcs-tol-irreflexive TolStr;
  cluster I --> P -> pcs-tol-irreflexive-yielding for ManySortedSet of I;
  coherence
  proof
    set f = I --> P;
    f is pcs-tol-irreflexive-yielding
    proof
      let S be TolStr;
      assume S in rng f;
      hence thesis by TARSKI:def 1;
    end;
    hence thesis;
  end;
end;

registration
  let I be set, P be pcs-tol-symmetric TolStr;
  cluster I --> P -> pcs-tol-symmetric-yielding for ManySortedSet of I;
  coherence
  proof
    set f = I --> P;
    f is pcs-tol-symmetric-yielding
    proof
      let S be TolStr;
      assume S in rng f;
      hence thesis by TARSKI:def 1;
    end;
    hence thesis;
  end;
end;

registration
  cluster TolStr-yielding -> 1-sorted-yielding for Function;
  coherence
  proof
    let f be Function;
    assume
A1: f is TolStr-yielding;
    let x be set;
    thus thesis by A1,Def14;
  end;
end;

registration
  let I be set;
  cluster pcs-tol-reflexive-yielding pcs-tol-symmetric-yielding TolStr-yielding
    for ManySortedSet of I;
  existence
  proof
    take I --> TolStr(#0,nabla 0#);
    thus thesis;
  end;
end;

registration
  let I be set;
  cluster pcs-tol-irreflexive-yielding pcs-tol-symmetric-yielding
    TolStr-yielding for ManySortedSet of I;
  existence
  proof
    take I --> TolStr(#0,{}(0,0)#);
    thus thesis;
  end;
end;

registration
  let I be set;
  cluster TolStr-yielding for ManySortedSet of I;
  existence
  proof
    set R = the TolStr;
    take I --> R;
    thus thesis;
  end;
end;

definition
  let I be non empty set, C be TolStr-yielding ManySortedSet of I,
  i be Element of I;
  redefine func C.i -> TolStr;
  coherence
  proof
    dom C = I by PARTFUN1:def 2;
    hence thesis by Def14;
  end;
end;

definition
  let I be set, C be TolStr-yielding ManySortedSet of I;
  func pcs-ToleranceRels C -> ManySortedSet of I means
  :Def19:
  for i being set st i in I
  ex P being TolStr st P = C.i & it.i = the ToleranceRel of P;
  existence
  proof
    defpred P[set,set] means
    ex R being TolStr st R = C.$1 & $2 = the ToleranceRel of R;
A1: for i being set st i in I ex j being set st P[i,j]
    proof
      let i be set;
      assume
A2:   i in I;
      then reconsider I as non empty set;
      reconsider B = C as TolStr-yielding ManySortedSet of I;
      reconsider i9 = i as Element of I by A2;
      take the ToleranceRel of B.i9, B.i9;
      thus thesis;
    end;
    consider M being Function such that
A3: dom M = I and
A4: for i being set st i in I holds P[i,M.i] from CLASSES1:sch 1(A1);
    M is ManySortedSet of I by A3,PARTFUN1:def 2,RELAT_1:def 18;
    hence thesis by A4;
  end;
  uniqueness
  proof
    let X, Y be ManySortedSet of I such that
A5: for j being set st j in I
    ex R being TolStr st R = C.j & X.j = the ToleranceRel of R and
A6: for j being set st j in I
    ex R being TolStr st R = C.j & Y.j = the ToleranceRel of R;
    for i being set st i in I holds X.i = Y.i
    proof
      let i be set;
      assume
A7:   i in I;
      then
A8:   ex R being TolStr st R = C.i & X.i = the ToleranceRel of R by A5;
      ex R being TolStr st R = C.i & Y.i = the ToleranceRel of R by A6,A7;
      hence thesis by A8;
    end;
    hence thesis by PBOOLE:3;
  end;
end;

definition
  let I be non empty set, C be TolStr-yielding ManySortedSet of I;
  redefine func pcs-ToleranceRels C means
  :Def20:
  for i being Element of I holds it.i = the ToleranceRel of C.i;
  compatibility
  proof
    let X be ManySortedSet of I;
    thus X = pcs-ToleranceRels C implies
    for i being Element of I holds X.i = the ToleranceRel of C.i
    proof
      assume
A1:   X = pcs-ToleranceRels C;
      let i be Element of I;
      ex P being TolStr st P = C.i & X.i = the ToleranceRel of P by A1,Def19;
      hence thesis;
    end;
    assume
A2: for i being Element of I holds X.i = the ToleranceRel of C.i;
    for i being set st i in I
    ex P being TolStr st P = C.i & X.i = the ToleranceRel of P
    proof
      let i be set;
      assume i in I;
      then reconsider i as Element of I;
      take C.i;
      thus thesis by A2;
    end;
    hence thesis by Def19;
  end;
end;

registration
  let I be set, C be TolStr-yielding ManySortedSet of I;
  cluster pcs-ToleranceRels C -> Relation-yielding;
  coherence
  proof
    set TR = pcs-ToleranceRels C;
    let i be set;
    assume i in dom TR;
    then ex P being TolStr st P = C.i & TR.i = the ToleranceRel of P
    by Def19;
    hence thesis;
  end;
end;

registration
  let I be non empty set;
  let C be pcs-tol-reflexive-yielding TolStr-yielding ManySortedSet of I;
  let i be Element of I;
  cluster C.i -> pcs-tol-reflexive for TolStr;
  coherence
  proof
    dom C = I by PARTFUN1:def 2;
    then C.i in rng C by FUNCT_1:3;
    hence thesis by Def16;
  end;
end;

registration
  let I be non empty set;
  let C be pcs-tol-irreflexive-yielding TolStr-yielding ManySortedSet of I;
  let i be Element of I;
  cluster C.i -> pcs-tol-irreflexive for TolStr;
  coherence
  proof
    dom C = I by PARTFUN1:def 2;
    then C.i in rng C by FUNCT_1:3;
    hence thesis by Def17;
  end;
end;

registration
  let I be non empty set;
  let C be pcs-tol-symmetric-yielding TolStr-yielding ManySortedSet of I;
  let i be Element of I;
  cluster C.i -> pcs-tol-symmetric for TolStr;
  coherence
  proof
    dom C = I by PARTFUN1:def 2;
    then C.i in rng C by FUNCT_1:3;
    hence thesis by Def18;
  end;
end;

theorem Th3:
  for P, Q being TolStr st the TolStr of P = the TolStr of Q &
  P is pcs-tol-reflexive holds Q is pcs-tol-reflexive
proof
  let P, Q be TolStr;
  assume that
A1: the TolStr of P = the TolStr of Q and
A2: the ToleranceRel of P is_reflexive_in the carrier of P;
  let x be set;
  assume x in the carrier of Q;
  hence thesis by A1,A2,RELAT_2:def 1;
end;

theorem Th4:
  for P, Q being TolStr st the TolStr of P = the TolStr of Q &
  P is pcs-tol-irreflexive holds Q is pcs-tol-irreflexive
proof
  let P, Q be TolStr;
  assume that
A1: the TolStr of P = the TolStr of Q and
A2: the ToleranceRel of P is_irreflexive_in the carrier of P;
  let x be set;
  assume x in the carrier of Q;
  hence thesis by A1,A2,RELAT_2:def 2;
end;

theorem Th5:
  for P, Q being TolStr st the TolStr of P = the TolStr of Q &
  P is pcs-tol-symmetric holds Q is pcs-tol-symmetric
proof
  let P, Q be TolStr;
  assume that
A1: the TolStr of P = the TolStr of Q and
A2: the ToleranceRel of P is_symmetric_in the carrier of P;
  let x, y be set;
  assume x in the carrier of Q;
  hence thesis by A1,A2,RELAT_2:def 3;
end;

definition
  let P, Q be TolStr;
  func [^P,Q^] -> TolStr equals
  TolStr (# [: the carrier of P, the carrier of Q :],
    [^ the ToleranceRel of P, the ToleranceRel of Q ^] #);
  coherence;
end;

notation
  let P, Q be TolStr, p be Element of P, q be Element of Q;
  synonym [^p,q^] for [p,q];
end;

definition
  let P, Q be non empty TolStr, p be Element of P, q be Element of Q;
  redefine func [^p,q^] -> Element of [^P,Q^];
  coherence
  proof
    [p,q] is Element of [^P,Q^];
    hence thesis;
  end;
end;

notation
  let P, Q be TolStr, p be Element of [^P,Q^];
  synonym p^`1 for p`1;
  synonym p^`2 for p`2;
end;

definition
  let P, Q be non empty TolStr, p be Element of [^P,Q^];
  redefine func p^`1 -> Element of P;
  coherence by MCART_1:10;
  redefine func p^`2 -> Element of Q;
  coherence by MCART_1:10;
end;

theorem Th6:
  for S1, S2 being non empty TolStr
  for a, c being Element of S1, b, d being Element of S2 holds
  [^a,b^] (--) [^c,d^] iff a (--) c or b (--) d
proof
  let S1, S2 be non empty TolStr, a, c be Element of S1,
  b, d be Element of S2;
  set I1 = the ToleranceRel of S1, I2 = the ToleranceRel of S2,
  x = [[a,b],[c,d]];
  thus [^a,b^] (--) [^c,d^] implies a (--) c or b (--) d
  proof
    assume [^a,b^] (--) [^c,d^];
    then x in the ToleranceRel of [^S1,S2^] by Def7;
    then [a,c] in I1 or [b,d] in I2 by Def3;
    hence thesis by Def7;
  end;
  assume a (--) c or b (--) d;
  then [x`1`1,x`2`1] in I1 or [x`1`2,x`2`2] in I2 by Def7;
  hence [[a,b],[c,d]] in the ToleranceRel of [^S1,S2^] by Def3;
end;

theorem
  for S1, S2 being non empty TolStr, x, y being Element of [^S1,S2^] holds
  x (--) y iff x^`1 (--) y^`1 or x^`2 (--) y^`2
proof
  let S1, S2 be non empty TolStr, x, y be Element of [^S1,S2^];
A1: ex a, b being set st a in the carrier of S1 & b in the carrier of S2 &
  x = [a,b] by ZFMISC_1:def 2;
A2: ex c, d being set st c in the carrier of S1 & d in the carrier of S2 &
  y = [c,d] by ZFMISC_1:def 2;
A3: x = [x^`1,x^`2] by A1,MCART_1:8;
  y = [y^`1,y^`2] by A2,MCART_1:8;
  hence thesis by A3,Th6;
end;

registration
  let P be TolStr, Q be pcs-tol-reflexive TolStr;
  cluster [^P,Q^] -> pcs-tol-reflexive;
  coherence
  proof
    let x be set;
    assume x in the carrier of [^P,Q^];
    then consider x1, x2 being set such that
A1: x1 in the carrier of P and
A2: x2 in the carrier of Q and
A3: x = [x1,x2] by ZFMISC_1:def 2;
    reconsider D2 = the carrier of Q as non empty set by A2;
    reconsider TQ = the ToleranceRel of Q as Relation of D2;
    D2 = field TQ by ORDERS_1:12;
    then TQ is_reflexive_in D2 by RELAT_2:def 9;
    then [x2,x2] in TQ by A2,RELAT_2:def 1;
    hence thesis by A1,A2,A3,Def3;
  end;
end;

registration
  let P be pcs-tol-reflexive TolStr, Q be TolStr;
  cluster [^P,Q^] -> pcs-tol-reflexive;
  coherence
  proof
    let x be set;
    assume x in the carrier of [^P,Q^];
    then consider x1, x2 being set such that
A1: x1 in the carrier of P and
A2: x2 in the carrier of Q and
A3: x = [x1,x2] by ZFMISC_1:def 2;
    reconsider D1 = the carrier of P as non empty set by A1;
    reconsider TP = the ToleranceRel of P as Relation of D1;
    D1 = field TP by ORDERS_1:12;
    then TP is_reflexive_in D1 by RELAT_2:def 9;
    then [x1,x1] in TP by A1,RELAT_2:def 1;
    hence thesis by A1,A2,A3,Def3;
  end;
end;

registration
  let P, Q be pcs-tol-symmetric TolStr;
  cluster [^P,Q^] -> pcs-tol-symmetric;
  coherence
  proof
    set R = [^P,Q^];
    set TR = the ToleranceRel of R;
A1: TR is_symmetric_in field TR by RELAT_2:def 11;
    let x, y be set;
    assume that x in the carrier of R and y in the carrier of R;
    assume
A2: [x,y] in TR;
    then
A3: x in field TR by RELAT_1:15;
    y in field TR by A2,RELAT_1:15;
    hence thesis by A1,A2,A3,RELAT_2:def 3;
  end;
end;

begin :: PCS's

definition
  struct (RelStr,TolStr) pcs-Str (# carrier -> set,
    InternalRel -> (Relation of the carrier),
    ToleranceRel -> Relation of the carrier #);
end;

definition
  let P be pcs-Str;
  attr P is pcs-compatible means
  :Def22:
  for p, p9, q, q9 being Element of P st
  p (--) q & p9 <= p & q9 <= q holds p9 (--) q9;
end;

definition
  let P be pcs-Str;
  attr P is pcs-like means
  :Def23:
  P is reflexive transitive pcs-tol-reflexive pcs-tol-symmetric pcs-compatible;
  attr P is anti-pcs-like means
  :Def24:
  P is reflexive transitive pcs-tol-irreflexive pcs-tol-symmetric
  pcs-compatible;
end;

registration
  cluster pcs-like -> reflexive transitive pcs-tol-reflexive pcs-tol-symmetric
    pcs-compatible for pcs-Str;
  coherence by Def23;
  cluster reflexive transitive pcs-tol-reflexive pcs-tol-symmetric
    pcs-compatible -> pcs-like for pcs-Str;
  coherence by Def23;
  cluster anti-pcs-like -> reflexive transitive pcs-tol-irreflexive
    pcs-tol-symmetric pcs-compatible for pcs-Str;
  coherence by Def24;
  cluster reflexive transitive pcs-tol-irreflexive pcs-tol-symmetric
    pcs-compatible -> anti-pcs-like for pcs-Str;
  coherence by Def24;
end;

definition
  let D be set;
  func pcs-total D -> pcs-Str equals
  pcs-Str (# D,nabla D,nabla D #);
  coherence;
end;

registration
  let D be set;
  cluster pcs-total D -> strict;
  coherence;
end;

registration
  let D be non empty set;
  cluster pcs-total D -> non empty;
  coherence;
end;

registration
  let D be set;
  cluster pcs-total D -> reflexive transitive
    pcs-tol-reflexive pcs-tol-symmetric;
  coherence
  proof
    set P = pcs-total D;
    set IR = the InternalRel of P;
    set TR = the ToleranceRel of P;
A1: field IR = the carrier of P by ORDERS_1:12;
    hence IR is_reflexive_in the carrier of P by RELAT_2:def 9;
    thus IR is_transitive_in the carrier of P by A1,RELAT_2:def 16;
    thus TR is_reflexive_in the carrier of P by A1,RELAT_2:def 9;
    thus TR is_symmetric_in the carrier of P by A1,RELAT_2:def 11;
  end;
end;

registration
  let D be set;
  cluster pcs-total D -> pcs-like;
  coherence
  proof
    set P = pcs-total D;
    thus P is reflexive transitive;
    thus P is pcs-tol-reflexive pcs-tol-symmetric;
    let p, p9, q, q9 be Element of P such that p (--) q;
    assume that
A1: p9 <= p and q9 <= q;
    [p9,p] in [:D,D:] by A1,ORDERS_2:def 5;
    then p9 in the carrier of P by ZFMISC_1:87;
    hence [p9,q9] in the ToleranceRel of P by ZFMISC_1:87;
  end;
end;

registration
  let D be set;
  cluster pcs-Str(#D,nabla D,{}(D,D)#) -> anti-pcs-like;
  coherence
  proof
    set P = pcs-Str(#D,nabla D,{}(D,D)#);
A1: the RelStr of P = the RelStr of RelStr(#D,nabla D#);
    hence P is reflexive by WAYBEL_8:12;
    thus P is transitive by A1,WAYBEL_8:13;
A2: the TolStr of P = the TolStr of TolStr(#D,{}(D,D)#);
    hence P is pcs-tol-irreflexive by Th4;
    thus P is pcs-tol-symmetric by A2,Th5;
    let p be Element of P;
    thus thesis by Def7;
  end;
end;

registration
  cluster strict non empty pcs-like for pcs-Str;
  existence
  proof
    take P = pcs-total {{}};
    thus P is strict;
    thus the carrier of P is non empty;
    thus thesis;
  end;
  cluster strict non empty anti-pcs-like for pcs-Str;
  existence
  proof
    take P = pcs-Str(#{{}},nabla {{}},{}({{}},{{}})#);
    thus P is strict;
    thus the carrier of P is non empty;
    thus thesis;
  end;
end;

definition
  mode pcs is pcs-like pcs-Str;
  mode anti-pcs is anti-pcs-like pcs-Str;
end;

definition
  func pcs-empty -> pcs-Str equals
  pcs-total 0;
  coherence;
end;

registration
  cluster pcs-empty -> strict empty pcs-like;
  coherence;
end;

definition
  let p be set;
  func pcs-singleton p -> pcs-Str equals
  pcs-total {p};
  coherence;
end;

registration
  let p be set;
  cluster pcs-singleton p -> strict non empty pcs-like;
  coherence;
end;

definition
  let R be Relation;
  attr R is pcs-Str-yielding means
  :Def28:
  for P being set st P in rng R holds P is pcs-Str;
  attr R is pcs-yielding means
  :Def29:
  for P being set st P in rng R holds P is pcs;
end;

definition
  let f be Function;
  redefine attr f is pcs-Str-yielding means
  :Def30:
  for x being set st x in dom f holds f.x is pcs-Str;
  compatibility
  proof
    hereby
      assume
A1:   f is pcs-Str-yielding;
      let x be set;
      assume x in dom f;
      then f.x in rng f by FUNCT_1:3;
      hence f.x is pcs-Str by A1,Def28;
    end;
    assume
A2: for x being set st x in dom f holds f.x is pcs-Str;
    let P be set;
    assume P in rng f;
    then ex x being set st x in dom f & f.x = P by FUNCT_1:def 3;
    hence thesis by A2;
  end;
  redefine attr f is pcs-yielding means
  :Def31:
  for x being set st x in dom f holds f.x is pcs;
  compatibility
  proof
    hereby
      assume
A3:   f is pcs-yielding;
      let x be set;
      assume x in dom f;
      then f.x in rng f by FUNCT_1:3;
      hence f.x is pcs by A3,Def29;
    end;
    assume
A4: for x being set st x in dom f holds f.x is pcs;
    let P be set;
    assume P in rng f;
    then ex x being set st x in dom f & f.x = P by FUNCT_1:def 3;
    hence thesis by A4;
  end;
end;

definition
  let I be set, f be ManySortedSet of I;
A1: dom f = I by PARTFUN1:def 2;
  redefine attr f is pcs-Str-yielding means
  :Def32:
  for x being set st x in I holds f.x is pcs-Str;
  compatibility by A1,Def30;
  redefine attr f is pcs-yielding means
  :Def33:
  for x being set st x in I holds f.x is pcs;
  compatibility by A1,Def31;
end;

registration
  cluster pcs-Str-yielding -> TolStr-yielding RelStr-yielding for Relation;
  coherence
  proof
    let f be Relation;
    assume
A1: f is pcs-Str-yielding;
    thus f is TolStr-yielding
    proof
      let y be set;
      thus thesis by A1,Def28;
    end;
    let y be set;
    thus thesis by A1,Def28;
  end;
  cluster pcs-yielding -> pcs-Str-yielding for Relation;
  coherence
  proof
    let f be Relation;
    assume
A2: f is pcs-yielding;
    let y be set;
    thus thesis by A2,Def29;
  end;
  cluster pcs-yielding -> reflexive-yielding transitive-yielding
    pcs-tol-reflexive-yielding pcs-tol-symmetric-yielding for Relation;
  coherence
  proof
    let f be Relation;
    assume
A3: f is pcs-yielding;
    thus f is reflexive-yielding
    proof
      let y be RelStr;
      thus thesis by A3,Def29;
    end;
    thus f is transitive-yielding
    proof
      let y be RelStr;
      thus thesis by A3,Def29;
    end;
    thus f is pcs-tol-reflexive-yielding
    proof
      let y be TolStr;
      thus thesis by A3,Def29;
    end;
    let y be TolStr;
    thus thesis by A3,Def29;
  end;
end;

registration
  let I be set, P be pcs;
  cluster I --> P -> pcs-yielding for ManySortedSet of I;
  coherence
  proof
    I --> P is pcs-yielding
    proof
      let i be set;
      thus thesis by FUNCOP_1:7;
    end;
    hence thesis;
  end;
end;

registration
  let I be set;
  cluster pcs-yielding for ManySortedSet of I;
  existence
  proof
    take I --> pcs-empty;
    thus thesis;
  end;
end;

definition
  let I be non empty set, C be pcs-Str-yielding ManySortedSet of I,
  i be Element of I;
  redefine func C.i -> pcs-Str;
  coherence by Def32;
end;

definition
  let I be non empty set, C be pcs-yielding ManySortedSet of I,
  i be Element of I;
  redefine func C.i -> pcs;
  coherence by Def33;
end;

:: Union of PCS's

definition
  let P, Q be pcs-Str;
  pred P c= Q means
  :Def34:
  the carrier of P c= the carrier of Q &
  the InternalRel of P c= the InternalRel of Q &
  the ToleranceRel of P c= the ToleranceRel of Q;
  reflexivity;
end;

theorem Th8:
  for P, Q being RelStr
  for p, q being Element of P, p1, q1 being Element of Q st
  the InternalRel of P c= the InternalRel of Q & p = p1 & q = q1 & p <= q
  holds p1 <= q1
proof
  let P, Q be RelStr;
  let p, q be Element of P, p1, q1 be Element of Q;
  assume that
A1: the InternalRel of P c= the InternalRel of Q and
A2: p = p1 and
A3: q = q1 and
A4: [p,q] in the InternalRel of P;
  thus [p1,q1] in the InternalRel of Q by A1,A2,A3,A4;
end;

theorem Th9:
  for P, Q being TolStr
  for p, q being Element of P, p1, q1 being Element of Q st
  the ToleranceRel of P c= the ToleranceRel of Q & p = p1 & q = q1 & p (--) q
  holds p1 (--) q1
proof
  let P, Q be TolStr;
  let p, q be Element of P, p1, q1 be Element of Q;
  assume that
A1: the ToleranceRel of P c= the ToleranceRel of Q and
A2: p = p1 and
A3: q = q1 and
A4: [p,q] in the ToleranceRel of P;
  thus [p1,q1] in the ToleranceRel of Q by A1,A2,A3,A4;
end;

Lm2: for P, Q being pcs-Str
for p being set st p in the carrier of P & P c= Q holds p is Element of Q
proof
  let P, Q be pcs-Str;
  let p be set such that
A1: p in the carrier of P;
  assume P c= Q;
  then the carrier of P c= the carrier of Q by Def34;
  hence thesis by A1;
end;

definition
  let C be Relation;
  attr C is pcs-chain-like means
  :Def35:
  for P, Q being pcs-Str st P in rng C & Q in rng C holds P c= Q or Q c= P;
end;

registration
  let I be set, P be pcs-Str;
  cluster I --> P -> pcs-chain-like for ManySortedSet of I;
  coherence
  proof
    set f = I --> P;
    f is pcs-chain-like
    proof
      let R, S be pcs-Str;
      assume that
A1:   R in rng f and
A2:   S in rng f;
      P = R & P = S or rng f = {} by A1,A2,TARSKI:def 1;
      hence thesis by A1;
    end;
    hence thesis;
  end;
end;

registration
  cluster pcs-chain-like pcs-yielding for Function;
  existence
  proof
    set P = the pcs;
    take 0 --> P;
    thus thesis;
  end;
end;

registration
  let I be set;
  cluster pcs-chain-like pcs-yielding for ManySortedSet of I;
  existence
  proof
    set P = the pcs;
    take I --> P;
    thus thesis;
  end;
end;

definition
  let I be set;
  mode pcs-Chain of I is pcs-chain-like pcs-yielding ManySortedSet of I;
end;

definition
  let I be set, C be pcs-Str-yielding ManySortedSet of I;
  func pcs-union C -> strict pcs-Str means
  :Def36:
  the carrier of it = Union Carrier C &
  the InternalRel of it = Union pcs-InternalRels C &
  the ToleranceRel of it = Union pcs-ToleranceRels C;
  existence
  proof
    set CA = Carrier C;
    set IRA = pcs-InternalRels C;
    set TRA = pcs-ToleranceRels C;
    set D = Union CA;
    set IR = Union IRA;
    set TR = Union TRA;
A1: dom CA = I by PARTFUN1:def 2;
    IR c= [:D,D:]
    proof
      let x be set;
      assume x in IR;
      then consider P being set such that
A2:   x in P and
A3:   P in rng IRA by TARSKI:def 4;
      consider i being set such that
A4:   i in dom IRA and
A5:   IRA.i = P by A3,FUNCT_1:def 3;
      consider R being RelStr such that
A6:   R = C.i and
A7:   IRA.i = the InternalRel of R by A4,Def5;
      consider x1, x2 being set such that
A8:   x = [x1,x2] and
A9:  x1 in the carrier of R and
A10:  x2 in the carrier of R by A2,A5,A7,RELSET_1:2;
      ex S being 1-sorted st S = C.i & CA.i = the carrier of S
      by A4,PRALG_1:def 13;
      then
A11:  the carrier of R in rng CA by A1,A4,A6,FUNCT_1:def 3;
      then
A12:  x1 in union rng CA by A9,TARSKI:def 4;
      x2 in union rng CA by A10,A11,TARSKI:def 4;
      hence thesis by A8,A12,ZFMISC_1:87;
    end;
    then reconsider IR as Relation of D;
    TR c= [:D,D:]
    proof
      let x be set;
      assume x in TR;
      then consider P being set such that
A13:  x in P and
A14:  P in rng TRA by TARSKI:def 4;
      consider i being set such that
A15:  i in dom TRA and
A16:  TRA.i = P by A14,FUNCT_1:def 3;
      consider R being TolStr such that
A17:  R = C.i and
A18:  TRA.i = the ToleranceRel of R by A15,Def19;
      consider x1, x2 being set such that
A19:  x = [x1,x2] and
A20:  x1 in the carrier of R and
A21:  x2 in the carrier of R by A13,A16,A18,RELSET_1:2;
      ex S being 1-sorted st S = C.i & CA.i = the carrier of S
      by A15,PRALG_1:def 13;
      then
A22:  the carrier of R in rng CA by A1,A15,A17,FUNCT_1:def 3;
      then
A23:  x1 in union rng CA by A20,TARSKI:def 4;
      x2 in union rng CA by A21,A22,TARSKI:def 4;
      hence thesis by A19,A23,ZFMISC_1:87;
    end;
    then reconsider TR as Relation of D;
    take pcs-Str(#D,IR,TR#);
    thus thesis;
  end;
  uniqueness;
end;

theorem Th10:
  for I being set, C being pcs-Str-yielding ManySortedSet of I
  for p, q being Element of pcs-union C holds p <= q iff
  ex i being set, P being pcs-Str, p9, q9 being Element of P st
  i in I & P = C.i & p9 = p & q9 = q & p9 <= q9
proof
  let I be set, C be pcs-Str-yielding ManySortedSet of I;
  set R = pcs-union C;
  let p, q be Element of R;
A1: dom pcs-InternalRels C = I by PARTFUN1:def 2;
  thus p <= q implies
  ex i being set, P being pcs-Str, p9, q9 being Element of P st
  i in I & P = C.i & p9 = p & q9 = q & p9 <= q9
  proof
    assume p <= q;
    then [p,q] in the InternalRel of R by ORDERS_2:def 5;
    then [p,q] in Union pcs-InternalRels C by Def36;
    then consider Z being set such that
A2: [p,q] in Z and
A3: Z in rng pcs-InternalRels C by TARSKI:def 4;
    consider i being set such that
A4: i in dom pcs-InternalRels C and
A5: (pcs-InternalRels C).i = Z by A3,FUNCT_1:def 3;
    reconsider I1 = I as non empty set by A4;
    reconsider A1 = C as pcs-Str-yielding ManySortedSet of I1;
    reconsider i1 = i as Element of I1 by A4;
    reconsider P = A1.i1 as pcs-Str;
    take i, P;
    Z = the InternalRel of A1.i1 by A5,Def6;
    then reconsider p9 = p, q9 = q as Element of P by A2,ZFMISC_1:87;
    take p9, q9;
    thus i in I by A4;
    thus P = C.i & p9 = p & q9 = q;
    thus [p9,q9] in the InternalRel of P by A2,A5,Def6;
  end;
  given i being set, P being pcs-Str, p9, q9 being Element of P such that
A6: i in I and
A7: P = C.i and
A8: p9 = p and
A9: q9 = q and
A10: p9 <= q9;
A11: [p9,q9] in the InternalRel of P by A10,ORDERS_2:def 5;
  reconsider I1 = I as non empty set by A6;
  reconsider i1 = i as Element of I1 by A6;
  reconsider A1 = C as pcs-Str-yielding ManySortedSet of I1;
  (pcs-InternalRels A1).i1 = the InternalRel of A1.i1 by Def6;
  then the InternalRel of A1.i1 in rng pcs-InternalRels C by A1,FUNCT_1:3;
  then [p,q] in Union pcs-InternalRels C by A7,A8,A9,A11,TARSKI:def 4;
  hence [p,q] in the InternalRel of R by Def36;
end;

theorem
  for I being non empty set, C being pcs-Str-yielding ManySortedSet of I
  for p, q being Element of pcs-union C holds p <= q iff
  ex i being Element of I, p9, q9 being Element of C.i st
  p9 = p & q9 = q & p9 <= q9
proof
  let I be non empty set, C be pcs-Str-yielding ManySortedSet of I;
  let p, q be Element of pcs-union C;
  thus
  p <= q implies ex i being Element of I, p9, q9 being Element of C.i st
  p9 = p & q9 = q & p9 <= q9
  proof
    assume p <= q;
    then ex i being set, P being pcs-Str, p9, q9 being Element of P st
    i in I & P = C.i & p9 = p & q9 = q & p9 <= q9 by Th10;
    hence thesis;
  end;
  thus thesis by Th10;
end;

theorem Th12:
  for I being set, C being pcs-Str-yielding ManySortedSet of I
  for p, q being Element of pcs-union C holds p (--) q iff
  ex i being set, P being pcs-Str, p9, q9 being Element of P st
  i in I & P = C.i & p9 = p & q9 = q & p9 (--) q9
proof
  let I be set, C be pcs-Str-yielding ManySortedSet of I;
  set R = pcs-union C;
  let p, q be Element of R;
A1: dom pcs-ToleranceRels C = I by PARTFUN1:def 2;
  thus p (--) q implies
  ex i being set, P being pcs-Str, p9, q9 being Element of P st
  i in I & P = C.i & p9 = p & q9 = q & p9 (--) q9
  proof
    assume p (--) q;
    then [p,q] in the ToleranceRel of R by Def7;
    then [p,q] in Union pcs-ToleranceRels C by Def36;
    then consider Z being set such that
A2: [p,q] in Z and
A3: Z in rng pcs-ToleranceRels C by TARSKI:def 4;
    consider i being set such that
A4: i in dom pcs-ToleranceRels C and
A5: (pcs-ToleranceRels C).i = Z by A3,FUNCT_1:def 3;
    reconsider I1 = I as non empty set by A4;
    reconsider A1 = C as pcs-Str-yielding ManySortedSet of I1;
    reconsider i1 = i as Element of I1 by A4;
    reconsider P = A1.i1 as pcs-Str;
    take i, P;
    Z = the ToleranceRel of A1.i1 by A5,Def20;
    then reconsider p9 = p, q9 = q as Element of P by A2,ZFMISC_1:87;
    take p9, q9;
    thus i in I by A4;
    thus P = C.i & p9 = p & q9 = q;
    thus [p9,q9] in the ToleranceRel of P by A2,A5,Def20;
  end;
  given i being set, P being pcs-Str, p9, q9 being Element of P such that
A6: i in I and
A7: P = C.i and
A8: p9 = p and
A9: q9 = q and
A10: p9 (--) q9;
A11: [p9,q9] in the ToleranceRel of P by A10,Def7;
  reconsider I1 = I as non empty set by A6;
  reconsider i1 = i as Element of I1 by A6;
  reconsider A1 = C as pcs-Str-yielding ManySortedSet of I1;
  (pcs-ToleranceRels A1).i1 = the ToleranceRel of A1.i1 by Def20;
  then the ToleranceRel of A1.i1 in rng pcs-ToleranceRels C by A1,FUNCT_1:3;
  then [p,q] in Union pcs-ToleranceRels C by A7,A8,A9,A11,TARSKI:def 4;
  hence [p,q] in the ToleranceRel of R by Def36;
end;

theorem
  for I being non empty set, C being pcs-Str-yielding ManySortedSet of I
  for p, q being Element of pcs-union C holds p (--) q iff
  ex i being Element of I, p9, q9 being Element of C.i st
  p9 = p & q9 = q & p9 (--) q9
proof
  let I be non empty set, C be pcs-Str-yielding ManySortedSet of I;
  let p, q be Element of pcs-union C;
  thus p (--) q implies ex i being Element of I, p9, q9 being Element of C.i st
  p9 = p & q9 = q & p9 (--) q9
  proof
    assume p (--) q;
    then ex i being set, P being pcs-Str, p9, q9 being Element of P st
    i in I & P = C.i & p9 = p & q9 = q & p9 (--) q9 by Th12;
    hence thesis;
  end;
  thus thesis by Th12;
end;

registration
  let I be set, C be reflexive-yielding pcs-Str-yielding ManySortedSet of I;
  cluster pcs-union C -> reflexive;
  coherence
  proof
    set P = pcs-union C;
    set IR = the InternalRel of P;
    set CP = the carrier of P;
    set CA = Carrier C;
A1: CP = Union CA by Def36;
A2: IR = Union pcs-InternalRels C by Def36;
A3: dom pcs-InternalRels C = I by PARTFUN1:def 2;
    let x be set;
    assume x in CP;
    then consider P being set such that
A4: x in P and
A5: P in rng CA by A1,TARSKI:def 4;
    consider i being set such that
A6: i in dom CA and
A7: CA.i = P by A5,FUNCT_1:def 3;
A8: ex R being 1-sorted st ( R = C.i)&( CA.i = the carrier of R)
    by A6,PRALG_1:def 13;
    reconsider I as non empty set by A6;
    reconsider i as Element of I by A6;
    reconsider C as reflexive-yielding pcs-Str-yielding ManySortedSet of I;
A9: (pcs-InternalRels C).i = the InternalRel of C.i by Def6;
    the InternalRel of C.i is_reflexive_in the carrier of C.i
    by ORDERS_2:def 2;
    then
A10: [x,x] in the InternalRel of C.i by A4,A7,A8,RELAT_2:def 1;
    the InternalRel of C.i in rng pcs-InternalRels C by A3,A9,FUNCT_1:3;
    hence thesis by A2,A10,TARSKI:def 4;
  end;
end;

registration
  let I be set,
  C be pcs-tol-reflexive-yielding pcs-Str-yielding ManySortedSet of I;
  cluster pcs-union C -> pcs-tol-reflexive;
  coherence
  proof
    set P = pcs-union C;
    set TR = the ToleranceRel of P;
    set CP = the carrier of P;
    set CA = Carrier C;
A1: CP = Union CA by Def36;
A2: TR = Union pcs-ToleranceRels C by Def36;
A3: dom pcs-ToleranceRels C = I by PARTFUN1:def 2;
    let x be set;
    assume x in CP;
    then consider P being set such that
A4: x in P and
A5: P in rng CA by A1,TARSKI:def 4;
    consider i being set such that
A6: i in dom CA and
A7: CA.i = P by A5,FUNCT_1:def 3;
A8: ex R being 1-sorted st ( R = C.i)&( CA.i = the carrier of R)
    by A6,PRALG_1:def 13;
    reconsider I as non empty set by A6;
    reconsider i as Element of I by A6;
    reconsider C as pcs-tol-reflexive-yielding pcs-Str-yielding
    ManySortedSet of I;
A9: (pcs-ToleranceRels C).i = the ToleranceRel of C.i by Def20;
    the ToleranceRel of C.i is_reflexive_in the carrier of C.i by Def9;
    then
A10: [x,x] in the ToleranceRel of C.i by A4,A7,A8,RELAT_2:def 1;
    the ToleranceRel of C.i in rng pcs-ToleranceRels C by A3,A9,FUNCT_1:3;
    hence thesis by A2,A10,TARSKI:def 4;
  end;
end;

registration
  let I be set,
  C be pcs-tol-symmetric-yielding pcs-Str-yielding ManySortedSet of I;
  cluster pcs-union C -> pcs-tol-symmetric;
  coherence
  proof
    set P = pcs-union C;
    set TR = the ToleranceRel of P;
    set CP = the carrier of P;
A1: TR = Union pcs-ToleranceRels C by Def36;
    let x, y be set;
    assume that x in CP and y in CP;
    assume [x,y] in TR;
    then consider P being set such that
A2: [x,y] in P and
A3: P in rng pcs-ToleranceRels C by A1,TARSKI:def 4;
    consider i being set such that
A4: i in dom pcs-ToleranceRels C and
A5: (pcs-ToleranceRels C).i = P by A3,FUNCT_1:def 3;
    reconsider I as non empty set by A4;
    reconsider C as pcs-tol-symmetric-yielding pcs-Str-yielding
    ManySortedSet of I;
    reconsider i as Element of I by A4;
A6: (pcs-ToleranceRels C).i = the ToleranceRel of C.i by Def20;
    then
A7: x in the carrier of C.i by A2,A5,ZFMISC_1:87;
A8: y in the carrier of C.i by A2,A5,A6,ZFMISC_1:87;
    the ToleranceRel of C.i is_symmetric_in the carrier of C.i by Def11;
    then
A9: [y,x] in the ToleranceRel of C.i by A2,A5,A6,A7,A8,RELAT_2:def 3;
    the ToleranceRel of C.i in rng pcs-ToleranceRels C by A4,A6,FUNCT_1:3;
    hence thesis by A1,A9,TARSKI:def 4;
  end;
end;

registration
  let I be set, C be pcs-Chain of I;
  cluster pcs-union C -> transitive pcs-compatible;
  coherence
  proof
    set P = pcs-union C;
    set IR = the InternalRel of P;
    set TR = the ToleranceRel of P;
    set CA = the carrier of P;
A1: IR = Union pcs-InternalRels C by Def36;
A2: TR = Union pcs-ToleranceRels C by Def36;
A3: dom C = I by PARTFUN1:def 2;
    thus P is transitive
    proof
      let x, y, z be set;
      assume that x in CA and y in CA
      and z in CA;
      assume [x,y] in IR;
      then consider Z1 being set such that
A4:   [x,y] in Z1 and
A5:   Z1 in rng pcs-InternalRels C by A1,TARSKI:def 4;
      consider i being set such that
A6:   i in dom pcs-InternalRels C and
A7:   (pcs-InternalRels C).i = Z1 by A5,FUNCT_1:def 3;
      assume [y,z] in IR;
      then consider Z2 being set such that
A8:   [y,z] in Z2 and
A9:   Z2 in rng pcs-InternalRels C by A1,TARSKI:def 4;
      consider j being set such that
A10:  j in dom pcs-InternalRels C and
A11:  (pcs-InternalRels C).j = Z2 by A9,FUNCT_1:def 3;
      reconsider I as non empty set by A6;
      reconsider C as pcs-Chain of I;
      reconsider i, j as Element of I by A6,A10;
A12:  (pcs-InternalRels C).i = the InternalRel of C.i by Def6;
      then
A13:  x in the carrier of C.i by A4,A7,ZFMISC_1:87;
A14:  y in the carrier of C.i by A4,A7,A12,ZFMISC_1:87;
A15:  (pcs-InternalRels C).j = the InternalRel of C.j by Def6;
A16:  C.i in rng C by A3,FUNCT_1:3;
A17:  C.j in rng C by A3,FUNCT_1:3;
A18:  the InternalRel of C.i is_transitive_in the carrier of C.i
      by ORDERS_2:def 3;
A19:  the InternalRel of C.j is_transitive_in the carrier of C.j
      by ORDERS_2:def 3;
      per cases by A16,A17,Def35;
      suppose C.i c= C.j;
        then
A20:    the InternalRel of C.i c= the InternalRel of C.j by Def34;
        then
A21:    [x,y] in the InternalRel of C.j by A4,A7,A12;
        then
A22:    x in the carrier of C.j by ZFMISC_1:87;
A23:    y in the carrier of C.j by A21,ZFMISC_1:87;
        z in the carrier of C.j by A8,A11,A15,ZFMISC_1:87;
        then
A24:    [x,z] in the InternalRel of C.j by A4,A7,A8,A11,A12,A15,A19,A20,A22,A23
,RELAT_2:def 8;
        the InternalRel of C.j c= IR by A1,A9,A11,A15,ZFMISC_1:74;
        hence thesis by A24;
      end;
      suppose C.j c= C.i;
        then
A25:    the InternalRel of C.j c= the InternalRel of C.i by Def34;
        then [y,z] in the InternalRel of C.i by A8,A11,A15;
        then z in the carrier of C.i by ZFMISC_1:87;
        then
A26:    [x,z] in the InternalRel of C.i by A4,A7,A8,A11,A12,A13,A14,A15,A18,A25
,RELAT_2:def 8;
        the InternalRel of C.i c= IR by A1,A5,A7,A12,ZFMISC_1:74;
        hence thesis by A26;
      end;
    end;
    let p, p9, q, q9 be Element of P such that
A27: p (--) q and
A28: p9 <= p and
A29: q9 <= q;
    [p9,p] in IR by A28,ORDERS_2:def 5;
    then consider Z1 being set such that
A30: [p9,p] in Z1 and
A31: Z1 in rng pcs-InternalRels C by A1,TARSKI:def 4;
    consider i being set such that
A32: i in dom pcs-InternalRels C and
A33: (pcs-InternalRels C).i = Z1 by A31,FUNCT_1:def 3;
    reconsider I as non empty set by A32;
    reconsider C as pcs-Chain of I;
    reconsider i as Element of I by A32;
A34: (pcs-ToleranceRels C).i = the ToleranceRel of C.i by Def20;
A35: (pcs-InternalRels C).i = the InternalRel of C.i by Def6;
    then reconsider pi1 = p, p9i = p9 as Element of C.i
    by A30,A33,ZFMISC_1:87;
    [q9,q] in IR by A29,ORDERS_2:def 5;
    then consider Z2 being set such that
A36: [q9,q] in Z2 and
A37: Z2 in rng pcs-InternalRels C by A1,TARSKI:def 4;
    consider j being set such that
A38: j in dom pcs-InternalRels C and
A39: (pcs-InternalRels C).j = Z2 by A37,FUNCT_1:def 3;
    reconsider j as Element of I by A38;
A40: (pcs-ToleranceRels C).j = the ToleranceRel of C.j by Def20;
A41: (pcs-InternalRels C).j = the InternalRel of C.j by Def6;
    then
A42: q9 in the carrier of C.j by A36,A39,ZFMISC_1:87;
A43: q in the carrier of C.j by A36,A39,A41,ZFMISC_1:87;
    reconsider qj = q as Element of C.j by A36,A39,A41,ZFMISC_1:87;
    [p,q] in TR by A27,Def7;
    then consider Z3 being set such that
A44: [p,q] in Z3 and
A45: Z3 in rng pcs-ToleranceRels C by A2,TARSKI:def 4;
    consider k being set such that
A46: k in dom pcs-ToleranceRels C and
A47: (pcs-ToleranceRels C).k = Z3 by A45,FUNCT_1:def 3;
    reconsider k as Element of I by A46;
A48: (pcs-ToleranceRels C).k = the ToleranceRel of C.k by Def20;
    then reconsider pk = p, qk = q as Element of C.k by A44,A47,ZFMISC_1:87;
A49: C.i in rng C by A3,FUNCT_1:3;
A50: C.j in rng C by A3,FUNCT_1:3;
A51: C.k in rng C by A3,FUNCT_1:3;
A52: dom pcs-ToleranceRels C = I by PARTFUN1:def 2;
    then
A53: the ToleranceRel of C.i c= TR by A2,A34,FUNCT_1:3,ZFMISC_1:74;
A54: the ToleranceRel of C.j c= TR by A2,A40,A52,FUNCT_1:3,ZFMISC_1:74;
A55: the ToleranceRel of C.k c= TR by A2,A45,A47,A48,ZFMISC_1:74;
    per cases by A49,A50,A51,Def35;
    suppose that
A56:  C.i c= C.j and
A57:  C.j c= C.k;
A58:  the InternalRel of C.j c= the InternalRel of C.k by A57,Def34;
      the InternalRel of C.i c= the InternalRel of C.j by A56,Def34;
      then
A59:  [p9,p] in the InternalRel of C.j by A30,A33,A35;
      then [p9,p] in the InternalRel of C.k by A58;
      then reconsider p9k = p9 as Element of C.k by ZFMISC_1:87;
      [q9,q] in the InternalRel of C.k by A36,A39,A41,A58;
      then reconsider q9k = q9 as Element of C.k by ZFMISC_1:87;
A60:  p9k <= pk by A58,A59,ORDERS_2:def 5;
A61:  q9k <= qk by A36,A39,A41,A58,ORDERS_2:def 5;
      pk (--) qk by A44,A47,A48,Def7;
      then p9k (--) q9k by A60,A61,Def22;
      then [p9k,q9k] in the ToleranceRel of C.k by Def7;
      hence [p9,q9] in TR by A55;
    end;
    suppose that
A62:  C.j c= C.i and
A63:  C.i c= C.k;
A64:  the InternalRel of C.i c= the InternalRel of C.k by A63,Def34;
A65:  the InternalRel of C.j c= the InternalRel of C.i by A62,Def34;
      [p9,p] in the InternalRel of C.k by A30,A33,A35,A64;
      then reconsider p9k = p9 as Element of C.k by ZFMISC_1:87;
A66:  [q9,q] in the InternalRel of C.i by A36,A39,A41,A65;
      then [q9,q] in the InternalRel of C.k by A64;
      then reconsider q9k = q9 as Element of C.k by ZFMISC_1:87;
A67:  p9k <= pk by A30,A33,A35,A64,ORDERS_2:def 5;
A68:  q9k <= qk by A64,A66,ORDERS_2:def 5;
      pk (--) qk by A44,A47,A48,Def7;
      then p9k (--) q9k by A67,A68,Def22;
      then [p9k,q9k] in the ToleranceRel of C.k by Def7;
      hence [p9,q9] in TR by A55;
    end;
    suppose that
A69:  C.i c= C.k and
A70:  C.k c= C.j;
A71:  the InternalRel of C.k c= the InternalRel of C.j by A70,Def34;
A72:  the ToleranceRel of C.k c= the ToleranceRel of C.j by A70,Def34;
      the InternalRel of C.i c= the InternalRel of C.k by A69,Def34;
      then
A73:  [p9,p] in the InternalRel of C.k by A30,A33,A35;
      then
A74:  [p9,p] in the InternalRel of C.j by A71;
      then reconsider p9j = p9 as Element of C.j by ZFMISC_1:87;
      reconsider q9j = q9 as Element of C.j by A36,A39,A41,ZFMISC_1:87;
      reconsider pj = p as Element of C.j by A74,ZFMISC_1:87;
A75:  p9j <= pj by A71,A73,ORDERS_2:def 5;
A76:  q9j <= qj by A36,A39,A41,ORDERS_2:def 5;
      pj (--) qj by A44,A47,A48,A72,Def7;
      then p9j (--) q9j by A75,A76,Def22;
      then [p9j,q9j] in the ToleranceRel of C.j by Def7;
      hence [p9,q9] in TR by A54;
    end;
    suppose that
A77:  C.k c= C.i and
A78:  C.i c= C.j;
A79:  the InternalRel of C.i c= the InternalRel of C.j by A78,Def34;
A80:  the ToleranceRel of C.i c= the ToleranceRel of C.j by A78,Def34;
A81:  the ToleranceRel of C.k c= the ToleranceRel of C.i by A77,Def34;
A82:  [p9,p] in the InternalRel of C.j by A30,A33,A35,A79;
      then reconsider p9j = p9 as Element of C.j by ZFMISC_1:87;
      reconsider q9j = q9 as Element of C.j by A36,A39,A41,ZFMISC_1:87;
      reconsider pj = p as Element of C.j by A82,ZFMISC_1:87;
      q in the carrier of C.k by A44,A47,A48,ZFMISC_1:87;
      then reconsider qi = q as Element of C.i by A77,Lm2;
A83:  p9j <= pj by A30,A33,A35,A79,ORDERS_2:def 5;
A84:  q9j <= qj by A36,A39,A41,ORDERS_2:def 5;
      pi1 (--) qi by A44,A47,A48,A81,Def7;
      then pj (--) qj by A80,Th9;
      then p9j (--) q9j by A83,A84,Def22;
      then [p9j,q9j] in the ToleranceRel of C.j by Def7;
      hence [p9,q9] in TR by A54;
    end;
    suppose that
A85:  C.k c= C.j and
A86:  C.j c= C.i;
A87:  the ToleranceRel of C.j c= the ToleranceRel of C.i by A86,Def34;
A88:  the ToleranceRel of C.k c= the ToleranceRel of C.j by A85,Def34;
A89:  the InternalRel of C.j c= the InternalRel of C.i by A86,Def34;
      reconsider q9i = q9 as Element of C.i by A42,A86,Lm2;
      reconsider qi = q as Element of C.i by A43,A86,Lm2;
      p in the carrier of C.k by A44,A47,A48,ZFMISC_1:87;
      then reconsider pj = p as Element of C.j by A85,Lm2;
A90:  p9i <= pi1 by A30,A33,A35,ORDERS_2:def 5;
A91:  q9i <= qi by A36,A39,A41,A89,ORDERS_2:def 5;
      pj (--) qj by A44,A47,A48,A88,Def7;
      then pi1 (--) qi by A87,Th9;
      then p9i (--) q9i by A90,A91,Def22;
      then [p9i,q9i] in the ToleranceRel of C.i by Def7;
      hence [p9,q9] in TR by A53;
    end;
    suppose that
A92:  C.j c= C.k and
A93:  C.k c= C.i;
A94:  the ToleranceRel of C.k c= the ToleranceRel of C.i by A93,Def34;
A95:  the InternalRel of C.k c= the InternalRel of C.i by A93,Def34;
A96:  the InternalRel of C.j c= the InternalRel of C.k by A92,Def34;
      reconsider q9k = q9 as Element of C.k by A42,A92,Lm2;
A97:  the carrier of C.j c= the carrier of C.k by A92,Def34;
      then reconsider q9i = q9 as Element of C.i by A42,A93,Lm2;
      reconsider qi = q as Element of C.i by A43,A93,A97,Lm2;
A98:  q9k <= qk by A36,A39,A41,A96,ORDERS_2:def 5;
A99:  p9i <= pi1 by A30,A33,A35,ORDERS_2:def 5;
A100: q9i <= qi by A95,A98,Th8;
      pi1 (--) qi by A44,A47,A48,A94,Def7;
      then p9i (--) q9i by A99,A100,Def22;
      then [p9i,q9i] in the ToleranceRel of C.i by Def7;
      hence [p9,q9] in TR by A53;
    end;
  end;
end;

:: Direct Sum of PCS's

registration
  let p, q be set;
  cluster <%p,q%> -> {0,1}-defined;
  coherence
  proof
    len <%p,q%> = {0,1} by AFINSQ_1:38,CARD_1:50;
    hence thesis by RELAT_1:def 18;
  end;
  cluster <%p,q%> -> total;
  coherence
  proof
    len <%p,q%> = {0,1} by AFINSQ_1:38,CARD_1:50;
    hence thesis by PARTFUN1:def 2;
  end;
end;

registration
  let P, Q be 1-sorted;
  cluster <%P,Q%> -> 1-sorted-yielding;
  coherence
  proof
    let x be set;
    assume x in dom <%P,Q%>;
    then x in len <%P,Q%>;
    then x in 2 by AFINSQ_1:38;
    then x = 0 or x = 1 by CARD_1:50,TARSKI:def 2;
    hence thesis by AFINSQ_1:38;
  end;
end;

Lm3:
now
  let a,b be set;
  <%a,b%> = (0,1) --> (a,b) by AFINSQ_1:76;
  hence rng <%a,b%> = {a,b} by FUNCT_4:64;
end;

registration
  let P, Q be RelStr;
  cluster <%P,Q%> -> RelStr-yielding;
  coherence
  proof
    let x be set;
    assume x in rng <%P,Q%>;
    then x in {P,Q} by Lm3;
    hence thesis by TARSKI:def 2;
  end;
end;

registration
  let P, Q be TolStr;
  cluster <%P,Q%> -> TolStr-yielding;
  coherence
  proof
    let x be set;
    assume x in {0,1};
    then x = 0 or x = 1 by TARSKI:def 2;
    hence thesis by AFINSQ_1:38;
  end;
end;

registration
  let P, Q be pcs-Str;
  cluster <%P,Q%> -> pcs-Str-yielding;
  coherence
  proof
    let x be set;
    assume x in {0,1};
    then x = 0 or x = 1 by TARSKI:def 2;
    hence thesis by AFINSQ_1:38;
  end;
end;

registration
  let P, Q be reflexive pcs-Str;
  cluster <%P,Q%> -> reflexive-yielding;
  coherence
  proof
    let x be RelStr;
    assume x in rng <%P,Q%>;
    then x in {P,Q} by Lm3;
    hence thesis by TARSKI:def 2;
  end;
end;

registration
  let P, Q be transitive pcs-Str;
  cluster <%P,Q%> -> transitive-yielding;
  coherence
  proof
    let x be RelStr;
    assume x in rng <%P,Q%>;
    then x in {P,Q} by Lm3;
    hence thesis by TARSKI:def 2;
  end;
end;

registration
  let P, Q be pcs-tol-reflexive pcs-Str;
  cluster <%P,Q%> -> pcs-tol-reflexive-yielding;
  coherence
  proof
    let x be TolStr;
    assume x in rng <%P,Q%>;
    then x in {P,Q} by Lm3;
    hence thesis by TARSKI:def 2;
  end;
end;

registration
  let P, Q be pcs-tol-symmetric pcs-Str;
  cluster <%P,Q%> -> pcs-tol-symmetric-yielding;
  coherence
  proof
    let x be TolStr;
    assume x in rng <%P,Q%>;
    then x in {P,Q} by Lm3;
    hence thesis by TARSKI:def 2;
  end;
end;

registration
  let P, Q be pcs;
  cluster <%P,Q%> -> pcs-yielding;
  coherence
  proof
    let x be set;
    assume x in {0,1};
    then x = 0 or x = 1 by TARSKI:def 2;
    hence thesis by AFINSQ_1:38;
  end;
end;

definition
  canceled;
  let P, Q be pcs-Str;
  func pcs-sum(P,Q) -> pcs-Str equals
  pcs-union <%P,Q%>;
  coherence;
end;

deffunc pcsSUM(pcs-Str,pcs-Str) = pcs-Str (#
  (the carrier of $1) \/ the carrier of $2,
  (the InternalRel of $1) \/ the InternalRel of $2,
  (the ToleranceRel of $1) \/ the ToleranceRel of $2 #);

theorem Th14:
  for P, Q being pcs-Str holds
  the carrier of pcs-sum(P,Q) = (the carrier of P) \/ the carrier of Q &
  the InternalRel of pcs-sum(P,Q) =
  (the InternalRel of P) \/ the InternalRel of Q &
  the ToleranceRel of pcs-sum(P,Q) =
  (the ToleranceRel of P) \/ the ToleranceRel of Q
proof
  let P, Q be pcs-Str;
  set S = pcsSUM(P,Q);
  set f = <%P,Q%>;
A1: dom Carrier f = {0,1} by PARTFUN1:def 2;
A2: dom pcs-InternalRels f = {0,1} by PARTFUN1:def 2;
A3: dom pcs-ToleranceRels f = {0,1} by PARTFUN1:def 2;
A4: f.0 = P by AFINSQ_1:38;
A5: f.1 = Q by AFINSQ_1:38;
A6: the carrier of S = Union Carrier f
  proof
    thus the carrier of S c= Union Carrier f
    proof
      let x be set;
      assume x in the carrier of S;
      then
A7:   x in the carrier of P or x in the carrier of Q by XBOOLE_0:def 3;
A8:   (Carrier f).z = the carrier of f.z by Def1;
A9:   (Carrier f).j = the carrier of f.j by Def1;
A10:  the carrier of P in rng Carrier f by A1,A4,A8,FUNCT_1:3;
      the carrier of Q in rng Carrier f by A1,A5,A9,FUNCT_1:3;
      hence thesis by A7,A10,TARSKI:def 4;
    end;
    let x be set;
    assume x in Union Carrier f;
    then consider Z being set such that
A11: x in Z and
A12: Z in rng Carrier f by TARSKI:def 4;
    consider i being set such that
A13: i in dom Carrier f and
A14: Carrier f.i = Z by A12,FUNCT_1:def 3;
    i = 0 or i = 1 by A13,TARSKI:def 2;
    then Z = the carrier of f.z or Z = the carrier of f.j by A14,Def1;
    hence thesis by A4,A5,A11,XBOOLE_0:def 3;
  end;
A15: the InternalRel of S = Union pcs-InternalRels f
  proof
    thus the InternalRel of S c= Union pcs-InternalRels f
    proof
      let x be set;
      assume x in the InternalRel of S;
      then
A16:  x in the InternalRel of P or x in the InternalRel of Q by XBOOLE_0:def 3;
A17:  (pcs-InternalRels f).z = the InternalRel of f.z by Def6;
A18:  (pcs-InternalRels f).j = the InternalRel of f.j by Def6;
A19:  the InternalRel of P in rng pcs-InternalRels f by A2,A4,A17,FUNCT_1:3;
      the InternalRel of Q in rng pcs-InternalRels f by A2,A5,A18,FUNCT_1:3;
      hence thesis by A16,A19,TARSKI:def 4;
    end;
    let x be set;
    assume x in Union pcs-InternalRels f;
    then consider Z being set such that
A20: x in Z and
A21: Z in rng pcs-InternalRels f by TARSKI:def 4;
    consider i being set such that
A22: i in dom pcs-InternalRels f and
A23: (pcs-InternalRels f).i = Z by A21,FUNCT_1:def 3;
    i = 0 or i = 1 by A22,TARSKI:def 2;
    then Z = the InternalRel of f.z or Z = the InternalRel of f.j by A23,Def6;
    hence thesis by A4,A5,A20,XBOOLE_0:def 3;
  end;
  the ToleranceRel of S = Union pcs-ToleranceRels f
  proof
    thus the ToleranceRel of S c= Union pcs-ToleranceRels f
    proof
      let x be set;
      assume x in the ToleranceRel of S;
      then
A24:  x in the ToleranceRel of P or x in the ToleranceRel of Q
      by XBOOLE_0:def 3;
A25:  (pcs-ToleranceRels f).z = the ToleranceRel of f.z by Def20;
A26:  (pcs-ToleranceRels f).j = the ToleranceRel of f.j by Def20;
A27:  the ToleranceRel of P in rng pcs-ToleranceRels f by A3,A4,A25,FUNCT_1:3;
      the ToleranceRel of Q in rng pcs-ToleranceRels f by A3,A5,A26,FUNCT_1:3;
      hence thesis by A24,A27,TARSKI:def 4;
    end;
    let x be set;
    assume x in Union pcs-ToleranceRels f;
    then consider Z being set such that
A28: x in Z and
A29: Z in rng pcs-ToleranceRels f by TARSKI:def 4;
    consider i being set such that
A30: i in dom pcs-ToleranceRels f and
A31: (pcs-ToleranceRels f).i = Z by A29,FUNCT_1:def 3;
    i = 0 or i = 1 by A30,TARSKI:def 2;
    then Z = the ToleranceRel of f.z or
    Z = the ToleranceRel of f.j by A31,Def20;
    hence thesis by A4,A5,A28,XBOOLE_0:def 3;
  end;
  hence thesis by A6,A15,Def36;
end;

theorem Th15:
  for P, Q being pcs-Str holds pcs-sum(P,Q) = pcs-Str (#
    (the carrier of P) \/ the carrier of Q,
    (the InternalRel of P) \/ the InternalRel of Q,
    (the ToleranceRel of P) \/ the ToleranceRel of Q #)
proof
  let P, Q be pcs-Str;
A1: the carrier of pcs-sum(P,Q) = (the carrier of P) \/ the carrier of Q by
Th14;
  the InternalRel of pcs-sum(P,Q) = (the InternalRel of P) \/ the
  InternalRel of Q by Th14;
  hence thesis by A1,Th14;
end;

theorem
  for P, Q being pcs-Str, p, q being Element of pcs-sum(P,Q) holds p <= q iff
  (ex p9, q9 being Element of P st p9 = p & q9 = q & p9 <= q9) or
  ex p9, q9 being Element of Q st p9 = p & q9 = q & p9 <= q9
proof
  let P, Q be pcs-Str;
  set R = pcs-sum(P,Q);
  let p, q be Element of R;
A1: the InternalRel of R =
  (the InternalRel of P) \/ the InternalRel of Q by Th14;
  thus p <= q implies
  (ex p9, q9 being Element of P st p9 = p & q9 = q & p9 <= q9) or
  ex p9, q9 being Element of Q st p9 = p & q9 = q & p9 <= q9
  proof
    assume
A2: [p,q] in the InternalRel of R;
    per cases by A1,A2,XBOOLE_0:def 3;
    suppose
A3:   [p,q] in the InternalRel of P;
      then reconsider p9 = p, q9 = q as Element of P by ZFMISC_1:87;
      p9 <= q9 by A3,ORDERS_2:def 5;
      hence thesis;
    end;
    suppose
A4:   [p,q] in the InternalRel of Q;
      then reconsider p9 = p, q9 = q as Element of Q by ZFMISC_1:87;
      p9 <= q9 by A4,ORDERS_2:def 5;
      hence thesis;
    end;
  end;
  assume
A5: (ex p9, q9 being Element of P st p9 = p & q9 = q & p9 <= q9) or
  ex p9, q9 being Element of Q st p9 = p & q9 = q & p9 <= q9;
  per cases by A5;
  suppose ex p9, q9 being Element of P st p9 = p & q9 = q & p9 <= q9;
    then consider p9, q9 being Element of P such that
A6: p9 = p and
A7: q9 = q and
A8: p9 <= q9;
    [p9,q9] in the InternalRel of P by A8,ORDERS_2:def 5;
    hence [p,q] in the InternalRel of R by A1,A6,A7,XBOOLE_0:def 3;
  end;
  suppose ex p9, q9 being Element of Q st p9 = p & q9 = q & p9 <= q9;
    then consider p9, q9 being Element of Q such that
A9: p9 = p and
A10: q9 = q and
A11: p9 <= q9;
    [p9,q9] in the InternalRel of Q by A11,ORDERS_2:def 5;
    hence [p,q] in the InternalRel of R by A1,A9,A10,XBOOLE_0:def 3;
  end;
end;

theorem
  for P, Q being pcs-Str, p, q being Element of pcs-sum(P,Q) holds p (--) q iff
  (ex p9, q9 being Element of P st p9 = p & q9 = q & p9 (--) q9) or
  ex p9, q9 being Element of Q st p9 = p & q9 = q & p9 (--) q9
proof
  let P, Q be pcs-Str;
  set R = pcs-sum(P,Q);
  let p, q be Element of R;
A1: the ToleranceRel of R =
  (the ToleranceRel of P) \/ the ToleranceRel of Q by Th14;
  thus p (--) q implies
  (ex p9, q9 being Element of P st p9 = p & q9 = q & p9 (--) q9) or
  ex p9, q9 being Element of Q st p9 = p & q9 = q & p9 (--) q9
  proof
    assume
A2: [p,q] in the ToleranceRel of R;
    per cases by A1,A2,XBOOLE_0:def 3;
    suppose
A3:   [p,q] in the ToleranceRel of P;
      then reconsider p9 = p, q9 = q as Element of P by ZFMISC_1:87;
      p9 (--) q9 by A3,Def7;
      hence thesis;
    end;
    suppose
A4:   [p,q] in the ToleranceRel of Q;
      then reconsider p9 = p, q9 = q as Element of Q by ZFMISC_1:87;
      p9 (--) q9 by A4,Def7;
      hence thesis;
    end;
  end;
  assume
A5: (ex p9, q9 being Element of P st p9 = p & q9 = q & p9 (--) q9) or
  ex p9, q9 being Element of Q st p9 = p & q9 = q & p9 (--) q9;
  per cases by A5;
  suppose ex p9, q9 being Element of P st p9 = p & q9 = q & p9 (--) q9;
    then consider p9, q9 being Element of P such that
A6: p9 = p and
A7: q9 = q and
A8: p9 (--) q9;
    [p9,q9] in the ToleranceRel of P by A8,Def7;
    hence [p,q] in the ToleranceRel of R by A1,A6,A7,XBOOLE_0:def 3;
  end;
  suppose ex p9, q9 being Element of Q st p9 = p & q9 = q & p9 (--) q9;
    then consider p9, q9 being Element of Q such that
A9: p9 = p and
A10: q9 = q and
A11: p9 (--) q9;
    [p9,q9] in the ToleranceRel of Q by A11,Def7;
    hence [p,q] in the ToleranceRel of R by A1,A9,A10,XBOOLE_0:def 3;
  end;
end;

registration
  let P, Q be reflexive pcs-Str;
  cluster pcs-sum(P,Q) -> reflexive;
  coherence;
end;

registration
  let P, Q be pcs-tol-reflexive pcs-Str;
  cluster pcs-sum(P,Q) -> pcs-tol-reflexive;
  coherence;
end;

registration
  let P, Q be pcs-tol-symmetric pcs-Str;
  cluster pcs-sum(P,Q) -> pcs-tol-symmetric;
  coherence;
end;

theorem Th18:
  for P, Q being pcs holds
  P misses Q implies the InternalRel of pcs-sum(P,Q) is transitive
proof
  let P, Q be pcs;
  assume
A1: the carrier of P misses the carrier of Q;
  pcs-sum(P,Q) = pcsSUM(P,Q) by Th15;
  hence thesis by A1,Th1;
end;

theorem Th19:
  for P, Q being pcs holds P misses Q implies pcs-sum(P,Q) is pcs-compatible
proof
  let P, Q be pcs;
  set D1 = the carrier of P;
  set D2 = the carrier of Q;
  set R1 = the InternalRel of P;
  set R2 = the InternalRel of Q;
  set T1 = the ToleranceRel of P;
  set T2 = the ToleranceRel of Q;
  set R = R1 \/ R2;
  set T = T1 \/ T2;
  assume
A1: D1 misses D2;
  let p, p9, q, q9 be Element of pcs-sum(P,Q) such that
A2: p (--) q and
A3: p9 <= p and
A4: q9 <= q;
A5: pcs-sum(P,Q) = pcsSUM(P,Q) by Th15;
  then
A6: [p,q] in T by A2,Def7;
  per cases by A6,XBOOLE_0:def 3;
  suppose
A7: [p,q] in T1;
    then
A8: p in D1 by ZFMISC_1:87;
A9: q in D1 by A7,ZFMISC_1:87;
    reconsider p1 = p, q1 = q as Element of P by A7,ZFMISC_1:87;
A10: p1 (--) q1 by A7,Def7;
A11: [p9,p] in R by A3,A5,ORDERS_2:def 5;
A12: [q9,q] in R by A4,A5,ORDERS_2:def 5;
    then reconsider p91 = p9, q91 = q9 as Element of P by A1,A8,A9,A11,Lm1;
A13: [p9,p] in R1 by A1,A8,A11,Lm1;
A14: [q9,q] in R1 by A1,A9,A12,Lm1;
A15: p91 <= p1 by A13,ORDERS_2:def 5;
    q91 <= q1 by A14,ORDERS_2:def 5;
    then p91 (--) q91 by A10,A15,Def22;
    then [p91,q91] in T1 by Def7;
    then [p91,q91] in T by XBOOLE_0:def 3;
    hence p9 (--) q9 by A5,Def7;
  end;
  suppose
A16: [p,q] in T2;
    then
A17: p in D2 by ZFMISC_1:87;
A18: q in D2 by A16,ZFMISC_1:87;
    reconsider p1 = p, q1 = q as Element of Q by A16,ZFMISC_1:87;
A19: p1 (--) q1 by A16,Def7;
A20: [p9,p] in R by A3,A5,ORDERS_2:def 5;
A21: [q9,q] in R by A4,A5,ORDERS_2:def 5;
    then reconsider p91 = p9, q91 = q9 as Element of Q by A1,A17,A18,A20,Lm1;
A22: [p9,p] in R2 by A1,A17,A20,Lm1;
A23: [q9,q] in R2 by A1,A18,A21,Lm1;
A24: p91 <= p1 by A22,ORDERS_2:def 5;
    q91 <= q1 by A23,ORDERS_2:def 5;
    then p91 (--) q91 by A19,A24,Def22;
    then [p91,q91] in T2 by Def7;
    then [p91,q91] in T by XBOOLE_0:def 3;
    hence p9 (--) q9 by A5,Def7;
  end;
end;

theorem
  for P, Q being pcs holds P misses Q implies pcs-sum(P,Q) is pcs
proof
  let P, Q be pcs;
  assume
A1: P misses Q;
  set R = pcs-sum(P,Q);
A2: field the InternalRel of R = the carrier of R by ORDERS_1:12;
  the InternalRel of R is transitive by A1,Th18;
  then the InternalRel of R is_transitive_in the carrier of R
  by A2,RELAT_2:def 16;
  then
A3: R is transitive by ORDERS_2:def 3;
  R is pcs-compatible by A1,Th19;
  hence thesis by A3;
end;

:: Extension

definition
  let P be pcs-Str, a be set;
  func pcs-extension(P,a) -> strict pcs-Str means
  :Def39:
  the carrier of it = {a} \/ the carrier of P & the InternalRel of it =
  [:{a},the carrier of it:] \/ the InternalRel of P &
  the ToleranceRel of it = [:{a},the carrier of it:] \/
  [:the carrier of it,{a}:] \/ the ToleranceRel of P;
  existence
  proof
    set D = {a} \/ the carrier of P;
    set IR = [:{a},D:] \/ the InternalRel of P;
    set TR = [:D,{a}:] \/ [:{a},D:] \/ the ToleranceRel of P;
A1: {a} c= D by XBOOLE_1:7;
    then
A2: [:{a},D:] c= [:D,D:] by ZFMISC_1:95;
    the carrier of P c= D by XBOOLE_1:7;
    then
A3: [:the carrier of P,the carrier of P:] c= [:D,D:] by ZFMISC_1:96;
    then the InternalRel of P c= [:D,D:] by XBOOLE_1:1;
    then reconsider IR as Relation of D by A2,XBOOLE_1:8;
    [:D,{a}:] c= [:D,D:] by A1,ZFMISC_1:95;
    then
A4: [:D,{a}:] \/ [:{a},D:] c= [:D,D:] by A2,XBOOLE_1:8;
    the ToleranceRel of P c= [:D,D:] by A3,XBOOLE_1:1;
    then reconsider TR as Relation of D by A4,XBOOLE_1:8;
    take pcs-Str(#D,IR,TR#);
    thus thesis;
  end;
  uniqueness;
end;

registration
  let P be pcs-Str, a be set;
  cluster pcs-extension(P,a) -> non empty;
  coherence
  proof
    the carrier of pcs-extension(P,a) = {a} \/ the carrier of P by Def39;
    hence the carrier of pcs-extension(P,a) is non empty;
  end;
end;

theorem Th21:
  for P being pcs-Str, a being set holds
  the carrier of P c= the carrier of pcs-extension(P,a) &
  the InternalRel of P c= the InternalRel of pcs-extension(P,a) &
  the ToleranceRel of P c= the ToleranceRel of pcs-extension(P,a)
proof
  let P be pcs-Str, a be set;
  set R = pcs-extension(P,a);
A1: the carrier of R = {a} \/ the carrier of P by Def39;
A2: the InternalRel of R = [:{a},the carrier of R:] \/ the InternalRel of P
  by Def39;
  the ToleranceRel of R = [:{a},the carrier of R:] \/ [:the carrier of R,{
  a}:] \/ the ToleranceRel of P by Def39;
  hence thesis by A1,A2,XBOOLE_1:7;
end;

theorem
  for P being pcs-Str, a being set,
  p, q being Element of pcs-extension(P,a) st p = a holds p <= q
proof
  let P be pcs-Str, a be set;
  set R = pcs-extension(P,a);
  let p, q be Element of R such that
A1: p = a;
A2: the InternalRel of R =
  [:{a},the carrier of R:] \/ the InternalRel of P by Def39;
  [a,q] in [:{a},the carrier of R:] by ZFMISC_1:105;
  hence [p,q] in the InternalRel of R by A1,A2,XBOOLE_0:def 3;
end;

theorem Th23:
  for P being pcs-Str, a being set, p, q being Element of P,
  p1, q1 being Element of pcs-extension(P,a) st p = p1 & q = q1 &
  p <= q holds p1 <= q1
proof
  let P be pcs-Str, a be set, p, q be Element of P,
  p1, q1 be Element of pcs-extension(P,a) such that
A1: p = p1 and
A2: q = q1 and
A3: [p,q] in the InternalRel of P;
  the InternalRel of P c= the InternalRel of pcs-extension(P,a) by Th21;
  hence [p1,q1] in the InternalRel of pcs-extension(P,a) by A1,A2,A3;
end;

theorem Th24:
  for P being pcs-Str, a being set, p being Element of P,
  p1, q1 being Element of pcs-extension(P,a)
  st p = p1 & p <> a & p1 <= q1 & not a in the carrier of P holds
  q1 in the carrier of P & q1 <> a
proof
  let P be pcs-Str, a be set, p be Element of P,
  p1, q1 be Element of pcs-extension(P,a) such that
A1: p = p1 and
A2: p <> a and
A3: p1 <= q1 and
A4: not a in the carrier of P;
  set R = pcs-extension(P,a);
A5: the InternalRel of R = [:{a},the carrier of R:] \/ the InternalRel of P
  by Def39;
  [p1,q1] in the InternalRel of R by A3,ORDERS_2:def 5;
  then [p1,q1] in [:{a},the carrier of R:] or [p1,q1] in the InternalRel of P
  by A5,XBOOLE_0:def 3;
  hence thesis by A1,A2,A4,ZFMISC_1:87,105;
end;

theorem Th25:
  for P being pcs-Str, a being set,
  p being Element of pcs-extension(P,a) st p <> a holds p in the carrier of P
proof
  let P be pcs-Str, a be set, p be Element of pcs-extension(P,a) such that
A1: p <> a;
  the carrier of pcs-extension(P,a) = {a} \/ the carrier of P by Def39;
  then p in {a} or p in the carrier of P by XBOOLE_0:def 3;
  hence thesis by A1,TARSKI:def 1;
end;

theorem Th26:
  for P being pcs-Str, a being set, p, q being Element of P,
  p1, q1 being Element of pcs-extension(P,a) st p = p1 & q = q1 &
  p <> a & p1 <= q1 holds p <= q
proof
  let P be pcs-Str, a be set, p, q be Element of P,
  p1, q1 be Element of pcs-extension(P,a) such that
A1: p = p1 and
A2: q = q1 and
A3: p <> a and
A4: p1 <= q1;
  set R = pcs-extension(P,a);
A5: the InternalRel of R = [:{a},the carrier of R:] \/ the InternalRel of P
  by Def39;
  [p1,q1] in the InternalRel of R by A4,ORDERS_2:def 5;
  then [p1,q1] in [:{a},the carrier of R:] or [p1,q1] in the InternalRel of P
  by A5,XBOOLE_0:def 3;
  hence [p,q] in the InternalRel of P by A1,A2,A3,ZFMISC_1:105;
end;

theorem Th27:
  for P being pcs-Str, a being set,
  p, q being Element of pcs-extension(P,a) st p = a holds p (--) q & q (--) p
proof
  let P be pcs-Str, a be set;
  set R = pcs-extension(P,a);
  let p, q be Element of R such that
A1: p = a;
  the ToleranceRel of R = [:{a},the carrier of R:] \/
  [:the carrier of R,{a}:] \/ the ToleranceRel of P by Def39;
  then
A2: the ToleranceRel of R = [:{a},the carrier of R:] \/
  ([:the carrier of R,{a}:] \/ the ToleranceRel of P) by XBOOLE_1:4;
A3: [a,q] in [:{a},the carrier of R:] by ZFMISC_1:105;
  [q,a] in [:the carrier of R,{a}:] by ZFMISC_1:106;
  then [q,a] in [:the carrier of R,{a}:] \/ the ToleranceRel of P
  by XBOOLE_0:def 3;
  hence [p,q] in the ToleranceRel of R & [q,p] in the ToleranceRel of R
  by A1,A2,A3,XBOOLE_0:def 3;
end;

theorem Th28:
  for P being pcs-Str, a being set, p, q being Element of P,
  p1, q1 being Element of pcs-extension(P,a) st p = p1 & q = q1 &
  p (--) q holds p1 (--) q1
proof
  let P be pcs-Str, a be set, p, q be Element of P,
  p1, q1 be Element of pcs-extension(P,a) such that
A1: p = p1 and
A2: q = q1 and
A3: [p,q] in the ToleranceRel of P;
  the ToleranceRel of P c= the ToleranceRel of pcs-extension(P,a) by Th21;
  hence [p1,q1] in the ToleranceRel of pcs-extension(P,a) by A1,A2,A3;
end;

theorem Th29:
  for P being pcs-Str, a being set, p, q being Element of P,
  p1, q1 being Element of pcs-extension(P,a) st p = p1 & q = q1 &
  p <> a & q <> a & p1 (--) q1 holds p (--) q
proof
  let P be pcs-Str, a be set, p, q be Element of P,
  p1, q1 be Element of pcs-extension(P,a) such that
A1: p = p1 and
A2: q = q1 and
A3: p <> a and
A4: q <> a and
A5: p1 (--) q1;
  set R = pcs-extension(P,a);
A6: the ToleranceRel of R = [:{a},the carrier of R:] \/
  [:the carrier of R,{a}:] \/ the ToleranceRel of P by Def39;
  [p1,q1] in the ToleranceRel of R by A5,Def7;
  then [p1,q1] in [:{a},the carrier of R:] \/ [:the carrier of R,{a}:] or
  [p1,q1] in the ToleranceRel of P by A6,XBOOLE_0:def 3;
  then [p1,q1] in [:{a},the carrier of R:] or
  [p1,q1] in [:the carrier of R,{a}:] or
  [p1,q1] in the ToleranceRel of P by XBOOLE_0:def 3;
  hence [p,q] in the ToleranceRel of P by A1,A2,A3,A4,ZFMISC_1:105,106;
end;

registration
  let P be reflexive pcs-Str, a be set;
  cluster pcs-extension(P,a) -> reflexive;
  coherence
  proof
    set R = pcs-extension(P,a);
A1: the carrier of R = {a} \/ the carrier of P by Def39;
A2: the InternalRel of R = [:{a},the carrier of R:] \/ the InternalRel of P
    by Def39;
    let p be set;
    assume
A3: p in the carrier of R;
    per cases by A1,A3,XBOOLE_0:def 3;
    suppose p in {a};
      then p = a by TARSKI:def 1;
      then [p,p] in [:{a},the carrier of R:] by A3,ZFMISC_1:105;
      hence thesis by A2,XBOOLE_0:def 3;
    end;
    suppose
A4:   p in the carrier of P;
      the InternalRel of P is_reflexive_in the carrier of P by ORDERS_2:def 2;
      then [p,p] in the InternalRel of P by A4,RELAT_2:def 1;
      hence thesis by A2,XBOOLE_0:def 3;
    end;
  end;
end;

theorem Th30:
  for P being transitive pcs-Str, a being set st not a in the carrier of P
  holds pcs-extension(P,a) is transitive
proof
  let P be transitive pcs-Str, a be set such that
A1: not a in the carrier of P;
  set R = pcs-extension(P,a);
A2: the InternalRel of R = [:{a},the carrier of R:] \/ the InternalRel of P
  by Def39;
  let x, y, z be set;
  assume that
A3: x in the carrier of R and
A4: y in the carrier of R and
A5: z in the carrier of R and
A6: [x,y] in the InternalRel of R and
A7: [y,z] in the InternalRel of R;
A8: [a,z] in [:{a},the carrier of R:] by A5,ZFMISC_1:105;
  reconsider x, y, z as Element of R by A3,A4,A5;
A9: x <= y by A6,ORDERS_2:def 5;
A10: y <= z by A7,ORDERS_2:def 5;
  per cases;
  suppose x = a;
    hence thesis by A2,A8,XBOOLE_0:def 3;
  end;
  suppose
A11: x <> a;
    then reconsider x0 = x as Element of P by Th25;
A12: x0 <> a by A11;
    then reconsider y0 = y as Element of P by A1,A9,Th24;
    y0 <> a by A1,A9,A12,Th24;
    then reconsider z0 = z as Element of P by A1,A10,Th24;
A13: y <> a by A1,A9,A12,Th24;
A14: x0 <= y0 by A9,A11,Th26;
    y0 <= z0 by A10,A13,Th26;
    then x0 <= z0 by A14,YELLOW_0:def 2;
    then x <= z by Th23;
    hence thesis by ORDERS_2:def 5;
  end;
end;

registration
  let P be pcs-tol-reflexive pcs-Str, a be set;
  cluster pcs-extension(P,a) -> pcs-tol-reflexive;
  coherence
  proof
    set R = pcs-extension(P,a);
A1: the carrier of R = {a} \/ the carrier of P by Def39;
A2: the ToleranceRel of R = [:{a},the carrier of R:] \/
    [:the carrier of R,{a}:] \/ the ToleranceRel of P by Def39;
    then
A3: the ToleranceRel of R = [:{a},the carrier of R:] \/
    ([:the carrier of R,{a}:] \/ the ToleranceRel of P) by XBOOLE_1:4;
    let p be set;
    assume
A4: p in the carrier of R;
    per cases by A1,A4,XBOOLE_0:def 3;
    suppose p in {a};
      then p = a by TARSKI:def 1;
      then [p,p] in [:{a},the carrier of R:] by A4,ZFMISC_1:105;
      hence thesis by A3,XBOOLE_0:def 3;
    end;
    suppose
A5:   p in the carrier of P;
      the ToleranceRel of P is_reflexive_in the carrier of P by Def9;
      then [p,p] in the ToleranceRel of P by A5,RELAT_2:def 1;
      hence thesis by A2,XBOOLE_0:def 3;
    end;
  end;
end;

registration
  let P be pcs-tol-symmetric pcs-Str, a be set;
  cluster pcs-extension(P,a) -> pcs-tol-symmetric;
  coherence
  proof
    set R = pcs-extension(P,a);
A1: the ToleranceRel of R = [:{a},the carrier of R:] \/
    [:the carrier of R,{a}:] \/ the ToleranceRel of P by Def39;
    let p, q be set;
    assume that p in the carrier of R and q in the carrier of R and
A2: [p,q] in the ToleranceRel of R;
A3: the ToleranceRel of P is_symmetric_in the carrier of P by Def11;
    per cases by A1,A2,XBOOLE_0:def 3;
    suppose
A4:   [p,q] in [:{a},the carrier of R:] \/ [:the carrier of R,{a}:];
      per cases by A4,XBOOLE_0:def 3;
      suppose
A5:     [p,q] in [:{a},the carrier of R:];
        then
A6:     p = a by ZFMISC_1:105;
        q in the carrier of R by A5,ZFMISC_1:105;
        then [q,p] in [:the carrier of R,{a}:] by A6,ZFMISC_1:106;
        then [q,p] in [:{a},the carrier of R:] \/ [:the carrier of R,{a}:]
        by XBOOLE_0:def 3;
        hence thesis by A1,XBOOLE_0:def 3;
      end;
      suppose
A7:     [p,q] in [:the carrier of R,{a}:];
        then
A8:     q = a by ZFMISC_1:106;
        p in the carrier of R by A7,ZFMISC_1:106;
        then [q,p] in [:{a},the carrier of R:] by A8,ZFMISC_1:105;
        then [q,p] in [:{a},the carrier of R:] \/ [:the carrier of R,{a}:]
        by XBOOLE_0:def 3;
        hence thesis by A1,XBOOLE_0:def 3;
      end;
    end;
    suppose
A9:   [p,q] in the ToleranceRel of P;
      then
A10:  p in the carrier of P by ZFMISC_1:87;
      q in the carrier of P by A9,ZFMISC_1:87;
      then [q,p] in the ToleranceRel of P by A3,A9,A10,RELAT_2:def 3;
      hence thesis by A1,XBOOLE_0:def 3;
    end;
  end;
end;

theorem Th31:
  for P being pcs-compatible pcs-Str, a being set st not a in the carrier of P
  holds pcs-extension(P,a) is pcs-compatible
proof
  let P be pcs-compatible pcs-Str, a be set such that
A1: not a in the carrier of P;
  set R = pcs-extension(P,a);
  let p, p9, q, q9 be Element of R such that
A2: p (--) q and
A3: p9 <= p and
A4: q9 <= q;
  per cases;
  suppose p9 = a or q9 = a;
    hence thesis by Th27;
  end;
  suppose that
A5: p9 <> a and
A6: q9 <> a;
    reconsider p90 = p9, q90 = q9 as Element of P by A5,A6,Th25;
A7: p90 <> a by A5;
A8: q90 <> a by A6;
A9: p <> a by A1,A3,A7,Th24;
A10: q <> a by A1,A4,A8,Th24;
    reconsider p0 = p, q0 = q as Element of P by A1,A3,A4,A7,A8,Th24;
A11: p0 (--) q0 by A2,A9,A10,Th29;
A12: p90 <= p0 by A3,A5,Th26;
    q90 <= q0 by A4,A6,Th26;
    then p90 (--) q90 by A11,A12,Def22;
    hence thesis by Th28;
  end;
end;

theorem
  for P being pcs, a being set st not a in the carrier of P
  holds pcs-extension(P,a) is pcs
proof
  let P be pcs, a be set such that
A1: not a in the carrier of P;
  set R = pcs-extension(P,a);
  R is reflexive transitive pcs-tol-reflexive pcs-tol-symmetric
  pcs-compatible by A1,Th30,Th31;
  hence thesis;
end;

:: Reverse

definition
  let P be pcs-Str;
  func pcs-reverse(P) -> strict pcs-Str means
  :Def40:
  the carrier of it = the carrier of P &
  the InternalRel of it = (the InternalRel of P)~ &
  the ToleranceRel of it = (the ToleranceRel of P)`;
  existence
  proof
    reconsider TR = (the ToleranceRel of P)` as Relation of the carrier of P;
    take pcs-Str(#the carrier of P,(the InternalRel of P)~,TR#);
    thus thesis;
  end;
  uniqueness;
end;

registration
  let P be non empty pcs-Str;
  cluster pcs-reverse(P) -> non empty;
  coherence
  proof
    the carrier of pcs-reverse(P) = the carrier of P by Def40;
    hence the carrier of pcs-reverse(P) is non empty;
  end;
end;

theorem Th33:
  for P being pcs-Str, p, q being Element of P
  for p9, q9 being Element of pcs-reverse(P) st p = p9 & q = q9 holds
  p <= q iff q9 <= p9
proof
  let P be pcs-Str, p, q be Element of P;
  set R = pcs-reverse(P);
  let p9, q9 be Element of R such that
A1: p = p9 and
A2: q = q9;
A3: the InternalRel of R = (the InternalRel of P)~ by Def40;
  thus p <= q implies q9 <= p9
  proof
    assume [p,q] in the InternalRel of P;
    hence [q9,p9] in the InternalRel of R by A1,A2,A3,RELAT_1:def 7;
  end;
  assume [q9,p9] in the InternalRel of R;
  hence [p,q] in the InternalRel of P by A1,A2,A3,RELAT_1:def 7;
end;

theorem Th34:
  for P being pcs-Str, p, q being Element of P
  for p9, q9 being Element of pcs-reverse(P) st p = p9 & q = q9 holds
  p (--) q implies not p9 (--) q9
proof
  let P be pcs-Str, p, q be Element of P;
  set R = pcs-reverse(P);
  let p9, q9 be Element of R such that
A1: p = p9 and
A2: q = q9;
A3: the ToleranceRel of R = (the ToleranceRel of P)` by Def40;
  assume [p,q] in the ToleranceRel of P;
  hence not [p9,q9] in the ToleranceRel of R by A1,A2,A3,XBOOLE_0:def 5;
end;

theorem Th35:
  for P being non empty pcs-Str, p, q being Element of P
  for p9, q9 being Element of pcs-reverse(P) st p = p9 & q = q9 holds
  not p9 (--) q9 implies p (--) q
proof
  let P be non empty pcs-Str, p, q be Element of P;
  set R = pcs-reverse(P);
  let p9, q9 be Element of R such that
A1: p = p9 and
A2: q = q9;
A3: the ToleranceRel of R = (the ToleranceRel of P)` by Def40;
  assume
A4: not [p9,q9] in the ToleranceRel of R;
  [p,q] in [:the carrier of P,the carrier of P:] by ZFMISC_1:87;
  hence [p,q] in the ToleranceRel of P by A1,A2,A3,A4,XBOOLE_0:def 5;
end;

registration
  let P be reflexive pcs-Str;
  cluster pcs-reverse(P) -> reflexive;
  coherence
  proof
    set R = pcs-reverse(P);
A1: the carrier of R = the carrier of P by Def40;
A2: the InternalRel of R = (the InternalRel of P)~ by Def40;
    the InternalRel of P is_reflexive_in the carrier of P by ORDERS_2:def 2;
    hence the InternalRel of R is_reflexive_in the carrier of R
    by A1,A2,ORDERS_1:79;
  end;
end;

registration
  let P be transitive pcs-Str;
  cluster pcs-reverse(P) -> transitive;
  coherence
  proof
    set R = pcs-reverse(P);
A1: the carrier of R = the carrier of P by Def40;
A2: the InternalRel of R = (the InternalRel of P)~ by Def40;
    the InternalRel of P is_transitive_in the carrier of P by ORDERS_2:def 3;
    hence the InternalRel of R is_transitive_in the carrier of R
    by A1,A2,ORDERS_1:80;
  end;
end;

registration
  let P be pcs-tol-reflexive pcs-Str;
  cluster pcs-reverse(P) -> pcs-tol-irreflexive;
  coherence
  proof
    set R = pcs-reverse(P);
A1: the carrier of R = the carrier of P by Def40;
A2: the ToleranceRel of R = (the ToleranceRel of P)` by Def40;
A3: the ToleranceRel of P is_reflexive_in the carrier of P by Def9;
    let x be set;
    assume x in the carrier of R;
    then [x,x] in the ToleranceRel of P by A1,A3,RELAT_2:def 1;
    hence thesis by A2,XBOOLE_0:def 5;
  end;
end;

registration
  let P be pcs-tol-irreflexive pcs-Str;
  cluster pcs-reverse(P) -> pcs-tol-reflexive;
  coherence
  proof
    set R = pcs-reverse(P);
A1: the carrier of R = the carrier of P by Def40;
A2: the ToleranceRel of R = (the ToleranceRel of P)` by Def40;
A3: the ToleranceRel of P is_irreflexive_in the carrier of P by Def10;
    let x be set;
    assume
A4: x in the carrier of R;
    then
A5: not [x,x] in the ToleranceRel of P by A1,A3,RELAT_2:def 2;
    [x,x] in [:the carrier of R,the carrier of R:] by A4,ZFMISC_1:87;
    hence thesis by A1,A2,A5,XBOOLE_0:def 5;
  end;
end;

registration
  let P be pcs-tol-symmetric pcs-Str;
  cluster pcs-reverse(P) -> pcs-tol-symmetric;
  coherence
  proof
    set R = pcs-reverse(P);
A1: the carrier of R = the carrier of P by Def40;
A2: the ToleranceRel of R = (the ToleranceRel of P)` by Def40;
A3: the ToleranceRel of P is_symmetric_in the carrier of P by Def11;
    let x, y be set;
    assume that
A4: x in the carrier of R and
A5: y in the carrier of R;
    assume [x,y] in the ToleranceRel of R;
    then not [x,y] in the ToleranceRel of P by A2,XBOOLE_0:def 5;
    then
A6: not [y,x] in the ToleranceRel of P by A1,A3,A4,A5,RELAT_2:def 3;
    [y,x] in [:the carrier of P,the carrier of P:] by A1,A4,A5,ZFMISC_1:87;
    hence thesis by A2,A6,XBOOLE_0:def 5;
  end;
end;

registration
  let P be pcs-compatible pcs-Str;
  cluster pcs-reverse(P) -> pcs-compatible;
  coherence
  proof
    set R = pcs-reverse(P);
A1: the carrier of R = the carrier of P by Def40;
A2: the InternalRel of R = (the InternalRel of P)~ by Def40;
A3: the ToleranceRel of R = (the ToleranceRel of P)` by Def40;
    let p, p9, q, q9 be Element of R such that
A4: [p,q] in the ToleranceRel of R and
A5: [p9,p] in the InternalRel of R and
A6: [q9,q] in the InternalRel of R;
A7: p9 in the carrier of R by A5,ZFMISC_1:87;
    reconsider p90 = p9, q90 = q9, p0 = p, q0 = q as Element of P by Def40;
    not [p0,q0] in the ToleranceRel of P by A3,A4,XBOOLE_0:def 5;
    then
A8: not p0 (--) q0 by Def7;
A9: [p0,p90] in the InternalRel of P by A2,A5,RELAT_1:def 7;
A10: [q0,q90] in the InternalRel of P by A2,A6,RELAT_1:def 7;
A11: p0 <= p90 by A9,ORDERS_2:def 5;
    q0 <= q90 by A10,ORDERS_2:def 5;
    then not p90 (--) q90 by A8,A11,Def22;
    then
A12: not [p90,q90] in the ToleranceRel of P by Def7;
    [p9,q9] in [:the carrier of P,the carrier of P:] by A1,A7,ZFMISC_1:87;
    hence [p9,q9] in the ToleranceRel of R by A3,A12,XBOOLE_0:def 5;
  end;
end;

:: Times

definition
  let P, Q be pcs-Str;
  func P pcs-times Q -> pcs-Str equals
  pcs-Str (# [: the carrier of P, the carrier of Q :],
    [" the InternalRel of P, the InternalRel of Q "],
    [^ the ToleranceRel of P, the ToleranceRel of Q ^] #);
  coherence;
end;

registration
  let P, Q be pcs-Str;
  cluster P pcs-times Q -> strict;
  coherence;
end;

registration
  let P, Q be non empty pcs-Str;
  cluster P pcs-times Q -> non empty;
  coherence;
end;

theorem
  for P, Q being pcs-Str, p, q being Element of P pcs-times Q
  for p1, p2 being Element of P, q1, q2 being Element of Q st
  p = [p1,q1] & q = [p2,q2] holds p <= q iff p1 <= p2 & q1 <= q2
proof
  let P, Q be pcs-Str, p, q be Element of P pcs-times Q;
  let p1, p2 be Element of P, q1, q2 be Element of Q such that
A1: p = [p1,q1] and
A2: q = [p2,q2];
  thus p <= q implies p1 <= p2 & q1 <= q2
  proof
    assume p <= q;
    then [p,q] in [" the InternalRel of P, the InternalRel of Q "]
    by ORDERS_2:def 5;
    then consider a, b, s, t being set such that
A3: p = [a,b] and
A4: q = [s,t] and
A5: [a,s] in the InternalRel of P and
A6: [b,t] in the InternalRel of Q by YELLOW_3:def 1;
A7: a = p1 by A1,A3,XTUPLE_0:1;
A8: b = q1 by A1,A3,XTUPLE_0:1;
    thus [p1,p2] in the InternalRel of P by A2,A4,A5,A7,XTUPLE_0:1;
    thus [q1,q2] in the InternalRel of Q by A2,A4,A6,A8,XTUPLE_0:1;
  end;
  assume that
A9: p1 <= p2 and
A10: q1 <= q2;
A11: [p1,p2] in the InternalRel of P by A9,ORDERS_2:def 5;
  [q1,q2] in the InternalRel of Q by A10,ORDERS_2:def 5;
  hence [p,q] in the InternalRel of P pcs-times Q by A1,A2,A11,YELLOW_3:def 1;
end;

theorem
  for P, Q being pcs-Str, p, q being Element of P pcs-times Q
  for p1, p2 being Element of P, q1, q2 being Element of Q st
  p = [p1,q1] & q = [p2,q2] holds p (--) q implies p1 (--) p2 or q1 (--) q2
proof
  let P, Q be pcs-Str, p, q be Element of P pcs-times Q;
  let p1, p2 be Element of P, q1, q2 be Element of Q such that
A1: p = [p1,q1] and
A2: q = [p2,q2];
  assume p (--) q;
  then [p,q] in [^ the ToleranceRel of P, the ToleranceRel of Q ^] by Def7;
  then consider a, b, c, d being set such that
A3: p = [a,b] and
A4: q = [c,d] and a in the carrier of P
  and b in the carrier of Q
  and c in the carrier of P
  and d in the carrier of Q and
A5: [a,c] in the ToleranceRel of P or [b,d] in the ToleranceRel of Q by Def2;
A6: a = p1 by A1,A3,XTUPLE_0:1;
A7: b = q1 by A1,A3,XTUPLE_0:1;
A8: c = p2 by A2,A4,XTUPLE_0:1;
  d = q2 by A2,A4,XTUPLE_0:1;
  hence thesis by A5,A6,A7,A8,Def7;
end;

theorem Th38:
  for P, Q being non empty pcs-Str, p, q being Element of P pcs-times Q
  for p1, p2 being Element of P, q1, q2 being Element of Q st
  p = [p1,q1] & q = [p2,q2] holds p1 (--) p2 or q1 (--) q2 implies p (--) q
proof
  let P, Q be non empty pcs-Str, p, q be Element of P pcs-times Q;
  let p1, p2 be Element of P, q1, q2 be Element of Q such that
A1: p = [p1,q1] and
A2: q = [p2,q2];
  assume p1 (--) p2 or q1 (--) q2;
  then [p1,p2] in the ToleranceRel of P or
  [q1,q2] in the ToleranceRel of Q by Def7;
  hence [p,q] in the ToleranceRel of P pcs-times Q by A1,A2,Def2;
end;

registration
  let P, Q be reflexive pcs-Str;
  cluster P pcs-times Q -> reflexive;
  coherence
  proof
    the RelStr of P pcs-times Q = [:P,Q:] by YELLOW_3:def 2;
    hence thesis by WAYBEL_8:12;
  end;
end;

registration
  let P, Q be transitive pcs-Str;
  cluster P pcs-times Q -> transitive;
  coherence
  proof
    the RelStr of P pcs-times Q = [:P,Q:] by YELLOW_3:def 2;
    hence thesis by WAYBEL_8:13;
  end;
end;

registration
  let P be pcs-Str;
  let Q be pcs-tol-reflexive pcs-Str;
  cluster P pcs-times Q -> pcs-tol-reflexive;
  coherence
  proof
    the TolStr of P pcs-times Q = [^P,Q^];
    hence thesis by Th3;
  end;
end;

registration
  let P be pcs-tol-reflexive pcs-Str;
  let Q be pcs-Str;
  cluster P pcs-times Q -> pcs-tol-reflexive;
  coherence
  proof
    the TolStr of P pcs-times Q = [^P,Q^];
    hence thesis by Th3;
  end;
end;

registration
  let P, Q be pcs-tol-symmetric pcs-Str;
  cluster P pcs-times Q -> pcs-tol-symmetric;
  coherence
  proof
    the TolStr of P pcs-times Q = [^P,Q^];
    hence thesis by Th5;
  end;
end;

registration
  let P, Q be pcs-compatible pcs-Str;
  cluster P pcs-times Q -> pcs-compatible;
  coherence
  proof
    set R = P pcs-times Q;
    set TR = the ToleranceRel of R;
    set D1 = the carrier of P;
    set D2 = the carrier of Q;
    let p, p9, q, q9 be Element of R such that
A1: p (--) q and
A2: p9 <= p and
A3: q9 <= q;
A4: [p,q] in TR by A1,Def7;
    then consider a, b, c, d being set such that
A5: p = [a,b] and
A6: q = [c,d] and
A7: a in D1 and
A8: b in D2 and
A9: c in D1 and
A10: d in D2 and
    [a,c] in the ToleranceRel of P or [b,d] in the ToleranceRel of Q by Def2;
A11: [p9,p] in the InternalRel of R by A2,ORDERS_2:def 5;
    then p9 in the carrier of R by ZFMISC_1:87;
    then consider e, f being set such that
A12: e in D1 and
A13: f in D2 and
A14: p9 = [e,f] by ZFMISC_1:def 2;
A15: [q9,q] in the InternalRel of R by A3,ORDERS_2:def 5;
    then q9 in the carrier of R by ZFMISC_1:87;
    then consider g, h being set such that
A16: g in D1 and
A17: h in D2 and
A18: q9 = [g,h] by ZFMISC_1:def 2;
    reconsider P, Q as non empty pcs-compatible pcs-Str by A7,A8;
    reconsider a, c, e, g as Element of P by A7,A9,A12,A16;
    reconsider b, d, f, h as Element of Q by A8,A10,A13,A17;
    [^a,b^] (--) [^c,d^] by A4,A5,A6,Def7;
    then
A19: a (--) c or b (--) d by Th6;
A20: the RelStr of P pcs-times Q = [:P,Q:] by YELLOW_3:def 2;
    then
A21: [e,f] <= [a,b] by A5,A11,A14,ORDERS_2:def 5;
    then
A22: e <= a by YELLOW_3:11;
A23: f <= b by A21,YELLOW_3:11;
A24: [g,h] <= [c,d] by A6,A15,A18,A20,ORDERS_2:def 5;
    then
A25: g <= c by YELLOW_3:11;
    h <= d by A24,YELLOW_3:11;
    then e (--) g or f (--) h by A19,A22,A23,A25,Def22;
    then
A26: [e,g] in the ToleranceRel of P or [f,h] in the ToleranceRel of Q by Def7;
A27: p9 = [e,f] by A14;
    q9 = [g,h] by A18;
    hence [p9,q9] in TR by A26,A27,Def3;
  end;
end;

definition
  let P, Q be pcs-Str;
  func P --> Q -> pcs-Str equals
  (pcs-reverse P) pcs-times Q;
  coherence;
end;

registration
  let P, Q be pcs-Str;
  cluster P --> Q -> strict;
  coherence;
end;

registration
  let P, Q be non empty pcs-Str;
  cluster P --> Q -> non empty;
  coherence;
end;

theorem
  for P, Q being pcs-Str, p, q being Element of P --> Q
  for p1, p2 being Element of P, q1, q2 being Element of Q st
  p = [p1,q1] & q = [p2,q2] holds p <= q iff p2 <= p1 & q1 <= q2
proof
  let P, Q be pcs-Str, p, q be Element of P --> Q;
  let p1, p2 be Element of P, q1, q2 be Element of Q such that
A1: p = [p1,q1] and
A2: q = [p2,q2];
  reconsider r1 = p1, r2 = p2 as Element of pcs-reverse P by Def40;
  thus p <= q implies p2 <= p1 & q1 <= q2
  proof
    assume p <= q;
    then [p,q] in ["the InternalRel of pcs-reverse P, the InternalRel of Q"]
    by ORDERS_2:def 5;
    then consider a, b, s, t being set such that
A3: p = [a,b] and
A4: q = [s,t] and
A5: [a,s] in the InternalRel of pcs-reverse P and
A6: [b,t] in the InternalRel of Q by YELLOW_3:def 1;
A7: a = p1 by A1,A3,XTUPLE_0:1;
A8: b = q1 by A1,A3,XTUPLE_0:1;
    s = p2 by A2,A4,XTUPLE_0:1;
    then r1 <= r2 by A5,A7,ORDERS_2:def 5;
    hence p2 <= p1 by Th33;
    thus [q1,q2] in the InternalRel of Q by A2,A4,A6,A8,XTUPLE_0:1;
  end;
  assume that
A9: p2 <= p1 and
A10: q1 <= q2;
  r1 <= r2 by A9,Th33;
  then
A11: [r1,r2] in the InternalRel of pcs-reverse P by ORDERS_2:def 5;
  [q1,q2] in the InternalRel of Q by A10,ORDERS_2:def 5;
  hence [p,q] in the InternalRel of P --> Q by A1,A2,A11,YELLOW_3:def 1;
end;

theorem
  for P, Q being pcs-Str, p, q being Element of P --> Q
  for p1, p2 being Element of P, q1, q2 being Element of Q st
  p = [p1,q1] & q = [p2,q2] holds p (--) q implies not p1 (--) p2 or q1 (--) q2
proof
  let P, Q be pcs-Str, p, q be Element of P --> Q;
  let p1, p2 be Element of P, q1, q2 be Element of Q such that
A1: p = [p1,q1] and
A2: q = [p2,q2];
  reconsider r1 = p1, r2 = p2 as Element of pcs-reverse P by Def40;
  assume [p,q] in the ToleranceRel of P --> Q;
  then consider a, b, s, t being set such that
A3: p = [a,b] and
A4: q = [s,t] and
  a in the carrier of pcs-reverse P and b in the carrier of Q
  and s in the carrier of pcs-reverse P
  and t in the carrier of Q and
A5: [a,s] in the ToleranceRel of pcs-reverse P or
  [b,t] in the ToleranceRel of Q by Def2;
A6: a = p1 by A1,A3,XTUPLE_0:1;
A7: b = q1 by A1,A3,XTUPLE_0:1;
A8: s = p2 by A2,A4,XTUPLE_0:1;
  t = q2 by A2,A4,XTUPLE_0:1;
  then r1 (--) r2 or q1 (--) q2 by A5,A6,A7,A8,Def7;
  hence thesis by Th34;
end;

theorem
  for P, Q being non empty pcs-Str, p, q being Element of P --> Q
  for p1, p2 being Element of P, q1, q2 being Element of Q st
  p = [p1,q1] & q = [p2,q2] holds not p1 (--) p2 or q1 (--) q2 implies p (--) q
proof
  let P, Q be non empty pcs-Str, p, q be Element of P --> Q;
  let p1, p2 be Element of P, q1, q2 be Element of Q such that
A1: p = [p1,q1] and
A2: q = [p2,q2];
  reconsider r1 = p1, r2 = p2 as Element of pcs-reverse P by Def40;
  reconsider w1 = [r1,q1], w2 = [r2,q2] as
  Element of (pcs-reverse P) pcs-times Q by A1,A2;
  assume not p1 (--) p2 or q1 (--) q2;
  then r1 (--) r2 or q1 (--) q2 by Th35;
  then w1 (--) w2 by Th38;
  hence thesis by A1,A2;
end;

registration
  let P, Q be reflexive pcs-Str;
  cluster P --> Q -> reflexive;
  coherence;
end;

registration
  let P, Q be transitive pcs-Str;
  cluster P --> Q -> transitive;
  coherence;
end;

registration
  let P be pcs-Str, Q be pcs-tol-reflexive pcs-Str;
  cluster P --> Q -> pcs-tol-reflexive;
  coherence;
end;

registration
  let P be pcs-tol-irreflexive pcs-Str, Q be pcs-Str;
  cluster P --> Q -> pcs-tol-reflexive;
  coherence;
end;

registration
  let P, Q be pcs-tol-symmetric pcs-Str;
  cluster P --> Q -> pcs-tol-symmetric;
  coherence;
end;

registration
  let P, Q be pcs-compatible pcs-Str;
  cluster P --> Q -> pcs-compatible;
  coherence;
end;

registration
  let P, Q be pcs;
  cluster P --> Q -> pcs-like;
  coherence;
end;

:: Self-coherence

definition
  let P be TolStr, S be Subset of P;
  attr S is pcs-self-coherent means
  :Def43:
  for x, y being Element of P st x in S & y in S holds x (--) y;
end;

registration
  let P be TolStr;
  cluster empty -> pcs-self-coherent for Subset of P;
  coherence
  proof
    let S be Subset of P;
    assume
A1: S is empty;
    let x be Element of P;
    thus thesis by A1;
  end;
end;

definition
  let P be TolStr, F be Subset-Family of P;
  attr F is pcs-self-coherent-membered means
  :Def44:
  for S being Subset of P st S in F holds S is pcs-self-coherent;
end;

registration
  let P be TolStr;
  cluster non empty pcs-self-coherent-membered for Subset-Family of P;
  existence
  proof
    reconsider F = {{}} as Subset-Family of P by SETFAM_1:46;
    take F;
    thus F is non empty;
    let S be Subset of P;
    assume S in F;
    then S = {}P by TARSKI:def 1;
    hence thesis;
  end;
end;

definition
  let P be RelStr, D be set;
  defpred P[set,set] means $1 in D & $2 in D &
  for a being set st a in $1 ex b being set st b in $2 &
  [a,b] in the InternalRel of P;
  func pcs-general-power-IR(P,D) -> Relation of D means
  :Def45:
  for A, B being set holds [A,B] in it iff A in D & B in D &
  for a being set st a in A ex b being set st b in B &
  [a,b] in the InternalRel of P;
  existence
  proof
    consider R being Relation of D such that
A1: for x, y being set holds [x,y] in R iff x in D & y in D & P[x,y]
    from RELSET_1:sch 1;
    take R;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let R1, R2 be Relation of D such that
A2: for A, B being set holds [A,B] in R1 iff A in D & B in D &
    for a being set st a in A ex b being set st b in B &
    [a,b] in the InternalRel of P and
A3: for A, B being set holds [A,B] in R2 iff A in D & B in D &
    for a being set st a in A ex b being set st b in B &
    [a,b] in the InternalRel of P;
A4: for a, b being set holds [a,b] in R1 iff P[a,b] by A2;
A5: for a, b being set holds [a,b] in R2 iff P[a,b] by A3;
    thus R1 = R2 from RELAT_1:sch 2(A4,A5);
  end;
end;

definition
  let P be TolStr, D be set;
  defpred Q[set,set] means $1 in D & $2 in D &
  for a, b being set st a in $1 & b in $2 holds [a,b] in the ToleranceRel of P;
  func pcs-general-power-TR(P,D) -> Relation of D means
  :Def46:
  for A, B being set holds [A,B] in it iff A in D & B in D &
  for a, b being set st a in A & b in B holds [a,b] in the ToleranceRel of P;
  existence
  proof
    consider R being Relation of D such that
A1: for x, y being set holds [x,y] in R iff x in D & y in D & Q[x,y]
    from RELSET_1:sch 1;
    take R;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let R1, R2 be Relation of D such that
A2: for A, B being set holds [A,B] in R1 iff A in D & B in D &
    for a, b being set st a in A & b in B holds [a,b] in the ToleranceRel of P
    and
A3: for A, B being set holds [A,B] in R2 iff A in D & B in D &
    for a, b being set st a in A & b in B holds [a,b] in the ToleranceRel of P;
A4: for a, b being set holds [a,b] in R1 iff Q[a,b] by A2;
A5: for a, b being set holds [a,b] in R2 iff Q[a,b] by A3;
    thus R1 = R2 from RELAT_1:sch 2(A4,A5);
  end;
end;

theorem
  for P being RelStr, D being Subset-Family of P
  for A, B being set holds [A,B] in pcs-general-power-IR(P,D) iff
  A in D & B in D &
  for a being Element of P st a in A ex b being Element of P st b in B & a <= b
proof
  let P be RelStr, D be Subset-Family of P;
  let A, B be set;
  thus [A,B] in pcs-general-power-IR(P,D) implies A in D & B in D &
  for a being Element of P st a in A ex b being Element of P st b in B &
  a <= b
  proof
    assume
A1: [A,B] in pcs-general-power-IR(P,D);
    hence
A2: A in D & B in D by Def45;
    let a be Element of P;
    assume a in A;
    then consider b being set such that
A3: b in B and
A4: [a,b] in the InternalRel of P by A1,Def45;
    reconsider b as Element of P by A2,A3;
    take b;
    thus thesis by A3,A4,ORDERS_2:def 5;
  end;
  assume that
A5: A in D and
A6: B in D and
A7: for a being Element of P st a in A ex b being Element of P st b in B &
  a <= b;
  for a being set st a in A ex b being set st b in B &
  [a,b] in the InternalRel of P
  proof
    let a be set;
    assume
A8: a in A;
    then reconsider a as Element of P by A5;
    consider b being Element of P such that
A9: b in B and
A10: a <= b by A7,A8;
    take b;
    thus thesis by A9,A10,ORDERS_2:def 5;
  end;
  hence thesis by A5,A6,Def45;
end;

theorem
  for P being TolStr, D being Subset-Family of P
  for A, B being set holds [A,B] in pcs-general-power-TR(P,D) iff
  A in D & B in D &
  for a, b being Element of P st a in A & b in B holds a (--) b
proof
  let P be TolStr, D be Subset-Family of P;
  let A, B be set;
  thus [A,B] in pcs-general-power-TR(P,D) implies A in D & B in D &
  for a, b being Element of P st a in A & b in B holds a (--) b
  proof
    assume
A1: [A,B] in pcs-general-power-TR(P,D);
    hence A in D & B in D by Def46;
    let a, b be Element of P;
    assume that
A2: a in A and
A3: b in B;
    [a,b] in the ToleranceRel of P by A1,A2,A3,Def46;
    hence thesis by Def7;
  end;
  assume that
A4: A in D and
A5: B in D and
A6: for a, b being Element of P st a in A & b in B holds a (--) b;
  for a, b being set st a in A & b in B holds [a,b] in the ToleranceRel of P
  proof
    let a, b be set;
    assume that
A7: a in A and
A8: b in B;
    reconsider a, b as Element of P by A4,A5,A7,A8;
    a (--) b by A6,A7,A8;
    hence thesis by Def7;
  end;
  hence thesis by A4,A5,Def46;
end;

definition
  let P be pcs-Str, D be set;
  func pcs-general-power(P,D) -> pcs-Str equals
  pcs-Str (# D, pcs-general-power-IR(P,D), pcs-general-power-TR(P,D) #);
  coherence;
end;

notation
  let P be pcs-Str, D be Subset-Family of P;
  synonym pcs-general-power(D) for pcs-general-power(P,D);
end;

registration
  let P be pcs-Str, D be non empty set;
  cluster pcs-general-power(P,D) -> non empty;
  coherence;
end;

theorem Th44:
  for P being pcs-Str, D be set
  for p, q being Element of pcs-general-power(P,D) holds p <= q
  implies for p9 being Element of P st p9 in p
  ex q9 being Element of P st q9 in q & p9 <= q9
proof
  let P be pcs-Str, D be set;
  set R = pcs-general-power(P,D);
  let p, q be Element of R;
  assume
A1: [p,q] in the InternalRel of R;
  let p9 be Element of P;
  assume p9 in p;
  then consider b being set such that
A2: b in q and
A3: [p9,b] in the InternalRel of P by A1,Def45;
  reconsider b as Element of P by A3,ZFMISC_1:87;
  take b;
  thus b in q & [p9,b] in the InternalRel of P by A2,A3;
end;

theorem
  for P being pcs-Str, D being non empty Subset-Family of P
  for p, q being Element of pcs-general-power(D) st
  for p9 being Element of P st p9 in p
  ex q9 being Element of P st q9 in q & p9 <= q9 holds p <= q
proof
  let P be pcs-Str, D be non empty Subset-Family of P;
  set R = pcs-general-power(D);
  let p, q be Element of R;
  assume
A1: for p9 being Element of P st p9 in p
  ex q9 being Element of P st q9 in q & p9 <= q9;
A2: p in D;
  for a being set st a in p ex b being set st b in q &
  [a,b] in the InternalRel of P
  proof
    let a be set;
    assume
A3: a in p;
    then reconsider a as Element of P by A2;
    consider q9 being Element of P such that
A4: q9 in q and
A5: a <= q9 by A1,A3;
    take q9;
    thus thesis by A4,A5,ORDERS_2:def 5;
  end;
  hence [p,q] in the InternalRel of R by Def45;
end;

theorem Th46:
  for P being pcs-Str, D being set
  for p, q being Element of pcs-general-power(P,D) holds p (--) q implies
  for p9, q9 being Element of P st p9 in p & q9 in q holds p9 (--) q9
proof
  let P be pcs-Str, D be set;
  set R = pcs-general-power(P,D);
  let p, q be Element of R;
  assume
A1: [p,q] in the ToleranceRel of R;
  let p9, q9 be Element of P;
  assume that
A2: p9 in p and
A3: q9 in q;
  thus [p9,q9] in the ToleranceRel of P by A1,A2,A3,Def46;
end;

theorem
  for P being pcs-Str, D being non empty Subset-Family of P
  for p, q being Element of pcs-general-power(D) st
  for p9, q9 being Element of P st p9 in p & q9 in q holds p9 (--) q9
  holds p (--) q
proof
  let P be pcs-Str, D be non empty Subset-Family of P;
  set R = pcs-general-power(D);
  let p, q be Element of R;
  assume
A1: for p9, q9 being Element of P st p9 in p & q9 in q holds p9 (--) q9;
A2: p in D;
A3: q in D;
  now
    let a, b be set;
    assume that
A4: a in p and
A5: b in q;
    reconsider a1 = a, b1 = b as Element of P by A2,A3,A4,A5;
    a1 (--) b1 by A1,A4,A5;
    hence [a,b] in the ToleranceRel of P by Def7;
  end;
  hence [p,q] in the ToleranceRel of R by Def46;
end;

registration
  let P be pcs-Str, D be set;
  cluster pcs-general-power(P,D) -> strict;
  coherence;
end;

registration
  let P be reflexive pcs-Str, D be Subset-Family of P;
  cluster pcs-general-power(D) -> reflexive;
  coherence
  proof
    set R = pcs-general-power(D);
    let x be set;
    assume
A1: x in the carrier of R;
    for a being set st a in x ex b being set st b in x &
    [a,b] in the InternalRel of P
    proof
      let a be set such that
A2:   a in x;
      take a;
      thus a in x by A2;
      field the InternalRel of P = the carrier of P by ORDERS_1:12;
      then the InternalRel of P is_reflexive_in the carrier of P by
RELAT_2:def 9;
      hence thesis by A1,A2,RELAT_2:def 1;
    end;
    hence thesis by A1,Def45;
  end;
end;

registration
  let P be transitive pcs-Str, D be set;
  cluster pcs-general-power(P,D) -> transitive;
  coherence
  proof
    set R = pcs-general-power(P,D);
    set IR = the InternalRel of R;
    let x, y, z be set;
    assume that
A1: x in the carrier of R and y in the carrier of R and
A2: z in the carrier of R and
A3: [x,y] in IR and
A4: [y,z] in IR;
    for a being set st a in x ex b being set st b in z &
    [a,b] in the InternalRel of P
    proof
      let a be set;
      assume a in x;
      then consider b being set such that
A5:   b in y and
A6:   [a,b] in the InternalRel of P by A3,Def45;
      consider c being set such that
A7:   c in z and
A8:   [b,c] in the InternalRel of P by A4,A5,Def45;
      take c;
      thus c in z by A7;
      A9:   the
 InternalRel of P is_transitive_in the carrier of P by ORDERS_2:def 3;
A10:  a in the carrier of P by A6,ZFMISC_1:87;
A11:  b in the carrier of P by A6,ZFMISC_1:87;
      c in the carrier of P by A8,ZFMISC_1:87;
      hence thesis by A6,A8,A9,A10,A11,RELAT_2:def 8;
    end;
    hence thesis by A1,A2,Def45;
  end;
end;

registration
  let P be pcs-tol-reflexive pcs-Str,
  D be pcs-self-coherent-membered Subset-Family of P;
  cluster pcs-general-power(D) -> pcs-tol-reflexive;
  coherence
  proof
    let x be set;
    assume
A1: x in the carrier of pcs-general-power(D);
    then reconsider x as Subset of P;
A2: x is pcs-self-coherent by A1,Def44;
    now
      let a, b be set such that
A3:   a in x and
A4:   b in x;
      reconsider a1 = a, b1 = b as Element of P by A3,A4;
      a1 (--) b1 by A2,A3,A4,Def43;
      hence [a,b] in the ToleranceRel of P by Def7;
    end;
    hence thesis by A1,Def46;
  end;
end;

registration
  let P be pcs-tol-symmetric pcs-Str, D be Subset-Family of P;
  cluster pcs-general-power(D) -> pcs-tol-symmetric;
  coherence
  proof
    set R = pcs-general-power(D);
    let x, y be set;
    assume
A1: x in the carrier of R;
    assume
A2: y in the carrier of R;
    assume
A3: [x,y] in the ToleranceRel of R;
    now
      let a, b be set such that
A4:   a in y and
A5:   b in x;
      reconsider a1 = a, b1 = b as Element of P by A1,A2,A4,A5;
      [b,a] in the ToleranceRel of P by A3,A4,A5,Def46;
      then b1 (--) a1 by Def7;
      hence [a,b] in the ToleranceRel of P by Def7;
    end;
    hence thesis by A1,A2,Def46;
  end;
end;

registration
  let P be pcs-compatible pcs-Str, D be Subset-Family of P;
  cluster pcs-general-power(D) -> pcs-compatible;
  coherence
  proof
    set R = pcs-general-power(D);
    let p, p9, q, q9 being Element of R such that
A1: p (--) q and
A2: p9 <= p and
A3: q9 <= q;
A4: [p9,p] in the InternalRel of R by A2,ORDERS_2:def 5;
A5: [q9,q] in the InternalRel of R by A3,ORDERS_2:def 5;
A6: p9 in the carrier of R by A4,ZFMISC_1:87;
A7: q9 in the carrier of R by A5,ZFMISC_1:87;
    now
      let a, b be set such that
A8:   a in p9 and
A9:   b in q9;
      reconsider a1 = a, b1 = b as Element of P by A6,A7,A8,A9;
      consider p1 being Element of P such that
A10:  p1 in p and
A11:  a1 <= p1 by A2,A8,Th44;
      consider q1 being Element of P such that
A12:  q1 in q and
A13:  b1 <= q1 by A3,A9,Th44;
      p1 (--) q1 by A1,A10,A12,Th46;
      then a1 (--) b1 by A11,A13,Def22;
      hence [a,b] in the ToleranceRel of P by Def7;
    end;
    hence [p9,q9] in the ToleranceRel of R by A6,Def46;
  end;
end;

definition
  let P be pcs-Str;
  func pcs-coherent-power(P) -> set equals
  {X where X is Subset of P: X is pcs-self-coherent};
  coherence;
end;

registration
  let P be pcs-Str;
  cluster pcs-self-coherent for Subset of P;
  existence
  proof
    take {}P;
    thus thesis;
  end;
end;

theorem Th48:
  for P being pcs-Str, X being set holds X in pcs-coherent-power(P)
  implies X is pcs-self-coherent Subset of P
proof
  let P be pcs-Str, X be set;
  assume X in pcs-coherent-power(P);
  then ex Y being Subset of P st X = Y & Y is pcs-self-coherent;
  hence thesis;
end;

registration
  let P be pcs-Str;
  cluster pcs-coherent-power(P) -> non empty;
  coherence
  proof
    {}P in pcs-coherent-power(P);
    hence thesis;
  end;
end;

definition
  let P be pcs-Str;
  redefine func pcs-coherent-power(P) -> Subset-Family of P;
  coherence
  proof
    pcs-coherent-power(P) c= bool the carrier of P
    proof
      let X be set;
      assume X in pcs-coherent-power(P);
      then X is Subset of P by Th48;
      hence thesis;
    end;
    hence thesis;
  end;
end;

registration
  let P be pcs-Str;
  cluster pcs-coherent-power(P) -> pcs-self-coherent-membered
    for Subset-Family of P;
  coherence
  proof
    pcs-coherent-power(P) is pcs-self-coherent-membered
    proof
      let S be Subset of P;
      thus thesis by Th48;
    end;
    hence thesis;
  end;
end;

definition
  let P be pcs-Str;
  func pcs-power(P) -> pcs-Str equals
  pcs-general-power(pcs-coherent-power(P));
  coherence;
end;

registration
  let P be pcs-Str;
  cluster pcs-power(P) -> strict;
  coherence;
end;

registration
  let P be pcs-Str;
  cluster pcs-power(P) -> non empty;
  coherence;
end;

registration
  let P be reflexive pcs-Str;
  cluster pcs-power(P) -> reflexive;
  coherence;
end;

registration
  let P be transitive pcs-Str;
  cluster pcs-power(P) -> transitive;
  coherence;
end;

registration
  let P be pcs-tol-reflexive pcs-Str;
  cluster pcs-power(P) -> pcs-tol-reflexive;
  coherence;
end;

registration
  let P be pcs-tol-symmetric pcs-Str;
  cluster pcs-power(P) -> pcs-tol-symmetric;
  coherence;
end;

registration
  let P be pcs-compatible pcs-Str;
  cluster pcs-power(P) -> pcs-compatible;
  coherence;
end;

registration
  let P be pcs;
  cluster pcs-power(P) -> pcs-like;
  coherence;
end;