pcs_0.miz

    begin

    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;

      :: original: field

      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;

      :: original: \/

      redefine

      func R \/ S -> Relation of (R1 \/ S1), (R2 \/ S2) ;

      coherence by ZFMISC_1: 119;

    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

        ( dom (R \/ S)) = (( dom R) \/ ( dom S)) by XTUPLE_0: 23

        .= (R1 \/ ( dom S)) by PARTFUN1:def 2

        .= (R1 \/ S1) by PARTFUN1:def 2;

        hence thesis;

      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 ;

    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 ;

    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 object 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 :: PCS_0:1



     Th1: for R1,S1 be set, R be transitive Relation of R1, S be 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 object;

      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;

      :: original: Carrier

      redefine

      :: PCS_0:def1

      func Carrier C -> ManySortedSet of I means

      : Def1: for i be 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 be 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 be 1-sorted st P = (C . i) & (X . i) = the carrier of P by A1, PRALG_1:def 15;

          hence thesis;

        end;

        assume

         A2: for i be Element of I holds (X . i) = the carrier of (C . i);

        for j be object st j in I holds (X . j) = (( Carrier C) . j)

        proof

          let j be object;

          assume

           b2: j in I;

          then

          reconsider jj = j as Element of I;



           B2: (X . j) = the carrier of (C . jj) by A2;

          I = ( dom C) by PARTFUN1:def 2;

          then ex R1 be 1-sorted st R1 = (C . j) & (( Carrier C) . j) = the carrier of R1 by b2, PRALG_1:def 14;

          hence thesis by B2;

        end;

        hence thesis by PBOOLE: 3;

      end;

      coherence

      proof

        ( dom ( Carrier C)) = I by PARTFUN1:def 2;

        hence thesis;

      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[ object, object] means ex r1,s1,r2,s2 be 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);

      :: PCS_0:def2

      func [^R,S^] -> Relation of [:R1, S1:], [:R2, S2:] means

      : Def2: for x,y be object holds [x, y] in it iff ex r1,s1,r2,s2 be 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 be Relation of [:R1, S1:], [:R2, S2:] such that

         A1: for x,y be object 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 object;

        thus [x, y] in Q implies P[x, y] by A1;

        given r1,s1,r2,s2 be 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 be object holds [x, y] in A iff P[x, y] and

         A11: for x,y be object 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;

      :: original: [^

      redefine

      :: PCS_0:def3

      func [^R,S^] means

      : Def3: for r1 be Element of R1, r2 be Element of R2 holds for s1 be Element of S1, s2 be 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 be Element of R1, r2 be Element of R2 holds for s1 be Element of S1, s2 be 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 be 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 be Element of R1, r2 be Element of R2 holds for s1 be Element of S1, s2 be Element of S2 holds [ [r1, s1], [r2, s2]] in f iff [r1, r2] in R or [s1, s2] in S;

        for x,y be object holds [x, y] in f iff [x, y] in [^R, S^]

        proof

          let x,y be object;

          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 be object 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 be object 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 be 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;

      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

        let x,y be object;

        thus [x, y] in ( dom [^R, S^]) implies [x, y] in [:R1, S1:];

        assume

         A1: [x, y] in [:R1, S1:];

        then

         A2: x in R1 by ZFMISC_1: 87;



         A3: y in S1 by A1, ZFMISC_1: 87;

        ( dom R) = R1 by PARTFUN1:def 2;

        then

        consider a be object such that

         A4: [x, a] in R by A2, XTUPLE_0:def 12;

        ( dom S) = S1 by PARTFUN1:def 2;

        then

        consider b be object such that

         A5: [y, b] in S by A3, 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 A2, A3, A4, A6, Def2;

        hence thesis by 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 object;

        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 be object such that

           A4: [x, y] in [^R, S^] by XTUPLE_0:def 12;

          consider p,q,s,t be 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;

            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;

            hence thesis by A5, A6, A7, Def2;

          end;

        end;

          suppose x in ( rng [^R, S^]);

          then

          consider y be object such that

           A9: [y, x] in [^R, S^] by XTUPLE_0:def 13;

          consider p,q,s,t be 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;

            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;

            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 object;

        assume x in ( field [^R, S^]);

        then

        consider x1,x2 be object 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;

        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 object;

        assume x in ( field [^R, S^]);

        then

        consider x1,x2 be object 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;

        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 object;

        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 be 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;

          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;

          hence thesis by A1, A2, A3, A4, A5, A6, Def2;

        end;

      end;

    end

    begin

    registration

      cluster empty -> total for RelStr;

      coherence ;

    end

    definition

      let R be Relation;

      :: PCS_0:def4

      attr R is transitive-yielding means

      : Def4: for S be RelStr st S in ( rng R) holds S is transitive;

    end

    registration

      cluster Poset-yielding -> transitive-yielding for Relation;

      coherence by YELLOW16:def 5;

    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;

      :: PCS_0:def5

      func pcs-InternalRels C -> ManySortedSet of I means

      : Def5: for i be set st i in I holds ex P be RelStr st P = (C . i) & (it . i) = the InternalRel of P;

      existence

      proof

        defpred P[ object, object] means ex R be RelStr st R = (C . $1) & $2 = the InternalRel of R;



         A1: for i be object st i in I holds ex j be object st P[i, j]

        proof

          let i be object;

          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 be Function such that

         A3: ( dom M) = I and

         A4: for i be object st i in I holds P[i, (M . i)] from CLASSES1:sch 1( A1);

        reconsider M as ManySortedSet of I by A3, PARTFUN1:def 2, RELAT_1:def 18;

        take M;

        thus thesis by A4;

      end;

      uniqueness

      proof

        let X,Y be ManySortedSet of I such that

         A5: for j be set st j in I holds ex R be RelStr st R = (C . j) & (X . j) = the InternalRel of R and

         A6: for j be set st j in I holds ex R be RelStr st R = (C . j) & (Y . j) = the InternalRel of R;

        for i be object st i in I holds (X . i) = (Y . i)

        proof

          let i be object;

          assume

           A7: i in I;

          then

           A8: ex R be RelStr st R = (C . i) & (X . i) = the InternalRel of R by A5;

          ex R be 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;

      :: original: pcs-InternalRels

      redefine

      :: PCS_0:def6

      func pcs-InternalRels C means

      : Def6: for i be 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 be 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 be RelStr st P = (C . i) & (X . i) = the InternalRel of P by A1, Def5;

          hence thesis;

        end;

        assume

         A2: for i be Element of I holds (X . i) = the InternalRel of (C . i);

        for i be set st i in I holds ex P be 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 be 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;

      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

    definition

      struct ( 1-sorted) TolStr (# the carrier -> set,

the ToleranceRel -> Relation of the carrier #)

       attr strict strict;

    end

    definition

      let P be TolStr;

      let p,q be Element of P;

      :: PCS_0:def7

      pred p (--) q means

      : Def7: [p, q] in the ToleranceRel of P;

    end

    definition

      let P be TolStr;

      :: PCS_0:def8

      attr P is pcs-tol-total means

      : Def8: the ToleranceRel of P is total;

      :: PCS_0:def9

      attr P is pcs-tol-reflexive means

      : Def9: the ToleranceRel of P is_reflexive_in the carrier of P;

      :: PCS_0:def10

      attr P is pcs-tol-irreflexive means

      : Def10: the ToleranceRel of P is_irreflexive_in the carrier of P;

      :: PCS_0:def11

      attr P is pcs-tol-symmetric means

      : Def11: the ToleranceRel of P is_symmetric_in the carrier of P;

    end

    definition

      :: PCS_0:def12

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

      coherence ;

    end

    registration

      cluster emptyTolStr -> empty strict;

      coherence ;

    end

    theorem :: PCS_0:2

    for P be 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;

        hence the ToleranceRel of P is total by ORDERS_1: 13;

      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;

        thus the ToleranceRel of P is_reflexive_in the carrier of P by A1;

        thus the ToleranceRel of P is_irreflexive_in the carrier of P by A1;

        thus the ToleranceRel of P is_symmetric_in the carrier of P by A1;

      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;

      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 object;

        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;

      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 object;

        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;

      end;

    end

    registration

      let L be pcs-tol-total TolStr;

      cluster the TolStr of L -> pcs-tol-total;

      coherence ;

    end

    definition

      let P be pcs-tol-symmetric TolStr;

      let p,q be Element of P;

      :: original: (--)

      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;

      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;

        let x be object;

        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;

      :: PCS_0:def13

      attr R is TolStr-yielding means for P be set st P in ( rng R) holds P is TolStr;

    end

    definition

      let f be Function;

      :: original: TolStr-yielding

      redefine

      :: PCS_0:def14

      attr f is TolStr-yielding means

      : Def14: for x be set st x in ( dom f) holds (f . x) is TolStr;

      compatibility

      proof

        thus f is TolStr-yielding implies for x be set st x in ( dom f) holds (f . x) is TolStr by FUNCT_1: 3;

        assume

         A1: for x be set st x in ( dom f) holds (f . x) is TolStr;

        let P be set;

        assume P in ( rng f);

        then ex x be object st x in ( dom f) & (f . x) = P by FUNCT_1:def 3;

        hence thesis by A1;

      end;

    end

    definition

      let I be set, f be ManySortedSet of I;



       A1: ( dom f) = I by PARTFUN1:def 2;

      :: original: TolStr-yielding

      redefine

      :: PCS_0:def15

      attr f is TolStr-yielding means for x be set st x in I holds (f . x) is TolStr;

      compatibility by A1;

    end

    definition

      let R be Relation;

      :: PCS_0:def16

      attr R is pcs-tol-reflexive-yielding means

      : Def16: for S be TolStr st S in ( rng R) holds S is pcs-tol-reflexive;

      :: PCS_0:def17

      attr R is pcs-tol-irreflexive-yielding means

      : Def17: for S be TolStr st S in ( rng R) holds S is pcs-tol-irreflexive;

      :: PCS_0:def18

      attr R is pcs-tol-symmetric-yielding means

      : Def18: for S be 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 ;

    end

    registration

      let I be set, P be TolStr;

      cluster (I --> P) -> TolStr-yielding;

      coherence by FUNCOP_1: 7;

    end

    registration

      let I be set, P be pcs-tol-reflexive TolStr;

      cluster (I --> P) -> pcs-tol-reflexive-yielding;

      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;

      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;

      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 object;

        thus thesis by A1;

      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;

      :: original: .

      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;

      :: PCS_0:def19

      func pcs-ToleranceRels C -> ManySortedSet of I means

      : Def19: for i be set st i in I holds ex P be TolStr st P = (C . i) & (it . i) = the ToleranceRel of P;

      existence

      proof

        defpred P[ object, object] means ex R be TolStr st R = (C . $1) & $2 = the ToleranceRel of R;



         A1: for i be object st i in I holds ex j be object st P[i, j]

        proof

          let i be object;

          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 be Function such that

         A3: ( dom M) = I and

         A4: for i be object st i in I holds P[i, (M . i)] from CLASSES1:sch 1( A1);

        reconsider M as ManySortedSet of I by A3, PARTFUN1:def 2, RELAT_1:def 18;

        take M;

        thus thesis by A4;

      end;

      uniqueness

      proof

        let X,Y be ManySortedSet of I such that

         A5: for j be set st j in I holds ex R be TolStr st R = (C . j) & (X . j) = the ToleranceRel of R and

         A6: for j be set st j in I holds ex R be TolStr st R = (C . j) & (Y . j) = the ToleranceRel of R;

        for i be object st i in I holds (X . i) = (Y . i)

        proof

          let i be object;

          assume

           A7: i in I;

          then

           A8: ex R be TolStr st R = (C . i) & (X . i) = the ToleranceRel of R by A5;

          ex R be 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;

      :: original: pcs-ToleranceRels

      redefine

      :: PCS_0:def20

      func pcs-ToleranceRels C means

      : Def20: for i be 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 be 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 be TolStr st P = (C . i) & (X . i) = the ToleranceRel of P by A1, Def19;

          hence thesis;

        end;

        assume

         A2: for i be Element of I holds (X . i) = the ToleranceRel of (C . i);

        for i be set st i in I holds ex P be 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 be 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;

      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;

      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;

      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 :: PCS_0:3



     Th3: for P,Q be TolStr st the TolStr of P = the TolStr of Q & P is pcs-tol-reflexive holds Q is pcs-tol-reflexive;

    theorem :: PCS_0:4



     Th4: for P,Q be TolStr st the TolStr of P = the TolStr of Q & P is pcs-tol-irreflexive holds Q is pcs-tol-irreflexive;

    theorem :: PCS_0:5



     Th5: for P,Q be TolStr st the TolStr of P = the TolStr of Q & P is pcs-tol-symmetric holds Q is pcs-tol-symmetric;

    definition

      let P,Q be TolStr;

      :: PCS_0:def21

      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;

      :: original: [^

      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^];

      :: original: ^`1

      redefine

      func p ^`1 -> Element of P ;

      coherence by MCART_1: 10;

      :: original: ^`2

      redefine

      func p ^`2 -> Element of Q ;

      coherence by MCART_1: 10;

    end

    theorem :: PCS_0:6



     Th6: for S1,S2 be non empty TolStr holds for a,c be Element of S1, b,d be Element of S2 holds [^a, b^] (--) [^c, d^] iff a (--) c or b (--) d by Def3;

    theorem :: PCS_0:7

    for S1,S2 be non empty TolStr, x,y be 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 be object 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 be object 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;

      y = [(y ^`1 ), (y ^`2 )] by A2;

      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 object;

        assume x in the carrier of [^P, Q^];

        then

        consider x1,x2 be object 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;

        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 object;

        assume x in the carrier of [^P, Q^];

        then

        consider x1,x2 be object 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;

        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 object;

        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;

      end;

    end

    begin

    definition

      struct ( RelStr, TolStr) pcs-Str (# the carrier -> set,

the InternalRel -> Relation of the carrier,

the ToleranceRel -> Relation of the carrier #)

       attr strict strict;

    end

    definition

      let P be pcs-Str;

      :: PCS_0:def22

      attr P is pcs-compatible means

      : Def22: for p,p9,q,q9 be Element of P st p (--) q & p9 <= p & q9 <= q holds p9 (--) q9;

    end

    definition

      let P be pcs-Str;

      :: PCS_0:def23

      attr P is pcs-like means P is reflexive transitive pcs-tol-reflexive pcs-tol-symmetric pcs-compatible;

      :: PCS_0:def24

      attr P is anti-pcs-like means 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 ;

      cluster reflexive transitive pcs-tol-reflexive pcs-tol-symmetric pcs-compatible -> pcs-like for pcs-Str;

      coherence ;

      cluster anti-pcs-like -> reflexive transitive pcs-tol-irreflexive pcs-tol-symmetric pcs-compatible for pcs-Str;

      coherence ;

      cluster reflexive transitive pcs-tol-irreflexive pcs-tol-symmetric pcs-compatible -> anti-pcs-like for pcs-Str;

      coherence ;

    end

    definition

      let D be set;

      :: PCS_0:def25

      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;

        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;

      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

      :: PCS_0:def26

      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;

      :: PCS_0:def27

      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;

      :: PCS_0:def28

      attr R is pcs-Str-yielding means for P be set st P in ( rng R) holds P is pcs-Str;

      :: PCS_0:def29

      attr R is pcs-yielding means for P be set st P in ( rng R) holds P is pcs;

    end

    definition

      let f be Function;

      :: original: pcs-Str-yielding

      redefine

      :: PCS_0:def30

      attr f is pcs-Str-yielding means for x be set st x in ( dom f) holds (f . x) is pcs-Str;

      compatibility

      proof

        thus f is pcs-Str-yielding implies for x be set st x in ( dom f) holds (f . x) is pcs-Str by FUNCT_1: 3;

        assume

         A1: for x be set st x in ( dom f) holds (f . x) is pcs-Str;

        let P be set;

        assume P in ( rng f);

        then ex x be object st x in ( dom f) & (f . x) = P by FUNCT_1:def 3;

        hence thesis by A1;

      end;

      :: original: pcs-yielding

      redefine

      :: PCS_0:def31

      attr f is pcs-yielding means for x be set st x in ( dom f) holds (f . x) is pcs;

      compatibility

      proof

        thus f is pcs-yielding implies for x be set st x in ( dom f) holds (f . x) is pcs by FUNCT_1: 3;

        assume

         A2: for x be set st x in ( dom f) holds (f . x) is pcs;

        let P be set;

        assume P in ( rng f);

        then ex x be object 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;

      :: original: pcs-Str-yielding

      redefine

      :: PCS_0:def32

      attr f is pcs-Str-yielding means

      : Def32: for x be set st x in I holds (f . x) is pcs-Str;

      compatibility by A1;

      :: original: pcs-yielding

      redefine

      :: PCS_0:def33

      attr f is pcs-yielding means

      : Def33: for x be set st x in I holds (f . x) is pcs;

      compatibility by A1;

    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 by A1;

        let y be set;

        thus thesis by A1;

      end;

      cluster pcs-yielding -> pcs-Str-yielding for Relation;

      coherence ;

      cluster pcs-yielding -> reflexive-yielding transitive-yielding pcs-tol-reflexive-yielding pcs-tol-symmetric-yielding for Relation;

      coherence ;

    end

    registration

      let I be set, P be pcs;

      cluster (I --> P) -> pcs-yielding;

      coherence by FUNCOP_1: 7;

    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;

      :: original: .

      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;

      :: original: .

      redefine

      func C . i -> pcs ;

      coherence by Def33;

    end

    definition

      let P,Q be pcs-Str;

      :: PCS_0:def34

      pred P c= Q means 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 :: PCS_0:8

    for P,Q be RelStr holds for p,q be Element of P, p1,q1 be Element of Q st the InternalRel of P c= the InternalRel of Q & p = p1 & q = q1 & p <= q holds p1 <= q1;

    theorem :: PCS_0:9

    for P,Q be TolStr holds for p,q be Element of P, p1,q1 be Element of Q st the ToleranceRel of P c= the ToleranceRel of Q & p = p1 & q = q1 & p (--) q holds p1 (--) q1;



     Lm2: for P,Q be pcs-Str holds for p be set st p in the carrier of P & P c= Q holds p is Element of Q;

    definition

      let C be Relation;

      :: PCS_0:def35

      attr C is pcs-chain-like means

      : Def35: for P,Q be 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;

      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;

      :: PCS_0:def36

      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 object;

          assume x in IR;

          then

          consider P be set such that

           A2: x in P and

           A3: P in ( rng IRA) by TARSKI:def 4;

          consider i be object such that

           A4: i in ( dom IRA) and

           A5: (IRA . i) = P by A3, FUNCT_1:def 3;

          consider R be RelStr such that

           A6: R = (C . i) and

           A7: (IRA . i) = the InternalRel of R by A4, Def5;

          consider x1,x2 be object 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 be 1-sorted st S = (C . i) & (CA . i) = the carrier of S by A4, PRALG_1:def 15;

          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 object;

          assume x in TR;

          then

          consider P be set such that

           A13: x in P and

           A14: P in ( rng TRA) by TARSKI:def 4;

          consider i be object such that

           A15: i in ( dom TRA) and

           A16: (TRA . i) = P by A14, FUNCT_1:def 3;

          consider R be TolStr such that

           A17: R = (C . i) and

           A18: (TRA . i) = the ToleranceRel of R by A15, Def19;

          consider x1,x2 be object 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 be 1-sorted st S = (C . i) & (CA . i) = the carrier of S by A15, PRALG_1:def 15;

          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 :: PCS_0:10



     Th10: for I be set, C be pcs-Str-yielding ManySortedSet of I holds for p,q be Element of ( pcs-union C) holds p <= q iff ex i be object, P be pcs-Str, p9,q9 be 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 be object, P be pcs-Str, p9,q9 be 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;

        then [p, q] in ( Union ( pcs-InternalRels C)) by Def36;

        then

        consider Z be set such that

         A2: [p, q] in Z and

         A3: Z in ( rng ( pcs-InternalRels C)) by TARSKI:def 4;

        consider i be object 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 be object, P be pcs-Str, p9,q9 be 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;

      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 :: PCS_0:11

    for I be non empty set, C be pcs-Str-yielding ManySortedSet of I holds for p,q be Element of ( pcs-union C) holds p <= q iff ex i be Element of I, p9,q9 be 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 be Element of I, p9,q9 be Element of (C . i) st p9 = p & q9 = q & p9 <= q9

      proof

        assume p <= q;

        then ex i be object, P be pcs-Str, p9,q9 be 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 :: PCS_0:12



     Th12: for I be set, C be pcs-Str-yielding ManySortedSet of I holds for p,q be Element of ( pcs-union C) holds p (--) q iff ex i be object, P be pcs-Str, p9,q9 be 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 be object, P be pcs-Str, p9,q9 be 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;

        then [p, q] in ( Union ( pcs-ToleranceRels C)) by Def36;

        then

        consider Z be set such that

         A2: [p, q] in Z and

         A3: Z in ( rng ( pcs-ToleranceRels C)) by TARSKI:def 4;

        consider i be object 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 be object, P be pcs-Str, p9,q9 be 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;

      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 :: PCS_0:13

    for I be non empty set, C be pcs-Str-yielding ManySortedSet of I holds for p,q be Element of ( pcs-union C) holds p (--) q iff ex i be Element of I, p9,q9 be 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 be Element of I, p9,q9 be Element of (C . i) st p9 = p & q9 = q & p9 (--) q9

      proof

        assume p (--) q;

        then ex i be object, P be pcs-Str, p9,q9 be 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 object;

        assume x in CP;

        then

        consider P be set such that

         A4: x in P and

         A5: P in ( rng CA) by A1, TARSKI:def 4;

        consider i be object such that

         A6: i in ( dom CA) and

         A7: (CA . i) = P by A5, FUNCT_1:def 3;



         A8: ex R be 1-sorted st (R = (C . i)) & ((CA . i) = the carrier of R) by A6, PRALG_1:def 15;

        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;

        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 object;

        assume x in CP;

        then

        consider P be set such that

         A4: x in P and

         A5: P in ( rng CA) by A1, TARSKI:def 4;

        consider i be object such that

         A6: i in ( dom CA) and

         A7: (CA . i) = P by A5, FUNCT_1:def 3;



         A8: ex R be 1-sorted st (R = (C . i)) & ((CA . i) = the carrier of R) by A6, PRALG_1:def 15;

        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;

        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 object;

        assume that x in CP and y in CP;

        assume [x, y] in TR;

        then

        consider P be set such that

         A2: [x, y] in P and

         A3: P in ( rng ( pcs-ToleranceRels C)) by A1, TARSKI:def 4;

        consider i be object 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;

        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 object;

          assume that x in CA and y in CA and z in CA;

          assume [x, y] in IR;

          then

          consider Z1 be set such that

           A4: [x, y] in Z1 and

           A5: Z1 in ( rng ( pcs-InternalRels C)) by A1, TARSKI:def 4;

          consider i be object 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 be set such that

           A8: [y, z] in Z2 and

           A9: Z2 in ( rng ( pcs-InternalRels C)) by A1, TARSKI:def 4;

          consider j be object 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);

            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;

            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);

            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;

            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;

        then

        consider Z1 be set such that

         A30: [p9, p] in Z1 and

         A31: Z1 in ( rng ( pcs-InternalRels C)) by A1, TARSKI:def 4;

        consider i be object 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;

        then

        consider Z2 be set such that

         A36: [q9, q] in Z2 and

         A37: Z2 in ( rng ( pcs-InternalRels C)) by A1, TARSKI:def 4;

        consider j be object 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;

        then

        consider Z3 be set such that

         A44: [p, q] in Z3 and

         A45: Z3 in ( rng ( pcs-ToleranceRels C)) by A2, TARSKI:def 4;

        consider k be object 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;

          the InternalRel of (C . i) c= the InternalRel of (C . j) by A56;

          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;



           A61: q9k <= qk by A36, A39, A41, A58;

          pk (--) qk by A44, A47, A48;

          then p9k (--) q9k by A60, A61, Def22;

          then [p9k, q9k] in the ToleranceRel of (C . k);

          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;



           A65: the InternalRel of (C . j) c= the InternalRel of (C . i) by A62;

           [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;



           A68: q9k <= qk by A64, A66;

          pk (--) qk by A44, A47, A48;

          then p9k (--) q9k by A67, A68, Def22;

          then [p9k, q9k] in the ToleranceRel of (C . k);

          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;



           A72: the ToleranceRel of (C . k) c= the ToleranceRel of (C . j) by A70;

          the InternalRel of (C . i) c= the InternalRel of (C . k) by A69;

          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;



           A76: q9j <= qj by A36, A39, A41;

          pj (--) qj by A44, A47, A48, A72;

          then p9j (--) q9j by A75, A76, Def22;

          then [p9j, q9j] in the ToleranceRel of (C . j);

          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;



           A80: the ToleranceRel of (C . i) c= the ToleranceRel of (C . j) by A78;



           A81: the ToleranceRel of (C . k) c= the ToleranceRel of (C . i) by A77;



           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;



           A83: p9j <= pj by A30, A33, A35, A79;



           A84: q9j <= qj by A36, A39, A41;

          pi1 (--) qi by A44, A47, A48, A81;

          then pj (--) qj by A80;

          then p9j (--) q9j by A83, A84, Def22;

          then [p9j, q9j] in the ToleranceRel of (C . j);

          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;



           A88: the ToleranceRel of (C . k) c= the ToleranceRel of (C . j) by A85;



           A89: the InternalRel of (C . j) c= the InternalRel of (C . i) by A86;

          reconsider q9i = q9 as Element of (C . i) by A42, A86;

          reconsider qi = q as Element of (C . i) by A43, A86;

          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;



           A90: p9i <= pi1 by A30, A33, A35;



           A91: q9i <= qi by A36, A39, A41, A89;

          pj (--) qj by A44, A47, A48, A88;

          then pi1 (--) qi by A87;

          then p9i (--) q9i by A90, A91, Def22;

          then [p9i, q9i] in the ToleranceRel of (C . i);

          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;



           A95: the InternalRel of (C . k) c= the InternalRel of (C . i) by A93;



           A96: the InternalRel of (C . j) c= the InternalRel of (C . k) by A92;

          reconsider q9k = q9 as Element of (C . k) by A42, A92;



           A97: the carrier of (C . j) c= the carrier of (C . k) by A92;

          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;



           A99: p9i <= pi1 by A30, A33, A35;



           A100: q9i <= qi by A95, A98;

          pi1 (--) qi by A44, A47, A48, A94;

          then p9i (--) q9i by A99, A100, Def22;

          then [p9i, q9i] in the ToleranceRel of (C . i);

          hence [p9, q9] in TR by A53;

        end;

      end;

    end

    definition

      let p,q be set;

      :: PCS_0:def37

      func <%p,q%> -> ManySortedSet of { 0 , 1} equals <%p, q%>;

      coherence by CARD_1: 50;

    end

    registration

      let P,Q be 1-sorted;

      cluster <%P, Q%> -> 1-sorted-yielding;

      coherence

      proof

        let x be object;

        assume x in ( dom <%P, Q%>);

        then x = 0 or x = 1 by TARSKI:def 2;

        hence thesis;

      end;

    end

     Lm3:

    now

      let a,b be object;

       <%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;

      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;

      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;

      end;

    end

    definition

      ::$Canceled

      let P,Q be pcs-Str;

      :: PCS_0:def39

      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 :: PCS_0:14



     Th14: for P,Q be 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: the carrier of S = ( Union ( Carrier f))

      proof

        thus the carrier of S c= ( Union ( Carrier f))

        proof

          let x be object;

          assume x in the carrier of S;

          then

           A5: x in the carrier of P or x in the carrier of Q by XBOOLE_0:def 3;



           A6: (( Carrier f) . z) = the carrier of (f . z) by Def1;



           A7: (( Carrier f) . j) = the carrier of (f . j) by Def1;



           A8: the carrier of P in ( rng ( Carrier f)) by A1, A6, FUNCT_1: 3;

          the carrier of Q in ( rng ( Carrier f)) by A1, A7, FUNCT_1: 3;

          hence thesis by A5, A8, TARSKI:def 4;

        end;

        let x be object;

        assume x in ( Union ( Carrier f));

        then

        consider Z be set such that

         A9: x in Z and

         A10: Z in ( rng ( Carrier f)) by TARSKI:def 4;

        consider i be object such that

         A11: i in ( dom ( Carrier f)) and

         A12: (( Carrier f) . i) = Z by A10, FUNCT_1:def 3;

        i = 0 or i = 1 by A11, TARSKI:def 2;

        then Z = the carrier of (f . z) or Z = the carrier of (f . j) by A12, Def1;

        hence thesis by A9, XBOOLE_0:def 3;

      end;



       A13: the InternalRel of S = ( Union ( pcs-InternalRels f))

      proof

        thus the InternalRel of S c= ( Union ( pcs-InternalRels f))

        proof

          let x be object;

          assume x in the InternalRel of S;

          then

           A14: x in the InternalRel of P or x in the InternalRel of Q by XBOOLE_0:def 3;



           A15: (( pcs-InternalRels f) . z) = the InternalRel of (f . z) by Def6;



           A16: (( pcs-InternalRels f) . j) = the InternalRel of (f . j) by Def6;



           A17: the InternalRel of P in ( rng ( pcs-InternalRels f)) by A2, A15, FUNCT_1: 3;

          the InternalRel of Q in ( rng ( pcs-InternalRels f)) by A2, A16, FUNCT_1: 3;

          hence thesis by A14, A17, TARSKI:def 4;

        end;

        let x be object;

        assume x in ( Union ( pcs-InternalRels f));

        then

        consider Z be set such that

         A18: x in Z and

         A19: Z in ( rng ( pcs-InternalRels f)) by TARSKI:def 4;

        consider i be object such that

         A20: i in ( dom ( pcs-InternalRels f)) and

         A21: (( pcs-InternalRels f) . i) = Z by A19, FUNCT_1:def 3;

        i = 0 or i = 1 by A20, TARSKI:def 2;

        then Z = the InternalRel of (f . z) or Z = the InternalRel of (f . j) by A21, Def6;

        hence thesis by A18, 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 object;

          assume x in the ToleranceRel of S;

          then

           A22: x in the ToleranceRel of P or x in the ToleranceRel of Q by XBOOLE_0:def 3;



           A23: (( pcs-ToleranceRels f) . z) = the ToleranceRel of (f . z) by Def20;



           A24: (( pcs-ToleranceRels f) . j) = the ToleranceRel of (f . j) by Def20;



           A25: the ToleranceRel of P in ( rng ( pcs-ToleranceRels f)) by A3, A23, FUNCT_1: 3;

          the ToleranceRel of Q in ( rng ( pcs-ToleranceRels f)) by A3, A24, FUNCT_1: 3;

          hence thesis by A22, A25, TARSKI:def 4;

        end;

        let x be object;

        assume x in ( Union ( pcs-ToleranceRels f));

        then

        consider Z be set such that

         A26: x in Z and

         A27: Z in ( rng ( pcs-ToleranceRels f)) by TARSKI:def 4;

        consider i be object such that

         A28: i in ( dom ( pcs-ToleranceRels f)) and

         A29: (( pcs-ToleranceRels f) . i) = Z by A27, FUNCT_1:def 3;

        i = 0 or i = 1 by A28, TARSKI:def 2;

        then Z = the ToleranceRel of (f . z) or Z = the ToleranceRel of (f . j) by A29, Def20;

        hence thesis by A26, XBOOLE_0:def 3;

      end;

      hence thesis by A4, A13, Def36;

    end;

    theorem :: PCS_0:15



     Th15: for P,Q be 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 :: PCS_0:16

    for P,Q be pcs-Str, p,q be Element of ( pcs-sum (P,Q)) holds p <= q iff (ex p9,q9 be Element of P st p9 = p & q9 = q & p9 <= q9) or ex p9,q9 be 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 be Element of P st p9 = p & q9 = q & p9 <= q9) or ex p9,q9 be 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;

          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;

          hence thesis;

        end;

      end;

      assume

       A5: (ex p9,q9 be Element of P st p9 = p & q9 = q & p9 <= q9) or ex p9,q9 be Element of Q st p9 = p & q9 = q & p9 <= q9;

      per cases by A5;

        suppose ex p9,q9 be Element of P st p9 = p & q9 = q & p9 <= q9;

        then

        consider p9,q9 be 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;

        hence [p, q] in the InternalRel of R by A1, A6, A7, XBOOLE_0:def 3;

      end;

        suppose ex p9,q9 be Element of Q st p9 = p & q9 = q & p9 <= q9;

        then

        consider p9,q9 be 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;

        hence [p, q] in the InternalRel of R by A1, A9, A10, XBOOLE_0:def 3;

      end;

    end;

    theorem :: PCS_0:17

    for P,Q be pcs-Str, p,q be Element of ( pcs-sum (P,Q)) holds p (--) q iff (ex p9,q9 be Element of P st p9 = p & q9 = q & p9 (--) q9) or ex p9,q9 be 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 be Element of P st p9 = p & q9 = q & p9 (--) q9) or ex p9,q9 be 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;

          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;

          hence thesis;

        end;

      end;

      assume

       A5: (ex p9,q9 be Element of P st p9 = p & q9 = q & p9 (--) q9) or ex p9,q9 be Element of Q st p9 = p & q9 = q & p9 (--) q9;

      per cases by A5;

        suppose ex p9,q9 be Element of P st p9 = p & q9 = q & p9 (--) q9;

        then

        consider p9,q9 be 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;

        hence [p, q] in the ToleranceRel of R by A1, A6, A7, XBOOLE_0:def 3;

      end;

        suppose ex p9,q9 be Element of Q st p9 = p & q9 = q & p9 (--) q9;

        then

        consider p9,q9 be 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;

        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 :: PCS_0:18



     Th18: for P,Q be 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 :: PCS_0:19



     Th19: for P,Q be 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;

      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;



         A11: [p9, p] in R by A3, A5;



         A12: [q9, q] in R by A4, A5;

        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;

        q91 <= q1 by A14;

        then p91 (--) q91 by A10, A15, Def22;

        then [p91, q91] in T1;

        then [p91, q91] in T by XBOOLE_0:def 3;

        hence p9 (--) q9 by A5;

      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;



         A20: [p9, p] in R by A3, A5;



         A21: [q9, q] in R by A4, A5;

        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;

        q91 <= q1 by A23;

        then p91 (--) q91 by A19, A24, Def22;

        then [p91, q91] in T2;

        then [p91, q91] in T by XBOOLE_0:def 3;

        hence p9 (--) q9 by A5;

      end;

    end;

    theorem :: PCS_0:20

    for P,Q be 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;

      then

       A3: R is transitive;

      R is pcs-compatible by A1, Th19;

      hence thesis by A3;

    end;

    definition

      let P be pcs-Str, a be set;

      :: PCS_0:def40

      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:];

        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;

        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 :: PCS_0:21



     Th21: for P be pcs-Str, a be 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 :: PCS_0:22

    for P be pcs-Str, a be set, p,q be 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 :: PCS_0:23



     Th23: for P be pcs-Str, a be set, p,q be Element of P, p1,q1 be 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 :: PCS_0:24



     Th24: for P be pcs-Str, a be set, p be Element of P, p1,q1 be 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;

      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, ZFMISC_1: 105;

    end;

    theorem :: PCS_0:25



     Th25: for P be pcs-Str, a be set, p be 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 :: PCS_0:26



     Th26: for P be pcs-Str, a be set, p,q be Element of P, p1,q1 be 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;

      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 :: PCS_0:27



     Th27: for P be pcs-Str, a be set, p,q be 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 :: PCS_0:28



     Th28: for P be pcs-Str, a be set, p,q be Element of P, p1,q1 be 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 :: PCS_0:29



     Th29: for P be pcs-Str, a be set, p,q be Element of P, p1,q1 be 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;

      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, ZFMISC_1: 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 object;

        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;

          hence thesis by A2, XBOOLE_0:def 3;

        end;

      end;

    end

    theorem :: PCS_0:30



     Th30: for P be transitive pcs-Str, a be 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 object;

      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;



       A10: y <= z by A7;

      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;

      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 object;

        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;

          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 object;

        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;

          hence thesis by A1, XBOOLE_0:def 3;

        end;

      end;

    end

    theorem :: PCS_0:31



     Th31: for P be pcs-compatible pcs-Str, a be 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 :: PCS_0:32

    for P be pcs, a be 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;

    definition

      let P be pcs-Str;

      :: PCS_0:def41

      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 :: PCS_0:33



     Th33: for P be pcs-Str, p,q be Element of P holds for p9,q9 be 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 by A1, A2, A3, RELAT_1:def 7;

      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 :: PCS_0:34



     Th34: for P be pcs-Str, p,q be Element of P holds for p9,q9 be 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 :: PCS_0:35



     Th35: for P be non empty pcs-Str, p,q be Element of P holds for p9,q9 be 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 object;

        assume x in the carrier of R;

        then [x, x] in the ToleranceRel of P by A1, A3;

        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 object;

        assume

         A4: x in the carrier of R;

        then

         A5: not [x, x] in the ToleranceRel of P by A1, A3;

         [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 object;

        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;

         [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;



         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;

        q0 <= q90 by A10;

        then not p90 (--) q90 by A8, A11, Def22;

        then

         A12: not [p90, q90] in the ToleranceRel of P;

         [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

    definition

      let P,Q be pcs-Str;

      :: PCS_0:def42

      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 :: PCS_0:36

    for P,Q be pcs-Str, p,q be Element of (P pcs-times Q) holds for p1,p2 be Element of P, q1,q2 be 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"];

        then

        consider a,b,s,t be object 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;

       [q1, q2] in the InternalRel of Q by A10;

      hence [p, q] in the InternalRel of (P pcs-times Q) by A1, A2, A11, YELLOW_3:def 1;

    end;

    theorem :: PCS_0:37

    for P,Q be pcs-Str, p,q be Element of (P pcs-times Q) holds for p1,p2 be Element of P, q1,q2 be 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^];

      then

      consider a,b,c,d be 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;

    end;

    theorem :: PCS_0:38



     Th38: for P,Q be non empty pcs-Str, p,q be Element of (P pcs-times Q) holds for p1,p2 be Element of P, q1,q2 be Element of Q st p = [p1, q1] & q = [p2, q2] holds p1 (--) p2 or q1 (--) q2 implies p (--) q by Def2;

    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;

        then

        consider a,b,c,d be 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;

        then p9 in the carrier of R by ZFMISC_1: 87;

        then

        consider e,f be object 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;

        then q9 in the carrier of R by ZFMISC_1: 87;

        then

        consider g,h be object 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;

        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;

        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;

        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;



         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;

      :: PCS_0:def43

      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 :: PCS_0:39

    for P,Q be pcs-Str, p,q be Element of (P --> Q) holds for p1,p2 be Element of P, q1,q2 be 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"];

        then

        consider a,b,s,t be object 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;

        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);

       [q1, q2] in the InternalRel of Q by A10;

      hence [p, q] in the InternalRel of (P --> Q) by A1, A2, A11, YELLOW_3:def 1;

    end;

    theorem :: PCS_0:40

    for P,Q be pcs-Str, p,q be Element of (P --> Q) holds for p1,p2 be Element of P, q1,q2 be 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 be 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;

      hence thesis by Th34;

    end;

    theorem :: PCS_0:41

    for P,Q be non empty pcs-Str, p,q be Element of (P --> Q) holds for p1,p2 be Element of P, q1,q2 be 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

    definition

      let P be TolStr, S be Subset of P;

      :: PCS_0:def44

      attr S is pcs-self-coherent means for x,y be 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 ;

    end

    definition

      let P be TolStr, F be Subset-Family of P;

      :: PCS_0:def45

      attr F is pcs-self-coherent-membered means

      : Def44: for S be 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 be set st a in $1 holds ex b be set st b in $2 & [a, b] in the InternalRel of P;

      :: PCS_0:def46

      func pcs-general-power-IR (P,D) -> Relation of D means

      : Def45: for A,B be set holds [A, B] in it iff A in D & B in D & for a be set st a in A holds ex b be set st b in B & [a, b] in the InternalRel of P;

      existence

      proof

        consider R be Relation of D such that

         A1: for x,y be set holds [x, y] in R iff x in D & y in D & P[x, y] from RELSET_1:sch 5;

        take R;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let R1,R2 be Relation of D such that

         A2: for A,B be set holds [A, B] in R1 iff A in D & B in D & for a be set st a in A holds ex b be set st b in B & [a, b] in the InternalRel of P and

         A3: for A,B be set holds [A, B] in R2 iff A in D & B in D & for a be set st a in A holds ex b be set st b in B & [a, b] in the InternalRel of P;

        let x,y be object;

        reconsider a = x, b = y as set by TARSKI: 1;



         A4: [a, b] in R1 iff P[a, b] by A2;

         [a, b] in R2 iff P[a, b] by A3;

        hence [x, y] in R1 iff [x, y] in R2 by A4;

      end;

    end

    definition

      let P be TolStr, D be set;

      defpred Q[ set, set] means $1 in D & $2 in D & for a,b be set st a in $1 & b in $2 holds [a, b] in the ToleranceRel of P;

      :: PCS_0:def47

      func pcs-general-power-TR (P,D) -> Relation of D means

      : Def46: for A,B be set holds [A, B] in it iff A in D & B in D & for a,b be set st a in A & b in B holds [a, b] in the ToleranceRel of P;

      existence

      proof

        consider R be Relation of D such that

         A1: for x,y be set holds [x, y] in R iff x in D & y in D & Q[x, y] from RELSET_1:sch 5;

        take R;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let R1,R2 be Relation of D such that

         A2: for A,B be set holds [A, B] in R1 iff A in D & B in D & for a,b be set st a in A & b in B holds [a, b] in the ToleranceRel of P and

         A3: for A,B be set holds [A, B] in R2 iff A in D & B in D & for a,b be set st a in A & b in B holds [a, b] in the ToleranceRel of P;

        let x,y be object;

        reconsider a = x, b = y as set by TARSKI: 1;



         A4: [a, b] in R1 iff Q[a, b] by A2;

         [a, b] in R2 iff Q[a, b] by A3;

        hence [x, y] in R1 iff [x, y] in R2 by A4;

      end;

    end

    theorem :: PCS_0:42

    for P be RelStr, D be Subset-Family of P holds for A,B be set holds [A, B] in ( pcs-general-power-IR (P,D)) iff A in D & B in D & for a be Element of P st a in A holds ex b be 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 be Element of P st a in A holds ex b be 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 be 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;

      end;

      assume that

       A5: A in D and

       A6: B in D and

       A7: for a be Element of P st a in A holds ex b be Element of P st b in B & a <= b;

      for a be set st a in A holds ex b be 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 be Element of P such that

         A9: b in B and

         A10: a <= b by A7, A8;

        take b;

        thus thesis by A9, A10;

      end;

      hence thesis by A5, A6, Def45;

    end;

    theorem :: PCS_0:43

    for P be TolStr, D be Subset-Family of P holds for A,B be set holds [A, B] in ( pcs-general-power-TR (P,D)) iff A in D & B in D & for a,b be 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 be Element of P st a in A & b in B holds a (--) b by Def46;

      assume that

       A1: A in D and

       A2: B in D and

       A3: for a,b be Element of P st a in A & b in B holds a (--) b;

      for a,b be set st a in A & b in B holds [a, b] in the ToleranceRel of P by A1, A2, A3, Def7;

      hence thesis by A1, A2, Def46;

    end;

    definition

      let P be pcs-Str, D be set;

      :: PCS_0:def48

      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 :: PCS_0:44



     Th44: for P be pcs-Str, D be set holds for p,q be Element of ( pcs-general-power (P,D)) holds p <= q implies for p9 be Element of P st p9 in p holds ex q9 be 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 be 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 :: PCS_0:45

    for P be pcs-Str, D be non empty Subset-Family of P holds for p,q be Element of ( pcs-general-power D) st for p9 be Element of P st p9 in p holds ex q9 be 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 be Element of P st p9 in p holds ex q9 be Element of P st q9 in q & p9 <= q9;



       A2: p in D;

      for a be set st a in p holds ex b be 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 be Element of P such that

         A4: q9 in q and

         A5: a <= q9 by A1, A3;

        take q9;

        thus thesis by A4, A5;

      end;

      hence [p, q] in the InternalRel of R by Def45;

    end;

    theorem :: PCS_0:46



     Th46: for P be pcs-Str, D be set holds for p,q be Element of ( pcs-general-power (P,D)) holds p (--) q implies for p9,q9 be Element of P st p9 in p & q9 in q holds p9 (--) q9 by Def46;

    theorem :: PCS_0:47

    for P be pcs-Str, D be non empty Subset-Family of P holds for p,q be Element of ( pcs-general-power D) st for p9,q9 be 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 be Element of P st p9 in p & q9 in q holds p9 (--) q9;



       A2: p in D;



       A3: q in D;

      for a,b be set st a in p & b in q holds [a, b] in the ToleranceRel of P by A1, A2, A3, Def7;

      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 object;

        assume

         A1: x in the carrier of R;

        reconsider x as set by TARSKI: 1;

        for a be set st a in x holds ex b be 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;

        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 object;

        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;

        reconsider x, y, z as set by TARSKI: 1;

        for a be set st a in x holds ex b be set st b in z & [a, b] in the InternalRel of P

        proof

          let a be set;

          assume a in x;

          then

          consider b be set such that

           A5: b in y and

           A6: [a, b] in the InternalRel of P by A3, Def45;

          consider c be 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;

        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 object;

        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;

        for a,b be set st a in x & b in x holds [a, b] in the ToleranceRel of P by A2, Def7;

        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 object;

        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;

        reconsider x, y as set by TARSKI: 1;

        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;

          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 be 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;



         A5: [q9, q] in the InternalRel of R by A3;



         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 be Element of P such that

           A10: p1 in p and

           A11: a1 <= p1 by A2, A8, Th44;

          consider q1 be 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;

        end;

        hence [p9, q9] in the ToleranceRel of R by A6, Def46;

      end;

    end

    definition

      let P be pcs-Str;

      :: PCS_0:def49

      func pcs-coherent-power (P) -> set equals { X where X be 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 :: PCS_0:48



     Th48: for P be pcs-Str, X be 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 be 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;

      :: original: pcs-coherent-power

      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 object;

          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;

      coherence by Th48;

    end

    definition

      let P be pcs-Str;

      :: PCS_0:def50

      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