:: Basic Operations on Preordered Coherent Spaces
:: by Klaus E. Grue and Artur Korni{\l}owicz
::
:: Received August 28, 2007
:: Copyright (c) 2007-2012 Association of Mizar Users


begin

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

definition
let R1, R2 be set ;
let R be Relation of R1,R2;
:: original:field
redefine func field R ->  Subset of (R1 \/ R2);
coherence
 field R is Subset of (R1 \/ R2) 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 funcR \/ S ->  Relation of (R1 \/ S1),(R2 \/ S2);
coherence
 R \/ S is Relation of (R1 \/ S1),(R2 \/ S2) 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;
clusterR \/ S ->  total for Relation of (R1 \/ S1);
coherence
 for b1 being Relation of (R1 \/ S1) st b1 = R \/ S holds
b1 is total
proofend;
end;

registration
let R1, S1 be set ;
let R be reflexive Relation of R1;
let S be reflexive Relation of S1;
clusterR \/ S ->  reflexive for Relation of (R1 \/ S1);
coherence
 for b1 being Relation of (R1 \/ S1) st b1 = R \/ S holds
b1 is reflexive ;
end;

registration
let R1, S1 be set ;
let R be symmetric Relation of R1;
let S be symmetric Relation of S1;
clusterR \/ S ->  symmetric for Relation of (R1 \/ S1);
coherence
 for b1 being Relation of (R1 \/ S1) st b1 = R \/ S holds
b1 is symmetric ;
end;

Lm1: now__::_thesis:_for_R1,_S1_being_set_
for_R_being_Relation_of_R1
for_S_being_Relation_of_S1_st_R1_misses_S1_holds_
for_q1,_q2_being_set_st_[q1,q2]_in_R_\/_S_&_q2_in_S1_holds_
(_[q1,q2]_in_S_&_q1_in_S1_)
let R1, S1 be set ; ::_thesis: for R being Relation of R1
for S being Relation of S1 st R1 misses S1 holds
for q1, q2 being set st [q1,q2] in R \/ S & q2 in S1 holds
( [q1,q2] in S & q1 in S1 )
let R be Relation of R1; ::_thesis: for S being Relation of S1 st R1 misses S1 holds
for q1, q2 being set st [q1,q2] in R \/ S & q2 in S1 holds
( [q1,q2] in S & q1 in S1 )
let S be Relation of S1; ::_thesis: ( R1 misses S1 implies for q1, q2 being set st [q1,q2] in R \/ S & q2 in S1 holds
( [q1,q2] in S & q1 in S1 ) )
assume A1: R1 misses S1 ; ::_thesis: for q1, q2 being set st [q1,q2] in R \/ S & q2 in S1 holds
( [q1,q2] in S & q1 in S1 )
let q1, q2 be set ; ::_thesis: ( [q1,q2] in R \/ S & q2 in S1 implies ( [q1,q2] in S & q1 in S1 ) )
assume that
A2: [q1,q2] in R \/ S and
A3: q2 in S1 ; ::_thesis: ( [q1,q2] in S & q1 in S1 )
A4: ( [q1,q2] in R or [q1,q2] in S ) by A2, XBOOLE_0:def_3;
now__::_thesis:_not_[q1,q2]_in_R
assume  [q1,q2] in R ; ::_thesis: contradiction
then  q2 in R1 by ZFMISC_1:87;
hence  contradiction by A1, A3, XBOOLE_0:3; ::_thesis: verum
end;
hence  ( [q1,q2] in S & q1 in S1 ) by A4, ZFMISC_1:87; ::_thesis: verum
end;

theorem Th1: :: PCS_0:1
for R1, S1 being set
for R being transitive Relation of R1
for S being transitive Relation of S1 st R1 misses S1 holds
R \/ S is transitive
proofend;

definition
let I be non empty set ;
let C be 1-sorted-yielding ManySortedSet of I;
redefine func Carrier C means :Def1: :: PCS_0:def 1
 for i being Element of I holds it . i = the carrier of (C . i);
compatibility
 for b1 being set holds
( b1 = Carrier C iff for i being Element of I holds b1 . i = the carrier of (C . i) )
proofend;
end;

:: deftheorem Def1 defines Carrier PCS_0:def_1_:_
 for I being non empty set
for C being 1-sorted-yielding ManySortedSet of I
for b3 being set holds
( b3 = Carrier C iff for i being Element of I holds b3 . i = the carrier of (C . i) );

definition
let R1, R2, S1, S2 be set ;
let R be Relation of R1,R2;
let S be Relation of S1,S2;
defpred S1[ set , set ] means  ex r1, s1, r2, s2 being set st
( $1 = [r1,s1] & $2 = [r2,s2] & r1 in R1 & s1 in S1 & r2 in R2 & s2 in S2 & ( [r1,r2] in R or [s1,s2] in S ) );
func[^R,S^] ->  Relation of [:R1,S1:],[:R2,S2:] means :Def2: :: PCS_0:def 2
 for x, y being set holds
( [x,y] in it iff ex r1, s1, r2, s2 being set st
( x = [r1,s1] & y = [r2,s2] & r1 in R1 & s1 in S1 & r2 in R2 & s2 in S2 & ( [r1,r2] in R or [s1,s2] in S ) ) );
existence
 ex b1 being Relation of [:R1,S1:],[:R2,S2:] st
for x, y being set holds
( [x,y] in b1 iff ex r1, s1, r2, s2 being set st
( x = [r1,s1] & y = [r2,s2] & r1 in R1 & s1 in S1 & r2 in R2 & s2 in S2 & ( [r1,r2] in R or [s1,s2] in S ) ) )
proofend;
uniqueness
 for b1, b2 being Relation of [:R1,S1:],[:R2,S2:] st ( for x, y being set holds
( [x,y] in b1 iff ex r1, s1, r2, s2 being set st
( x = [r1,s1] & y = [r2,s2] & r1 in R1 & s1 in S1 & r2 in R2 & s2 in S2 & ( [r1,r2] in R or [s1,s2] in S ) ) ) ) & ( for x, y being set holds
( [x,y] in b2 iff ex r1, s1, r2, s2 being set st
( x = [r1,s1] & y = [r2,s2] & r1 in R1 & s1 in S1 & r2 in R2 & s2 in S2 & ( [r1,r2] in R or [s1,s2] in S ) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines [^ PCS_0:def_2_:_
 for R1, R2, S1, S2 being set
for R being Relation of R1,R2
for S being Relation of S1,S2
for b7 being Relation of [:R1,S1:],[:R2,S2:] holds
( b7 = [^R,S^] iff for x, y being set holds
( [x,y] in b7 iff ex r1, s1, r2, s2 being set st
( x = [r1,s1] & y = [r2,s2] & r1 in R1 & s1 in S1 & r2 in R2 & s2 in S2 & ( [r1,r2] in R or [s1,s2] in S ) ) ) );

definition
let R1, R2, S1, S2 be non empty set ;
let R be Relation of R1,R2;
let S be Relation of S1,S2;
redefine func [^R,S^] means :Def3: :: PCS_0:def 3
 for r1 being Element of R1
for r2 being Element of R2
for s1 being Element of S1
for s2 being Element of S2 holds
( [[r1,s1],[r2,s2]] in it iff ( [r1,r2] in R or [s1,s2] in S ) );
compatibility
 for b1 being Relation of [:R1,S1:],[:R2,S2:] holds
( b1 = [^R,S^] iff for r1 being Element of R1
for r2 being Element of R2
for s1 being Element of S1
for s2 being Element of S2 holds
( [[r1,s1],[r2,s2]] in b1 iff ( [r1,r2] in R or [s1,s2] in S ) ) )
proofend;
end;

:: deftheorem Def3 defines [^ PCS_0:def_3_:_
 for R1, R2, S1, S2 being non empty set
for R being Relation of R1,R2
for S being Relation of S1,S2
for b7 being Relation of [:R1,S1:],[:R2,S2:] holds
( b7 = [^R,S^] iff for r1 being Element of R1
for r2 being Element of R2
for s1 being Element of S1
for s2 being Element of S2 holds
( [[r1,s1],[r2,s2]] in b7 iff ( [r1,r2] in R or [s1,s2] in S ) ) );

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
 [^R,S^] is total
proofend;
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
 [^R,S^] is reflexive
proofend;
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
 [^R,S^] is reflexive
proofend;
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
 [^R,S^] is reflexive
proofend;
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
 [^R,S^] is symmetric
proofend;
end;

begin

registration
cluster empty  ->  total for RelStr ;
coherence
 for b1 being RelStr st b1 is empty holds
b1 is total
proofend;
end;

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

:: deftheorem Def4 defines transitive-yielding PCS_0:def_4_:_
 for R being Relation holds
( R is transitive-yielding iff for S being RelStr st S in rng R holds
S is transitive );

registration
cluster Relation-like Poset-yielding  ->  transitive-yielding for set ;
coherence
 for b1 being Relation st b1 is Poset-yielding holds
b1 is transitive-yielding
proofend;
end;

registration
cluster Relation-like Function-like Poset-yielding for set ;
existence
 ex b1 being Function st b1 is Poset-yielding
proofend;
end;

registration
let I be set ;
cluster Relation-like I -defined Function-like total Poset-yielding for set ;
existence
 ex b1 being ManySortedSet of I st b1 is Poset-yielding
proofend;
end;

definition
let I be set ;
let C be RelStr-yielding ManySortedSet of I;
func pcs-InternalRels C ->  ManySortedSet of I means :Def5: :: PCS_0:def 5
 for i being set st i in I holds
ex P being RelStr st
( P = C . i & it . i = the InternalRel of P );
existence
 ex b1 being ManySortedSet of I st
for i being set st i in I holds
ex P being RelStr st
( P = C . i & b1 . i = the InternalRel of P )
proofend;
uniqueness
 for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds
ex P being RelStr st
( P = C . i & b1 . i = the InternalRel of P ) ) & ( for i being set st i in I holds
ex P being RelStr st
( P = C . i & b2 . i = the InternalRel of P ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines pcs-InternalRels PCS_0:def_5_:_
 for I being set
for C being RelStr-yielding ManySortedSet of I
for b3 being ManySortedSet of I holds
( b3 = pcs-InternalRels C iff for i being set st i in I holds
ex P being RelStr st
( P = C . i & b3 . i = the InternalRel of P ) );

definition
let I be non empty set ;
let C be RelStr-yielding ManySortedSet of I;
redefine func pcs-InternalRels C means :Def6: :: PCS_0:def 6
 for i being Element of I holds it . i = the InternalRel of (C . i);
compatibility
 for b1 being ManySortedSet of I holds
( b1 = pcs-InternalRels C iff for i being Element of I holds b1 . i = the InternalRel of (C . i) )
proofend;
end;

:: deftheorem Def6 defines pcs-InternalRels PCS_0:def_6_:_
 for I being non empty set
for C being RelStr-yielding ManySortedSet of I
for b3 being ManySortedSet of I holds
( b3 = pcs-InternalRels C iff for i being Element of I holds b3 . i = the InternalRel of (C . i) );

registration
let I be set ;
let C be RelStr-yielding ManySortedSet of I;
cluster pcs-InternalRels C ->  Relation-yielding ;
coherence
 pcs-InternalRels C is Relation-yielding
proofend;
end;

registration
let I be non empty set ;
let C be RelStr-yielding transitive-yielding ManySortedSet of I;
let i be Element of I;
clusterC . i ->  transitive for RelStr ;
coherence
 for b1 being RelStr st b1 = C . i holds
b1 is transitive
proofend;
end;

begin

definition
attrc1 is strict ;
struct TolStr  ->  1-sorted ;
aggrTolStr(# carrier, ToleranceRel #) ->  TolStr ;
sel ToleranceRel c1 ->  Relation of the carrier of c1;
end;

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

:: deftheorem Def7 defines (--) PCS_0:def_7_:_
 for P being TolStr
for p, q being Element of P holds
( p (--) q iff [p,q] in the ToleranceRel of P );

definition
let P be TolStr ;
attrP is pcs-tol-total  means :Def8: :: PCS_0:def 8
 the ToleranceRel of P is total ;
attrP is pcs-tol-reflexive  means :Def9: :: PCS_0:def 9
 the ToleranceRel of P is_reflexive_in the carrier of P;
attrP is pcs-tol-irreflexive  means :Def10: :: PCS_0:def 10
 the ToleranceRel of P is_irreflexive_in the carrier of P;
attrP is pcs-tol-symmetric  means :Def11: :: PCS_0:def 11
 the ToleranceRel of P is_symmetric_in the carrier of P;
end;

:: deftheorem Def8 defines pcs-tol-total PCS_0:def_8_:_
 for P being TolStr holds
( P is pcs-tol-total iff the ToleranceRel of P is total );

:: deftheorem Def9 defines pcs-tol-reflexive PCS_0:def_9_:_
 for P being TolStr holds
( P is pcs-tol-reflexive iff the ToleranceRel of P is_reflexive_in the carrier of P );

:: deftheorem Def10 defines pcs-tol-irreflexive PCS_0:def_10_:_
 for P being TolStr holds
( P is pcs-tol-irreflexive iff the ToleranceRel of P is_irreflexive_in the carrier of P );

:: deftheorem Def11 defines pcs-tol-symmetric PCS_0:def_11_:_
 for P being TolStr holds
( P is pcs-tol-symmetric iff the ToleranceRel of P is_symmetric_in the carrier of P );

definition
func emptyTolStr  ->  TolStr  equals :: PCS_0:def 12
 TolStr(# {},({} ({},{})) #);
coherence
 TolStr(# {},({} ({},{})) #) is TolStr ;
end;

:: deftheorem  defines emptyTolStr PCS_0:def_12_:_
 emptyTolStr = TolStr(# {},({} ({},{})) #);

registration
cluster emptyTolStr  ->  empty strict ;
coherence
 ( emptyTolStr is empty & emptyTolStr is strict ) ;
end;

theorem Th2: :: PCS_0:2
for P being TolStr st P is empty holds
TolStr(# the carrier of P, the ToleranceRel of P #) = emptyTolStr
proofend;

registration
cluster pcs-tol-reflexive  ->  pcs-tol-total for TolStr ;
coherence
 for b1 being TolStr st b1 is pcs-tol-reflexive holds
b1 is pcs-tol-total
proofend;
end;

registration
cluster empty  ->  pcs-tol-reflexive pcs-tol-irreflexive pcs-tol-symmetric for TolStr ;
coherence
 for b1 being TolStr st b1 is empty holds
( b1 is pcs-tol-reflexive & b1 is pcs-tol-irreflexive & b1 is pcs-tol-symmetric )
proofend;
end;

registration
cluster empty strict for TolStr ;
existence
 ex b1 being TolStr st
( b1 is empty & b1 is strict )
proofend;
end;

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

registration
let P be pcs-tol-reflexive TolStr ;
cluster the ToleranceRel of P ->  reflexive ;
coherence
 the ToleranceRel of P is reflexive
proofend;
end;

registration
let P be pcs-tol-irreflexive TolStr ;
cluster the ToleranceRel of P ->  irreflexive ;
coherence
 the ToleranceRel of P is irreflexive
proofend;
end;

registration
let P be pcs-tol-symmetric TolStr ;
cluster the ToleranceRel of P ->  symmetric ;
coherence
 the ToleranceRel of P is symmetric
proofend;
end;

registration
let L be pcs-tol-total TolStr ;
cluster TolStr(# the carrier of L, the ToleranceRel of L #) ->  pcs-tol-total ;
coherence
 TolStr(# the carrier of L, the ToleranceRel of L #) is pcs-tol-total by Def8;
end;

definition
let P be pcs-tol-symmetric TolStr ;
let p, q be Element of P;
:: original:(--)
redefine predp (--) q;
symmetry
 for p, q being Element of P st (P,b1,b2) holds
(P,b2,b1)
proofend;
end;

registration
let D be set ;
cluster TolStr(# D,(nabla D) #) ->  pcs-tol-reflexive pcs-tol-symmetric ;
coherence
 ( TolStr(# D,(nabla D) #) is pcs-tol-reflexive & TolStr(# D,(nabla D) #) is pcs-tol-symmetric )
proofend;
end;

registration
let D be set ;
cluster TolStr(# D,({} (D,D)) #) ->  pcs-tol-irreflexive pcs-tol-symmetric ;
coherence
 ( TolStr(# D,({} (D,D)) #) is pcs-tol-irreflexive & TolStr(# D,({} (D,D)) #) is pcs-tol-symmetric )
proofend;
end;

registration
cluster non empty strict pcs-tol-reflexive pcs-tol-symmetric for TolStr ;
existence
 ex b1 being TolStr st
( b1 is strict & not b1 is empty & b1 is pcs-tol-reflexive & b1 is pcs-tol-symmetric )
proofend;
end;

registration
cluster non empty strict pcs-tol-irreflexive pcs-tol-symmetric for TolStr ;
existence
 ex b1 being TolStr st
( b1 is strict & not b1 is empty & b1 is pcs-tol-irreflexive & b1 is pcs-tol-symmetric )
proofend;
end;

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

:: deftheorem Def13 defines TolStr-yielding PCS_0:def_13_:_
 for R being Relation holds
( R is TolStr-yielding iff for P being set st P in rng R holds
P is TolStr );

definition
let f be Function;
redefine attr f is TolStr-yielding  means :Def14: :: PCS_0:def 14
 for x being set st x in dom f holds
f . x is TolStr ;
compatibility
 ( f is TolStr-yielding iff for x being set st x in dom f holds
f . x is TolStr )
proofend;
end;

:: deftheorem Def14 defines TolStr-yielding PCS_0:def_14_:_
 for f being Function holds
( f is TolStr-yielding iff for x being set st x in dom f holds
f . x is TolStr );

definition
let I be set ;
let f be ManySortedSet of I;
A1: dom f = I by PARTFUN1:def_2;
:: original:TolStr-yielding
redefine attrf is TolStr-yielding  means :: PCS_0:def 15
 for x being set st x in I holds
f . x is TolStr ;
compatibility
 ( f is TolStr-yielding iff for x being set st x in I holds
f . x is TolStr ) by A1, Def14;
end;

:: deftheorem  defines TolStr-yielding PCS_0:def_15_:_
 for I being set
for f being ManySortedSet of I holds
( f is TolStr-yielding iff for x being set st x in I holds
f . x is TolStr );

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

:: deftheorem Def16 defines pcs-tol-reflexive-yielding PCS_0:def_16_:_
 for R being Relation holds
( R is pcs-tol-reflexive-yielding iff for S being TolStr st S in rng R holds
S is pcs-tol-reflexive );

:: deftheorem Def17 defines pcs-tol-irreflexive-yielding PCS_0:def_17_:_
 for R being Relation holds
( R is pcs-tol-irreflexive-yielding iff for S being TolStr st S in rng R holds
S is pcs-tol-irreflexive );

:: deftheorem Def18 defines pcs-tol-symmetric-yielding PCS_0:def_18_:_
 for R being Relation holds
( R is pcs-tol-symmetric-yielding iff for S being TolStr st S in rng R holds
S is pcs-tol-symmetric );

registration
cluster Relation-like empty  ->  pcs-tol-reflexive-yielding pcs-tol-irreflexive-yielding pcs-tol-symmetric-yielding for set ;
coherence
 for b1 being Relation st b1 is empty holds
( b1 is pcs-tol-reflexive-yielding & b1 is pcs-tol-irreflexive-yielding & b1 is pcs-tol-symmetric-yielding )
proofend;
end;

registration
let I be set ;
let P be TolStr ;
clusterI --> P -> () for ManySortedSet of I;
coherence
 for b1 being ManySortedSet of I st b1 = I --> P holds
b1 is TolStr-yielding
proofend;
end;

registration
let I be set ;
let P be pcs-tol-reflexive TolStr ;
clusterI --> P ->  pcs-tol-reflexive-yielding for ManySortedSet of I;
coherence
 for b1 being ManySortedSet of I st b1 = I --> P holds
b1 is pcs-tol-reflexive-yielding
proofend;
end;

registration
let I be set ;
let P be pcs-tol-irreflexive TolStr ;
clusterI --> P ->  pcs-tol-irreflexive-yielding for ManySortedSet of I;
coherence
 for b1 being ManySortedSet of I st b1 = I --> P holds
b1 is pcs-tol-irreflexive-yielding
proofend;
end;

registration
let I be set ;
let P be pcs-tol-symmetric TolStr ;
clusterI --> P ->  pcs-tol-symmetric-yielding for ManySortedSet of I;
coherence
 for b1 being ManySortedSet of I st b1 = I --> P holds
b1 is pcs-tol-symmetric-yielding
proofend;
end;

registration
cluster Relation-like Function-like TolStr-yielding  ->  1-sorted-yielding for set ;
coherence
 for b1 being Function st b1 is TolStr-yielding holds
b1 is 1-sorted-yielding
proofend;
end;

registration
let I be set ;
cluster Relation-like I -defined Function-like total () pcs-tol-reflexive-yielding pcs-tol-symmetric-yielding for set ;
existence
 ex b1 being ManySortedSet of I st
( b1 is pcs-tol-reflexive-yielding & b1 is pcs-tol-symmetric-yielding & b1 is () )
proofend;
end;

registration
let I be set ;
cluster Relation-like I -defined Function-like total () pcs-tol-irreflexive-yielding pcs-tol-symmetric-yielding for set ;
existence
 ex b1 being ManySortedSet of I st
( b1 is pcs-tol-irreflexive-yielding & b1 is pcs-tol-symmetric-yielding & b1 is () )
proofend;
end;

registration
let I be set ;
cluster Relation-like I -defined Function-like total () for set ;
existence
 not for b1 being ManySortedSet of I holds b1 is ()
proofend;
end;

definition
let I be non empty set ;
let C be () ManySortedSet of I;
let i be Element of I;
:: original:.
redefine funcC . i ->  TolStr ;
coherence
 C . i is TolStr
proofend;
end;

definition
let I be set ;
let C be () ManySortedSet of I;
func pcs-ToleranceRels C ->  ManySortedSet of I means :Def19: :: PCS_0:def 19
 for i being set st i in I holds
ex P being TolStr st
( P = C . i & it . i = the ToleranceRel of P );
existence
 ex b1 being ManySortedSet of I st
for i being set st i in I holds
ex P being TolStr st
( P = C . i & b1 . i = the ToleranceRel of P )
proofend;
uniqueness
 for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds
ex P being TolStr st
( P = C . i & b1 . i = the ToleranceRel of P ) ) & ( for i being set st i in I holds
ex P being TolStr st
( P = C . i & b2 . i = the ToleranceRel of P ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def19 defines pcs-ToleranceRels PCS_0:def_19_:_
 for I being set
for C being () ManySortedSet of I
for b3 being ManySortedSet of I holds
( b3 = pcs-ToleranceRels C iff for i being set st i in I holds
ex P being TolStr st
( P = C . i & b3 . i = the ToleranceRel of P ) );

definition
let I be non empty set ;
let C be () ManySortedSet of I;
redefine func pcs-ToleranceRels C means :Def20: :: PCS_0:def 20
 for i being Element of I holds it . i = the ToleranceRel of (C . i);
compatibility
 for b1 being ManySortedSet of I holds
( b1 = pcs-ToleranceRels C iff for i being Element of I holds b1 . i = the ToleranceRel of (C . i) )
proofend;
end;

:: deftheorem Def20 defines pcs-ToleranceRels PCS_0:def_20_:_
 for I being non empty set
for C being () ManySortedSet of I
for b3 being ManySortedSet of I holds
( b3 = pcs-ToleranceRels C iff for i being Element of I holds b3 . i = the ToleranceRel of (C . i) );

registration
let I be set ;
let C be () ManySortedSet of I;
cluster pcs-ToleranceRels C ->  Relation-yielding ;
coherence
 pcs-ToleranceRels C is Relation-yielding
proofend;
end;

registration
let I be non empty set ;
let C be () pcs-tol-reflexive-yielding ManySortedSet of I;
let i be Element of I;
clusterC . i ->  pcs-tol-reflexive for TolStr ;
coherence
 for b1 being TolStr st b1 = C . i holds
b1 is pcs-tol-reflexive
proofend;
end;

registration
let I be non empty set ;
let C be () pcs-tol-irreflexive-yielding ManySortedSet of I;
let i be Element of I;
clusterC . i ->  pcs-tol-irreflexive for TolStr ;
coherence
 for b1 being TolStr st b1 = C . i holds
b1 is pcs-tol-irreflexive
proofend;
end;

registration
let I be non empty set ;
let C be () pcs-tol-symmetric-yielding ManySortedSet of I;
let i be Element of I;
clusterC . i ->  pcs-tol-symmetric for TolStr ;
coherence
 for b1 being TolStr st b1 = C . i holds
b1 is pcs-tol-symmetric
proofend;
end;

theorem Th3: :: PCS_0:3
for P, Q being TolStr st TolStr(# the carrier of P, the ToleranceRel of P #) = TolStr(# the carrier of Q, the ToleranceRel of Q #) & P is pcs-tol-reflexive holds
Q is pcs-tol-reflexive
proofend;

theorem Th4: :: PCS_0:4
for P, Q being TolStr st TolStr(# the carrier of P, the ToleranceRel of P #) = TolStr(# the carrier of Q, the ToleranceRel of Q #) & P is pcs-tol-irreflexive holds
Q is pcs-tol-irreflexive
proofend;

theorem Th5: :: PCS_0:5
for P, Q being TolStr st TolStr(# the carrier of P, the ToleranceRel of P #) = TolStr(# the carrier of Q, the ToleranceRel of Q #) & P is pcs-tol-symmetric holds
Q is pcs-tol-symmetric
proofend;

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

:: deftheorem  defines [^ PCS_0:def_21_:_
 for P, Q being TolStr holds [^P,Q^] = TolStr(# [: the carrier of P, the carrier of Q:],[^ the ToleranceRel of P, the ToleranceRel of Q^] #);

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

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

notation
let P, Q be TolStr ;
let 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 ;
let p be Element of [^P,Q^];
:: original:^`1
redefine funcp ^`1  ->  Element of P;
coherence
 ^`1 is Element of P by MCART_1:10;
:: original:^`2
redefine funcp ^`2  ->  Element of Q;
coherence
 ^`2 is Element of Q by MCART_1:10;
end;

theorem Th6: :: PCS_0:6
for S1, S2 being non empty TolStr
for a, c being Element of S1
for b, d being Element of S2 holds
( [^a,b^] (--) [^c,d^] iff ( a (--) c or b (--) d ) )
proofend;

theorem :: PCS_0:7
for S1, S2 being non empty TolStr
for x, y being Element of [^S1,S2^] holds
( x (--) y iff ( x ^`1 (--) y ^`1 or x ^`2 (--) y ^`2 ) )
proofend;

registration
let P be TolStr ;
let Q be pcs-tol-reflexive TolStr ;
cluster[^P,Q^] ->  pcs-tol-reflexive ;
coherence
 [^P,Q^] is pcs-tol-reflexive
proofend;
end;

registration
let P be pcs-tol-reflexive TolStr ;
let Q be TolStr ;
cluster[^P,Q^] ->  pcs-tol-reflexive ;
coherence
 [^P,Q^] is pcs-tol-reflexive
proofend;
end;

registration
let P, Q be pcs-tol-symmetric TolStr ;
cluster[^P,Q^] ->  pcs-tol-symmetric ;
coherence
 [^P,Q^] is pcs-tol-symmetric
proofend;
end;

begin

definition
attrc1 is strict ;
struct pcs-Str  ->  RelStr , TolStr ;
aggrpcs-Str(# carrier, InternalRel, ToleranceRel #) ->  pcs-Str ;
end;

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

:: deftheorem Def22 defines pcs-compatible PCS_0:def_22_:_
 for P being pcs-Str holds
( P is pcs-compatible iff for p, p9, q, q9 being Element of P st p (--) q &amp; p9 <= p &amp; q9 <= q holds
p9 (--) q9 );

definition
let P be pcs-Str ;
attrP is pcs-like  means :Def23: :: PCS_0:def 23
( P is reflexive &amp; P is transitive &amp; P is pcs-tol-reflexive &amp; P is pcs-tol-symmetric &amp; P is pcs-compatible );
attrP is anti-pcs-like  means :Def24: :: PCS_0:def 24
( P is reflexive &amp; P is transitive &amp; P is pcs-tol-irreflexive &amp; P is pcs-tol-symmetric &amp; P is pcs-compatible );
end;

:: deftheorem Def23 defines pcs-like PCS_0:def_23_:_
 for P being pcs-Str holds
( P is pcs-like iff ( P is reflexive &amp; P is transitive &amp; P is pcs-tol-reflexive &amp; P is pcs-tol-symmetric &amp; P is pcs-compatible ) );

:: deftheorem Def24 defines anti-pcs-like PCS_0:def_24_:_
 for P being pcs-Str holds
( P is anti-pcs-like iff ( P is reflexive &amp; P is transitive &amp; P is pcs-tol-irreflexive &amp; P is pcs-tol-symmetric &amp; P is pcs-compatible ) );

registration
cluster pcs-like  ->  reflexive transitive pcs-tol-reflexive pcs-tol-symmetric pcs-compatible for pcs-Str ;
coherence
 for b1 being pcs-Str st b1 is pcs-like holds
( b1 is reflexive &amp; b1 is transitive &amp; b1 is pcs-tol-reflexive &amp; b1 is pcs-tol-symmetric &amp; b1 is pcs-compatible ) by Def23;
cluster reflexive transitive pcs-tol-reflexive pcs-tol-symmetric pcs-compatible  ->  pcs-like for pcs-Str ;
coherence
 for b1 being pcs-Str st b1 is reflexive &amp; b1 is transitive &amp; b1 is pcs-tol-reflexive &amp; b1 is pcs-tol-symmetric &amp; b1 is pcs-compatible holds
b1 is pcs-like by Def23;
cluster anti-pcs-like  ->  reflexive transitive pcs-tol-irreflexive pcs-tol-symmetric pcs-compatible for pcs-Str ;
coherence
 for b1 being pcs-Str st b1 is anti-pcs-like holds
( b1 is reflexive &amp; b1 is transitive &amp; b1 is pcs-tol-irreflexive &amp; b1 is pcs-tol-symmetric &amp; b1 is pcs-compatible ) by Def24;
cluster reflexive transitive pcs-tol-irreflexive pcs-tol-symmetric pcs-compatible  ->  anti-pcs-like for pcs-Str ;
coherence
 for b1 being pcs-Str st b1 is reflexive &amp; b1 is transitive &amp; b1 is pcs-tol-irreflexive &amp; b1 is pcs-tol-symmetric &amp; b1 is pcs-compatible holds
b1 is anti-pcs-like by Def24;
end;

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

:: deftheorem  defines pcs-total PCS_0:def_25_:_
 for D being set holds pcs-total D = pcs-Str(# D,(nabla D),(nabla D) #);

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

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

registration
let D be set ;
cluster pcs-total D ->  reflexive transitive pcs-tol-reflexive pcs-tol-symmetric ;
coherence
 ( pcs-total D is reflexive &amp; pcs-total D is transitive &amp; pcs-total D is pcs-tol-reflexive &amp; pcs-total D is pcs-tol-symmetric )
proofend;
end;

registration
let D be set ;
cluster pcs-total D ->  pcs-like ;
coherence
 pcs-total D is pcs-like
proofend;
end;

registration
let D be set ;
cluster pcs-Str(# D,(nabla D),({} (D,D)) #) ->  anti-pcs-like ;
coherence
 pcs-Str(# D,(nabla D),({} (D,D)) #) is anti-pcs-like
proofend;
end;

registration
cluster non empty strict pcs-like for pcs-Str ;
existence
 ex b1 being pcs-Str st
( b1 is strict &amp; not b1 is empty &amp; b1 is pcs-like )
proofend;
cluster non empty strict anti-pcs-like for pcs-Str ;
existence
 ex b1 being pcs-Str st
( b1 is strict &amp; not b1 is empty &amp; b1 is anti-pcs-like )
proofend;
end;

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

definition
func pcs-empty  ->  pcs-Str  equals :: PCS_0:def 26
 pcs-total 0;
coherence
 pcs-total 0 is pcs-Str ;
end;

:: deftheorem  defines pcs-empty PCS_0:def_26_:_
 pcs-empty = pcs-total 0;

registration
cluster pcs-empty  ->  empty strict pcs-like ;
coherence
 ( pcs-empty is strict &amp; pcs-empty is empty &amp; pcs-empty is pcs-like ) ;
end;

definition
let p be set ;
func pcs-singleton p ->  pcs-Str  equals :: PCS_0:def 27
 pcs-total {p};
coherence
 pcs-total {p} is pcs-Str ;
end;

:: deftheorem  defines pcs-singleton PCS_0:def_27_:_
 for p being set holds pcs-singleton p = pcs-total {p};

registration
let p be set ;
cluster pcs-singleton p ->  non empty strict pcs-like ;
coherence
 ( pcs-singleton p is strict &amp; not pcs-singleton p is empty &amp; pcs-singleton p is pcs-like ) ;
end;

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

:: deftheorem Def28 defines pcs-Str-yielding PCS_0:def_28_:_
 for R being Relation holds
( R is pcs-Str-yielding iff for P being set st P in rng R holds
P is pcs-Str );

:: deftheorem Def29 defines pcs-yielding PCS_0:def_29_:_
 for R being Relation holds
( R is pcs-yielding iff for P being set st P in rng R holds
P is pcs );

definition
let f be Function;
redefine attr f is pcs-Str-yielding  means :Def30: :: PCS_0:def 30
 for x being set st x in dom f holds
f . x is pcs-Str ;
compatibility
 ( f is pcs-Str-yielding iff for x being set st x in dom f holds
f . x is pcs-Str )
proofend;
redefine attr f is pcs-yielding  means :Def31: :: PCS_0:def 31
 for x being set st x in dom f holds
f . x is pcs;
compatibility
 ( f is pcs-yielding iff for x being set st x in dom f holds
f . x is pcs )
proofend;
end;

:: deftheorem Def30 defines pcs-Str-yielding PCS_0:def_30_:_
 for f being Function holds
( f is pcs-Str-yielding iff for x being set st x in dom f holds
f . x is pcs-Str );

:: deftheorem Def31 defines pcs-yielding PCS_0:def_31_:_
 for f being Function holds
( f is pcs-yielding iff for x being set st x in dom f holds
f . x is pcs );

definition
let I be set ;
let f be ManySortedSet of I;
A1: dom f = I by PARTFUN1:def_2;
:: original:pcs-Str-yielding
redefine attrf is pcs-Str-yielding  means :Def32: :: PCS_0:def 32
 for x being set st x in I holds
f . x is pcs-Str ;
compatibility
 ( f is pcs-Str-yielding iff for x being set st x in I holds
f . x is pcs-Str ) by A1, Def30;
:: original:pcs-yielding
redefine attrf is pcs-yielding  means :Def33: :: PCS_0:def 33
 for x being set st x in I holds
f . x is pcs;
compatibility
 ( f is pcs-yielding iff for x being set st x in I holds
f . x is pcs ) by A1, Def31;
end;

:: deftheorem Def32 defines pcs-Str-yielding PCS_0:def_32_:_
 for I being set
for f being ManySortedSet of I holds
( f is pcs-Str-yielding iff for x being set st x in I holds
f . x is pcs-Str );

:: deftheorem Def33 defines pcs-yielding PCS_0:def_33_:_
 for I being set
for f being ManySortedSet of I holds
( f is pcs-yielding iff for x being set st x in I holds
f . x is pcs );

registration
cluster Relation-like pcs-Str-yielding  ->  RelStr-yielding TolStr-yielding for set ;
coherence
 for b1 being Relation st b1 is pcs-Str-yielding holds
( b1 is TolStr-yielding &amp; b1 is RelStr-yielding )
proofend;
cluster Relation-like pcs-yielding  ->  pcs-Str-yielding for set ;
coherence
 for b1 being Relation st b1 is pcs-yielding holds
b1 is pcs-Str-yielding
proofend;
cluster Relation-like pcs-yielding  ->  reflexive-yielding transitive-yielding pcs-tol-reflexive-yielding pcs-tol-symmetric-yielding for set ;
coherence
 for b1 being Relation st b1 is pcs-yielding holds
( b1 is reflexive-yielding &amp; b1 is transitive-yielding &amp; b1 is pcs-tol-reflexive-yielding &amp; b1 is pcs-tol-symmetric-yielding )
proofend;
end;

registration
let I be set ;
let P be pcs;
clusterI --> P -> () for ManySortedSet of I;
coherence
 for b1 being ManySortedSet of I st b1 = I --> P holds
b1 is pcs-yielding
proofend;
end;

registration
let I be set ;
cluster Relation-like I -defined Function-like total () for set ;
existence
 not for b1 being ManySortedSet of I holds b1 is ()
proofend;
end;

definition
let I be non empty set ;
let C be () ManySortedSet of I;
let i be Element of I;
:: original:.
redefine funcC . i ->  pcs-Str ;
coherence
 C . i is pcs-Str by Def32;
end;

definition
let I be non empty set ;
let C be () ManySortedSet of I;
let i be Element of I;
:: original:.
redefine funcC . i ->  pcs;
coherence
 C . i is pcs by Def33;
end;

:: Union of PCS's
definition
let P, Q be pcs-Str ;
predP c= Q means :Def34: :: PCS_0:def 34
( the carrier of P c= the carrier of Q &amp; the InternalRel of P c= the InternalRel of Q &amp; the ToleranceRel of P c= the ToleranceRel of Q );
reflexivity
 for P being pcs-Str holds
( the carrier of P c= the carrier of P &amp; the InternalRel of P c= the InternalRel of P &amp; the ToleranceRel of P c= the ToleranceRel of P ) ;
end;

:: deftheorem Def34 defines c= PCS_0:def_34_:_
 for P, Q being pcs-Str holds
( P c= Q iff ( the carrier of P c= the carrier of Q &amp; the InternalRel of P c= the InternalRel of Q &amp; the ToleranceRel of P c= the ToleranceRel of Q ) );

theorem Th8: :: PCS_0:8
for P, Q being RelStr
for p, q being Element of P
for p1, q1 being Element of Q st the InternalRel of P c= the InternalRel of Q &amp; p = p1 &amp; q = q1 &amp; p <= q holds
p1 <= q1
proofend;

theorem Th9: :: PCS_0:9
for P, Q being TolStr
for p, q being Element of P
for p1, q1 being Element of Q st the ToleranceRel of P c= the ToleranceRel of Q &amp; p = p1 &amp; q = q1 &amp; p (--) q holds
p1 (--) q1
proofend;

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

definition
let C be Relation;
attrC is pcs-chain-like  means :Def35: :: PCS_0:def 35
 for P, Q being pcs-Str st P in rng C &amp; Q in rng C &amp; not P c= Q holds
Q c= P;
end;

:: deftheorem Def35 defines pcs-chain-like PCS_0:def_35_:_
 for C being Relation holds
( C is pcs-chain-like iff for P, Q being pcs-Str st P in rng C &amp; Q in rng C &amp; not P c= Q holds
Q c= P );

registration
let I be set ;
let P be pcs-Str ;
clusterI --> P ->  pcs-chain-like for ManySortedSet of I;
coherence
 for b1 being ManySortedSet of I st b1 = I --> P holds
b1 is pcs-chain-like
proofend;
end;

registration
cluster Relation-like Function-like pcs-yielding pcs-chain-like for set ;
existence
 ex b1 being Function st
( b1 is pcs-chain-like &amp; b1 is pcs-yielding )
proofend;
end;

registration
let I be set ;
cluster Relation-like I -defined Function-like total () pcs-chain-like for set ;
existence
 ex b1 being ManySortedSet of I st
( b1 is pcs-chain-like &amp; b1 is () )
proofend;
end;

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

definition
let I be set ;
let C be () ManySortedSet of I;
func pcs-union C ->  strict pcs-Str  means :Def36: :: PCS_0:def 36
( the carrier of it = Union (Carrier C) &amp; the InternalRel of it = Union (pcs-InternalRels C) &amp; the ToleranceRel of it = Union (pcs-ToleranceRels C) );
existence
 ex b1 being strict pcs-Str st
( the carrier of b1 = Union (Carrier C) &amp; the InternalRel of b1 = Union (pcs-InternalRels C) &amp; the ToleranceRel of b1 = Union (pcs-ToleranceRels C) )
proofend;
uniqueness
 for b1, b2 being strict pcs-Str st the carrier of b1 = Union (Carrier C) &amp; the InternalRel of b1 = Union (pcs-InternalRels C) &amp; the ToleranceRel of b1 = Union (pcs-ToleranceRels C) &amp; the carrier of b2 = Union (Carrier C) &amp; the InternalRel of b2 = Union (pcs-InternalRels C) &amp; the ToleranceRel of b2 = Union (pcs-ToleranceRels C) holds
b1 = b2 ;
end;

:: deftheorem Def36 defines pcs-union PCS_0:def_36_:_
 for I being set
for C being () ManySortedSet of I
for b3 being strict pcs-Str holds
( b3 = pcs-union C iff ( the carrier of b3 = Union (Carrier C) &amp; the InternalRel of b3 = Union (pcs-InternalRels C) &amp; the ToleranceRel of b3 = Union (pcs-ToleranceRels C) ) );

theorem Th10: :: PCS_0:10
for I being set
for C being () ManySortedSet of I
for p, q being Element of (pcs-union C) holds
( p <= q iff ex i being set ex P being pcs-Str ex p9, q9 being Element of P st
( i in I &amp; P = C . i &amp; p9 = p &amp; q9 = q &amp; p9 <= q9 ) )
proofend;

theorem :: PCS_0:11
for I being non empty set
for C being () ManySortedSet of I
for p, q being Element of (pcs-union C) holds
( p <= q iff ex i being Element of I ex p9, q9 being Element of (C . i) st
( p9 = p &amp; q9 = q &amp; p9 <= q9 ) )
proofend;

theorem Th12: :: PCS_0:12
for I being set
for C being () ManySortedSet of I
for p, q being Element of (pcs-union C) holds
( p (--) q iff ex i being set ex P being pcs-Str ex p9, q9 being Element of P st
( i in I &amp; P = C . i &amp; p9 = p &amp; q9 = q &amp; p9 (--) q9 ) )
proofend;

theorem :: PCS_0:13
for I being non empty set
for C being () ManySortedSet of I
for p, q being Element of (pcs-union C) holds
( p (--) q iff ex i being Element of I ex p9, q9 being Element of (C . i) st
( p9 = p &amp; q9 = q &amp; p9 (--) q9 ) )
proofend;

registration
let I be set ;
let C be reflexive-yielding () ManySortedSet of I;
cluster pcs-union C ->  reflexive strict ;
coherence
 pcs-union C is reflexive
proofend;
end;

registration
let I be set ;
let C be pcs-tol-reflexive-yielding () ManySortedSet of I;
cluster pcs-union C ->  pcs-tol-reflexive strict ;
coherence
 pcs-union C is pcs-tol-reflexive
proofend;
end;

registration
let I be set ;
let C be pcs-tol-symmetric-yielding () ManySortedSet of I;
cluster pcs-union C ->  pcs-tol-symmetric strict ;
coherence
 pcs-union C is pcs-tol-symmetric
proofend;
end;

registration
let I be set ;
let C be pcs-Chain of I;
cluster pcs-union C ->  transitive strict pcs-compatible ;
coherence
 ( pcs-union C is transitive &amp; pcs-union C is pcs-compatible )
proofend;
end;

:: Direct Sum of PCS's
registration
let p, q be set ;
cluster<%p,q%> -> {0,1} -defined ;
coherence
 <%p,q%> is {0,1} -defined
proofend;
cluster<%p,q%> ->  total ;
coherence
 <%p,q%> is total
proofend;
end;

registration
let P, Q be 1-sorted ;
cluster<%P,Q%> ->  1-sorted-yielding ;
coherence
 <%P,Q%> is 1-sorted-yielding
proofend;
end;

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

registration
let P, Q be RelStr ;
cluster<%P,Q%> ->  RelStr-yielding ;
coherence
 <%P,Q%> is RelStr-yielding
proofend;
end;

registration
let P, Q be TolStr ;
cluster<%P,Q%> -> () ;
coherence
 <%P,Q%> is TolStr-yielding
proofend;
end;

registration
let P, Q be pcs-Str ;
cluster<%P,Q%> -> () ;
coherence
 <%P,Q%> is pcs-Str-yielding
proofend;
end;

registration
let P, Q be reflexive pcs-Str ;
cluster<%P,Q%> ->  reflexive-yielding ;
coherence
 <%P,Q%> is reflexive-yielding
proofend;
end;

registration
let P, Q be transitive pcs-Str ;
cluster<%P,Q%> ->  transitive-yielding ;
coherence
 <%P,Q%> is transitive-yielding
proofend;
end;

registration
let P, Q be pcs-tol-reflexive pcs-Str ;
cluster<%P,Q%> ->  pcs-tol-reflexive-yielding ;
coherence
 <%P,Q%> is pcs-tol-reflexive-yielding
proofend;
end;

registration
let P, Q be pcs-tol-symmetric pcs-Str ;
cluster<%P,Q%> ->  pcs-tol-symmetric-yielding ;
coherence
 <%P,Q%> is pcs-tol-symmetric-yielding
proofend;
end;

registration
let P, Q be pcs;
cluster<%P,Q%> -> () ;
coherence
 <%P,Q%> is pcs-yielding
proofend;
end;

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

:: deftheorem  PCS_0:def_37_:_
canceled;

:: deftheorem  defines pcs-sum PCS_0:def_38_:_
 for P, Q being pcs-Str holds pcs-sum (P,Q) = pcs-union <%P,Q%>;

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

theorem Th14: :: PCS_0:14
for P, Q being pcs-Str holds
( the carrier of (pcs-sum (P,Q)) = the carrier of P \/ the carrier of Q &amp; the InternalRel of (pcs-sum (P,Q)) = the InternalRel of P \/ the InternalRel of Q &amp; the ToleranceRel of (pcs-sum (P,Q)) = the ToleranceRel of P \/ the ToleranceRel of Q )
proofend;

theorem Th15: :: PCS_0:15
for P, Q being pcs-Str holds pcs-sum (P,Q) = pcs-Str(# ( the carrier of P \/ the carrier of Q),( the InternalRel of P \/ the InternalRel of Q),( the ToleranceRel of P \/ the ToleranceRel of Q) #)
proofend;

theorem :: PCS_0:16
for P, Q being pcs-Str
for p, q being Element of (pcs-sum (P,Q)) holds
( p <= q iff ( ex p9, q9 being Element of P st
( p9 = p &amp; q9 = q &amp; p9 <= q9 ) or ex p9, q9 being Element of Q st
( p9 = p &amp; q9 = q &amp; p9 <= q9 ) ) )
proofend;

theorem :: PCS_0:17
for P, Q being pcs-Str
for p, q being Element of (pcs-sum (P,Q)) holds
( p (--) q iff ( ex p9, q9 being Element of P st
( p9 = p &amp; q9 = q &amp; p9 (--) q9 ) or ex p9, q9 being Element of Q st
( p9 = p &amp; q9 = q &amp; p9 (--) q9 ) ) )
proofend;

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

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

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

theorem Th18: :: PCS_0:18
for P, Q being pcs st P misses Q holds
the InternalRel of (pcs-sum (P,Q)) is transitive
proofend;

theorem Th19: :: PCS_0:19
for P, Q being pcs st P misses Q holds
pcs-sum (P,Q) is pcs-compatible
proofend;

theorem :: PCS_0:20
for P, Q being pcs st P misses Q holds
pcs-sum (P,Q) is pcs
proofend;

:: Extension
definition
let P be pcs-Str ;
let a be set ;
func pcs-extension (P,a) ->  strict pcs-Str  means :Def39: :: PCS_0:def 39
( the carrier of it = {a} \/ the carrier of P &amp; the InternalRel of it = [:{a}, the carrier of it:] \/ the InternalRel of P &amp; the ToleranceRel of it = ([:{a}, the carrier of it:] \/ [: the carrier of it,{a}:]) \/ the ToleranceRel of P );
existence
 ex b1 being strict pcs-Str st
( the carrier of b1 = {a} \/ the carrier of P &amp; the InternalRel of b1 = [:{a}, the carrier of b1:] \/ the InternalRel of P &amp; the ToleranceRel of b1 = ([:{a}, the carrier of b1:] \/ [: the carrier of b1,{a}:]) \/ the ToleranceRel of P )
proofend;
uniqueness
 for b1, b2 being strict pcs-Str st the carrier of b1 = {a} \/ the carrier of P &amp; the InternalRel of b1 = [:{a}, the carrier of b1:] \/ the InternalRel of P &amp; the ToleranceRel of b1 = ([:{a}, the carrier of b1:] \/ [: the carrier of b1,{a}:]) \/ the ToleranceRel of P &amp; the carrier of b2 = {a} \/ the carrier of P &amp; the InternalRel of b2 = [:{a}, the carrier of b2:] \/ the InternalRel of P &amp; the ToleranceRel of b2 = ([:{a}, the carrier of b2:] \/ [: the carrier of b2,{a}:]) \/ the ToleranceRel of P holds
b1 = b2 ;
end;

:: deftheorem Def39 defines pcs-extension PCS_0:def_39_:_
 for P being pcs-Str
for a being set
for b3 being strict pcs-Str holds
( b3 = pcs-extension (P,a) iff ( the carrier of b3 = {a} \/ the carrier of P &amp; the InternalRel of b3 = [:{a}, the carrier of b3:] \/ the InternalRel of P &amp; the ToleranceRel of b3 = ([:{a}, the carrier of b3:] \/ [: the carrier of b3,{a}:]) \/ the ToleranceRel of P ) );

registration
let P be pcs-Str ;
let a be set ;
cluster pcs-extension (P,a) ->  non empty strict ;
coherence
 not pcs-extension (P,a) is empty
proofend;
end;

theorem Th21: :: PCS_0:21
for P being pcs-Str
for a being set holds
( the carrier of P c= the carrier of (pcs-extension (P,a)) &amp; the InternalRel of P c= the InternalRel of (pcs-extension (P,a)) &amp; the ToleranceRel of P c= the ToleranceRel of (pcs-extension (P,a)) )
proofend;

theorem :: PCS_0:22
for P being pcs-Str
for a being set
for p, q being Element of (pcs-extension (P,a)) st p = a holds
p <= q
proofend;

theorem Th23: :: PCS_0:23
for P being pcs-Str
for a being set
for p, q being Element of P
for p1, q1 being Element of (pcs-extension (P,a)) st p = p1 &amp; q = q1 &amp; p <= q holds
p1 <= q1
proofend;

theorem Th24: :: PCS_0:24
for P being pcs-Str
for a being set
for p being Element of P
for p1, q1 being Element of (pcs-extension (P,a)) st p = p1 &amp; p <> a &amp; p1 <= q1 &amp; not a in the carrier of P holds
( q1 in the carrier of P &amp; q1 <> a )
proofend;

theorem Th25: :: PCS_0:25
for P being pcs-Str
for a being set
for p being Element of (pcs-extension (P,a)) st p <> a holds
p in the carrier of P
proofend;

theorem Th26: :: PCS_0:26
for P being pcs-Str
for a being set
for p, q being Element of P
for p1, q1 being Element of (pcs-extension (P,a)) st p = p1 &amp; q = q1 &amp; p <> a &amp; p1 <= q1 holds
p <= q
proofend;

theorem Th27: :: PCS_0:27
for P being pcs-Str
for a being set
for p, q being Element of (pcs-extension (P,a)) st p = a holds
( p (--) q &amp; q (--) p )
proofend;

theorem Th28: :: PCS_0:28
for P being pcs-Str
for a being set
for p, q being Element of P
for p1, q1 being Element of (pcs-extension (P,a)) st p = p1 &amp; q = q1 &amp; p (--) q holds
p1 (--) q1
proofend;

theorem Th29: :: PCS_0:29
for P being pcs-Str
for a being set
for p, q being Element of P
for p1, q1 being Element of (pcs-extension (P,a)) st p = p1 &amp; q = q1 &amp; p <> a &amp; q <> a &amp; p1 (--) q1 holds
p (--) q
proofend;

registration
let P be reflexive pcs-Str ;
let a be set ;
cluster pcs-extension (P,a) ->  reflexive strict ;
coherence
 pcs-extension (P,a) is reflexive
proofend;
end;

theorem Th30: :: PCS_0:30
for P being transitive pcs-Str
for a being set st not a in the carrier of P holds
pcs-extension (P,a) is transitive
proofend;

registration
let P be pcs-tol-reflexive pcs-Str ;
let a be set ;
cluster pcs-extension (P,a) ->  pcs-tol-reflexive strict ;
coherence
 pcs-extension (P,a) is pcs-tol-reflexive
proofend;
end;

registration
let P be pcs-tol-symmetric pcs-Str ;
let a be set ;
cluster pcs-extension (P,a) ->  pcs-tol-symmetric strict ;
coherence
 pcs-extension (P,a) is pcs-tol-symmetric
proofend;
end;

theorem Th31: :: PCS_0:31
for P being pcs-compatible pcs-Str
for a being set st not a in the carrier of P holds
pcs-extension (P,a) is pcs-compatible
proofend;

theorem :: PCS_0:32
for P being pcs
for a being set st not a in the carrier of P holds
pcs-extension (P,a) is pcs
proofend;

:: Reverse
definition
let P be pcs-Str ;
func pcs-reverse P ->  strict pcs-Str  means :Def40: :: PCS_0:def 40
( the carrier of it = the carrier of P &amp; the InternalRel of it = the InternalRel of P ~ &amp; the ToleranceRel of it = the ToleranceRel of P ` );
existence
 ex b1 being strict pcs-Str st
( the carrier of b1 = the carrier of P &amp; the InternalRel of b1 = the InternalRel of P ~ &amp; the ToleranceRel of b1 = the ToleranceRel of P ` )
proofend;
uniqueness
 for b1, b2 being strict pcs-Str st the carrier of b1 = the carrier of P &amp; the InternalRel of b1 = the InternalRel of P ~ &amp; the ToleranceRel of b1 = the ToleranceRel of P ` &amp; the carrier of b2 = the carrier of P &amp; the InternalRel of b2 = the InternalRel of P ~ &amp; the ToleranceRel of b2 = the ToleranceRel of P ` holds
b1 = b2 ;
end;

:: deftheorem Def40 defines pcs-reverse PCS_0:def_40_:_
 for P being pcs-Str
for b2 being strict pcs-Str holds
( b2 = pcs-reverse P iff ( the carrier of b2 = the carrier of P &amp; the InternalRel of b2 = the InternalRel of P ~ &amp; the ToleranceRel of b2 = the ToleranceRel of P ` ) );

registration
let P be non empty pcs-Str ;
cluster pcs-reverse P ->  non empty strict ;
coherence
 not pcs-reverse P is empty
proofend;
end;

theorem Th33: :: PCS_0:33
for P being pcs-Str
for p, q being Element of P
for p9, q9 being Element of (pcs-reverse P) st p = p9 &amp; q = q9 holds
( p <= q iff q9 <= p9 )
proofend;

theorem Th34: :: PCS_0:34
for P being pcs-Str
for p, q being Element of P
for p9, q9 being Element of (pcs-reverse P) st p = p9 &amp; q = q9 &amp; p (--) q holds
not p9 (--) q9
proofend;

theorem Th35: :: PCS_0:35
for P being non empty pcs-Str
for p, q being Element of P
for p9, q9 being Element of (pcs-reverse P) st p = p9 &amp; q = q9 &amp; not p9 (--) q9 holds
p (--) q
proofend;

registration
let P be reflexive pcs-Str ;
cluster pcs-reverse P ->  reflexive strict ;
coherence
 pcs-reverse P is reflexive
proofend;
end;

registration
let P be transitive pcs-Str ;
cluster pcs-reverse P ->  transitive strict ;
coherence
 pcs-reverse P is transitive
proofend;
end;

registration
let P be pcs-tol-reflexive pcs-Str ;
cluster pcs-reverse P ->  pcs-tol-irreflexive strict ;
coherence
 pcs-reverse P is pcs-tol-irreflexive
proofend;
end;

registration
let P be pcs-tol-irreflexive pcs-Str ;
cluster pcs-reverse P ->  pcs-tol-reflexive strict ;
coherence
 pcs-reverse P is pcs-tol-reflexive
proofend;
end;

registration
let P be pcs-tol-symmetric pcs-Str ;
cluster pcs-reverse P ->  pcs-tol-symmetric strict ;
coherence
 pcs-reverse P is pcs-tol-symmetric
proofend;
end;

registration
let P be pcs-compatible pcs-Str ;
cluster pcs-reverse P ->  strict pcs-compatible ;
coherence
 pcs-reverse P is pcs-compatible
proofend;
end;

:: Times
definition
let P, Q be pcs-Str ;
funcP pcs-times Q ->  pcs-Str  equals :: PCS_0:def 41
 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
 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^] #) is pcs-Str ;
end;

:: deftheorem  defines pcs-times PCS_0:def_41_:_
 for P, Q being pcs-Str holds P pcs-times 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^] #);

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

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

theorem :: PCS_0:36
for P, Q being pcs-Str
for p, q being Element of (P pcs-times Q)
for p1, p2 being Element of P
for q1, q2 being Element of Q st p = [p1,q1] &amp; q = [p2,q2] holds
( p <= q iff ( p1 <= p2 &amp; q1 <= q2 ) )
proofend;

theorem :: PCS_0:37
for P, Q being pcs-Str
for p, q being Element of (P pcs-times Q)
for p1, p2 being Element of P
for q1, q2 being Element of Q st p = [p1,q1] &amp; q = [p2,q2] &amp; p (--) q &amp; not p1 (--) p2 holds
q1 (--) q2
proofend;

theorem Th38: :: PCS_0:38
for P, Q being non empty pcs-Str
for p, q being Element of (P pcs-times Q)
for p1, p2 being Element of P
for q1, q2 being Element of Q st p = [p1,q1] &amp; q = [p2,q2] &amp; ( p1 (--) p2 or q1 (--) q2 ) holds
p (--) q
proofend;

registration
let P, Q be reflexive pcs-Str ;
clusterP pcs-times Q ->  reflexive ;
coherence
 P pcs-times Q is reflexive
proofend;
end;

registration
let P, Q be transitive pcs-Str ;
clusterP pcs-times Q ->  transitive ;
coherence
 P pcs-times Q is transitive
proofend;
end;

registration
let P be pcs-Str ;
let Q be pcs-tol-reflexive pcs-Str ;
clusterP pcs-times Q ->  pcs-tol-reflexive ;
coherence
 P pcs-times Q is pcs-tol-reflexive
proofend;
end;

registration
let P be pcs-tol-reflexive pcs-Str ;
let Q be pcs-Str ;
clusterP pcs-times Q ->  pcs-tol-reflexive ;
coherence
 P pcs-times Q is pcs-tol-reflexive
proofend;
end;

registration
let P, Q be pcs-tol-symmetric pcs-Str ;
clusterP pcs-times Q ->  pcs-tol-symmetric ;
coherence
 P pcs-times Q is pcs-tol-symmetric
proofend;
end;

registration
let P, Q be pcs-compatible pcs-Str ;
clusterP pcs-times Q ->  pcs-compatible ;
coherence
 P pcs-times Q is pcs-compatible
proofend;
end;

definition
let P, Q be pcs-Str ;
funcP --> Q ->  pcs-Str  equals :: PCS_0:def 42
(pcs-reverse P) pcs-times Q;
coherence
 (pcs-reverse P) pcs-times Q is pcs-Str ;
end;

:: deftheorem  defines --> PCS_0:def_42_:_
 for P, Q being pcs-Str holds P --> Q = (pcs-reverse P) pcs-times Q;

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

registration
let P, Q be non empty pcs-Str ;
clusterP --> Q ->  non empty ;
coherence
 not P --> Q is empty ;
end;

theorem :: PCS_0:39
for P, Q being pcs-Str
for p, q being Element of (P --> Q)
for p1, p2 being Element of P
for q1, q2 being Element of Q st p = [p1,q1] &amp; q = [p2,q2] holds
( p <= q iff ( p2 <= p1 &amp; q1 <= q2 ) )
proofend;

theorem :: PCS_0:40
for P, Q being pcs-Str
for p, q being Element of (P --> Q)
for p1, p2 being Element of P
for q1, q2 being Element of Q st p = [p1,q1] &amp; q = [p2,q2] &amp; p (--) q &amp; p1 (--) p2 holds
q1 (--) q2
proofend;

theorem :: PCS_0:41
for P, Q being non empty pcs-Str
for p, q being Element of (P --> Q)
for p1, p2 being Element of P
for q1, q2 being Element of Q st p = [p1,q1] &amp; q = [p2,q2] &amp; ( not p1 (--) p2 or q1 (--) q2 ) holds
p (--) q
proofend;

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

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

registration
let P be pcs-Str ;
let Q be pcs-tol-reflexive pcs-Str ;
clusterP --> Q ->  pcs-tol-reflexive ;
coherence
 P --> Q is pcs-tol-reflexive ;
end;

registration
let P be pcs-tol-irreflexive pcs-Str ;
let Q be pcs-Str ;
clusterP --> Q ->  pcs-tol-reflexive ;
coherence
 P --> Q is pcs-tol-reflexive ;
end;

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

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

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

:: Self-coherence
definition
let P be TolStr ;
let S be Subset of P;
attrS is pcs-self-coherent  means :Def43: :: PCS_0:def 43
 for x, y being Element of P st x in S &amp; y in S holds
x (--) y;
end;

:: deftheorem Def43 defines pcs-self-coherent PCS_0:def_43_:_
 for P being TolStr
for S being Subset of P holds
( S is pcs-self-coherent iff for x, y being Element of P st x in S &amp; y in S holds
x (--) y );

registration
let P be TolStr ;
cluster empty  ->  pcs-self-coherent for Element of bool the carrier of P;
coherence
 for b1 being Subset of P st b1 is empty holds
b1 is pcs-self-coherent
proofend;
end;

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

:: deftheorem Def44 defines pcs-self-coherent-membered PCS_0:def_44_:_
 for P being TolStr
for F being Subset-Family of P holds
( F is pcs-self-coherent-membered iff for S being Subset of P st S in F holds
S is pcs-self-coherent );

registration
let P be TolStr ;
cluster non empty pcs-self-coherent-membered for Element of bool (bool the carrier of P);
existence
 ex b1 being Subset-Family of P st
( not b1 is empty &amp; b1 is pcs-self-coherent-membered )
proofend;
end;

definition
let P be RelStr ;
let D be set ;
defpred S1[ set , set ] means ( $1 in D &amp; $2 in D &amp; ( for a being set st a in $1 holds
ex b being set st
( b in $2 &amp; [a,b] in the InternalRel of P ) ) );
func pcs-general-power-IR (P,D) ->  Relation of D means :Def45: :: PCS_0:def 45
 for A, B being set holds
( [A,B] in it iff ( A in D &amp; B in D &amp; ( for a being set st a in A holds
ex b being set st
( b in B &amp; [a,b] in the InternalRel of P ) ) ) );
existence
 ex b1 being Relation of D st
for A, B being set holds
( [A,B] in b1 iff ( A in D &amp; B in D &amp; ( for a being set st a in A holds
ex b being set st
( b in B &amp; [a,b] in the InternalRel of P ) ) ) )
proofend;
uniqueness
 for b1, b2 being Relation of D st ( for A, B being set holds
( [A,B] in b1 iff ( A in D &amp; B in D &amp; ( for a being set st a in A holds
ex b being set st
( b in B &amp; [a,b] in the InternalRel of P ) ) ) ) ) &amp; ( for A, B being set holds
( [A,B] in b2 iff ( A in D &amp; B in D &amp; ( for a being set st a in A holds
ex b being set st
( b in B &amp; [a,b] in the InternalRel of P ) ) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def45 defines pcs-general-power-IR PCS_0:def_45_:_
 for P being RelStr
for D being set
for b3 being Relation of D holds
( b3 = pcs-general-power-IR (P,D) iff for A, B being set holds
( [A,B] in b3 iff ( A in D &amp; B in D &amp; ( for a being set st a in A holds
ex b being set st
( b in B &amp; [a,b] in the InternalRel of P ) ) ) ) );

definition
let P be TolStr ;
let D be set ;
defpred S1[ set , set ] means ( $1 in D &amp; $2 in D &amp; ( for a, b being set st a in $1 &amp; b in $2 holds
[a,b] in the ToleranceRel of P ) );
func pcs-general-power-TR (P,D) ->  Relation of D means :Def46: :: PCS_0:def 46
 for A, B being set holds
( [A,B] in it iff ( A in D &amp; B in D &amp; ( for a, b being set st a in A &amp; b in B holds
[a,b] in the ToleranceRel of P ) ) );
existence
 ex b1 being Relation of D st
for A, B being set holds
( [A,B] in b1 iff ( A in D &amp; B in D &amp; ( for a, b being set st a in A &amp; b in B holds
[a,b] in the ToleranceRel of P ) ) )
proofend;
uniqueness
 for b1, b2 being Relation of D st ( for A, B being set holds
( [A,B] in b1 iff ( A in D &amp; B in D &amp; ( for a, b being set st a in A &amp; b in B holds
[a,b] in the ToleranceRel of P ) ) ) ) &amp; ( for A, B being set holds
( [A,B] in b2 iff ( A in D &amp; B in D &amp; ( for a, b being set st a in A &amp; b in B holds
[a,b] in the ToleranceRel of P ) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def46 defines pcs-general-power-TR PCS_0:def_46_:_
 for P being TolStr
for D being set
for b3 being Relation of D holds
( b3 = pcs-general-power-TR (P,D) iff for A, B being set holds
( [A,B] in b3 iff ( A in D &amp; B in D &amp; ( for a, b being set st a in A &amp; b in B holds
[a,b] in the ToleranceRel of P ) ) ) );

theorem :: PCS_0:42
for P being RelStr
for D being Subset-Family of P
for A, B being set holds
( [A,B] in pcs-general-power-IR (P,D) iff ( A in D &amp; B in D &amp; ( for a being Element of P st a in A holds
ex b being Element of P st
( b in B &amp; a <= b ) ) ) )
proofend;

theorem :: PCS_0:43
for P being TolStr
for D being Subset-Family of P
for A, B being set holds
( [A,B] in pcs-general-power-TR (P,D) iff ( A in D &amp; B in D &amp; ( for a, b being Element of P st a in A &amp; b in B holds
a (--) b ) ) )
proofend;

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

:: deftheorem  defines pcs-general-power PCS_0:def_47_:_
 for P being pcs-Str
for D being set holds pcs-general-power (P,D) = pcs-Str(# D,(pcs-general-power-IR (P,D)),(pcs-general-power-TR (P,D)) #);

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

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

theorem Th44: :: PCS_0:44
for P being pcs-Str
for D being set
for p, q being Element of (pcs-general-power (P,D)) st p <= q holds
for p9 being Element of P st p9 in p holds
ex q9 being Element of P st
( q9 in q &amp; p9 <= q9 )
proofend;

theorem :: PCS_0:45
for P being pcs-Str
for D being non empty Subset-Family of P
for p, q being Element of (pcs-general-power D) st ( for p9 being Element of P st p9 in p holds
ex q9 being Element of P st
( q9 in q &amp; p9 <= q9 ) ) holds
p <= q
proofend;

theorem Th46: :: PCS_0:46
for P being pcs-Str
for D being set
for p, q being Element of (pcs-general-power (P,D)) st p (--) q holds
for p9, q9 being Element of P st p9 in p &amp; q9 in q holds
p9 (--) q9
proofend;

theorem :: PCS_0:47
for P being pcs-Str
for D being non empty Subset-Family of P
for p, q being Element of (pcs-general-power D) st ( for p9, q9 being Element of P st p9 in p &amp; q9 in q holds
p9 (--) q9 ) holds
p (--) q
proofend;

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

registration
let P be reflexive pcs-Str ;
let D be Subset-Family of P;
cluster pcs-general-power (P,D) ->  reflexive ;
coherence
 pcs-general-power D is reflexive
proofend;
end;

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

registration
let P be pcs-tol-reflexive pcs-Str ;
let D be pcs-self-coherent-membered Subset-Family of P;
cluster pcs-general-power (P,D) ->  pcs-tol-reflexive ;
coherence
 pcs-general-power D is pcs-tol-reflexive
proofend;
end;

registration
let P be pcs-tol-symmetric pcs-Str ;
let D be Subset-Family of P;
cluster pcs-general-power (P,D) ->  pcs-tol-symmetric ;
coherence
 pcs-general-power D is pcs-tol-symmetric
proofend;
end;

registration
let P be pcs-compatible pcs-Str ;
let D be Subset-Family of P;
cluster pcs-general-power (P,D) ->  pcs-compatible ;
coherence
 pcs-general-power D is pcs-compatible
proofend;
end;

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

:: deftheorem  defines pcs-coherent-power PCS_0:def_48_:_
 for P being pcs-Str holds pcs-coherent-power P =  {  X where X is Subset of P : X is pcs-self-coherent  }  ;

registration
let P be pcs-Str ;
cluster pcs-self-coherent for Element of bool the carrier of P;
existence
 ex b1 being Subset of P st b1 is pcs-self-coherent
proofend;
end;

theorem Th48: :: PCS_0:48
for P being pcs-Str
for X being set st X in pcs-coherent-power P holds
X is pcs-self-coherent Subset of P
proofend;

registration
let P be pcs-Str ;
cluster pcs-coherent-power P ->  non empty ;
coherence
 not pcs-coherent-power P is empty
proofend;
end;

definition
let P be pcs-Str ;
:: original:pcs-coherent-power
redefine func pcs-coherent-power P ->  Subset-Family of P;
coherence
 pcs-coherent-power P is Subset-Family of P
proofend;
end;

registration
let P be pcs-Str ;
cluster pcs-coherent-power P ->  pcs-self-coherent-membered for Subset-Family of P;
coherence
 for b1 being Subset-Family of P st b1 = pcs-coherent-power P holds
b1 is pcs-self-coherent-membered
proofend;
end;

definition
let P be pcs-Str ;
func pcs-power P ->  pcs-Str  equals :: PCS_0:def 49
 pcs-general-power (pcs-coherent-power P);
coherence
 pcs-general-power (pcs-coherent-power P) is pcs-Str ;
end;

:: deftheorem  defines pcs-power PCS_0:def_49_:_
 for P being pcs-Str holds pcs-power P = pcs-general-power (pcs-coherent-power P);

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

registration
let P be pcs-Str ;
cluster pcs-power P ->  non empty ;
coherence
 not pcs-power P is empty ;
end;

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

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

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

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

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

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