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

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 func R \/ 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;
cluster R \/ S -> total for Relation of (R1 \/ S1);
coherence
for b1 being Relation of (R1 \/ S1) st b1 = R \/ S holds
b1 is total
proof 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 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;
cluster R \/ 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 object 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 object 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 object 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 object 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 object st [q1,q2] in R \/ S & q2 in S1 holds
( [q1,q2] in S & q1 in S1 )

let q1, q2 be object ; :: 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 ;
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 ; :: thesis: verum
end;
hence ( [q1,q2] in S & q1 in S1 ) by ; :: 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
proof end;

definition
let I be non empty set ;
let C be 1-sorted-yielding ManySortedSet of I;
:: original: Carrier
redefine func Carrier C -> ManySortedSet of I means :Def1: :: PCS_0:def 1
for i being Element of I holds it . i = the carrier of (C . i);
compatibility
for b1 being ManySortedSet of I holds
( b1 = Carrier C iff for i being Element of I holds b1 . i = the carrier of (C . i) )
proof end;
coherence
Carrier C is ManySortedSet of I
proof end;
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 ManySortedSet of I 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[ object , object ] 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 object 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 object 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 ) ) )
proof end;
uniqueness
for b1, b2 being Relation of [:R1,S1:],[:R2,S2:] st ( for x, y being object 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 object 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
proof end;
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 object 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 ) ) )
proof end;
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
proof 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
[^R,S^] is reflexive
proof 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
[^R,S^] is reflexive
proof 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
[^R,S^] is reflexive
proof 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
[^R,S^] is symmetric
proof end;
end;

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

definition
let R be Relation;
attr R 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
coherence
for b1 being Relation st b1 is Poset-yielding holds
b1 is transitive-yielding
by YELLOW16:def 5;
end;

registration
existence
ex b1 being Function st b1 is Poset-yielding
proof end;
end;

registration
let I be set ;
existence
ex b1 being ManySortedSet of I st b1 is Poset-yielding
proof end;
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 )
proof end;
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
proof end;
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) )
proof end;
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;
coherence
proof end;
end;

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

definition
attr c1 is strict ;
struct TolStr -> 1-sorted ;
aggr TolStr(# 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;
pred p (--) 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 ;
attr P is pcs-tol-total means :Def8: :: PCS_0:def 8
the ToleranceRel of P is total ;
attr P is pcs-tol-reflexive means :Def9: :: PCS_0:def 9
the ToleranceRel of P is_reflexive_in the carrier of P;
attr P is pcs-tol-irreflexive means :Def10: :: PCS_0:def 10
the ToleranceRel of P is_irreflexive_in the carrier of P;
attr P 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
coherence ;
end;

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

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

registration
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 )
proof end;
end;

registration
existence
ex b1 being TolStr st
( b1 is empty & b1 is strict )
proof end;
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
proof end;
end;

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

registration
let P be pcs-tol-symmetric TolStr ;
cluster the ToleranceRel of P -> symmetric ;
coherence
the ToleranceRel of P is symmetric
proof end;
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
;
end;

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

registration
let D be set ;
cluster TolStr(# D,() #) -> pcs-tol-reflexive pcs-tol-symmetric ;
coherence
( TolStr(# D,() #) is pcs-tol-reflexive & TolStr(# D,() #) is pcs-tol-symmetric )
proof end;
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 )
proof end;
end;

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

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

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

:: deftheorem 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 )
proof end;
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 attr f 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;
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;
attr R 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 ;
attr R 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 ;
attr R 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
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 )
;
end;

registration
let I be set ;
let P be TolStr ;
cluster I --> P -> () for ManySortedSet of I;
coherence
for b1 being ManySortedSet of I st b1 = I --> P holds
b1 is TolStr-yielding
by FUNCOP_1:7;
end;

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

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

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

registration
coherence
for b1 being Function st b1 is TolStr-yielding holds
b1 is 1-sorted-yielding
proof end;
end;

registration
let I be set ;
existence
ex b1 being ManySortedSet of I st
( b1 is pcs-tol-reflexive-yielding & b1 is pcs-tol-symmetric-yielding & b1 is () )
proof end;
end;

registration
let I be set ;
existence
ex b1 being ManySortedSet of I st
( b1 is pcs-tol-irreflexive-yielding & b1 is pcs-tol-symmetric-yielding & b1 is () )
proof end;
end;

registration
let I be set ;
existence
not for b1 being ManySortedSet of I holds b1 is ()
proof end;
end;

definition
let I be non empty set ;
let C be () ManySortedSet of I;
let i be Element of I;
:: original: .
redefine func C . i -> TolStr ;
coherence
C . i is TolStr
proof end;
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 )
proof end;
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
proof end;
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) )
proof end;
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;
coherence
proof end;
end;

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

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

registration
let I be non empty set ;
let C be () pcs-tol-symmetric-yielding ManySortedSet of I;
let i be Element of I;
cluster C . i -> pcs-tol-symmetric for TolStr ;
coherence
for b1 being TolStr st b1 = C . i holds
b1 is pcs-tol-symmetric
proof end;
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 ;

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 ;

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 ;

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^]
proof end;
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 func p ^1 -> Element of P;
coherence
^1 is Element of P
by MCART_1:10;
:: original: ^2
redefine func p ^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 ) ) by Def3;

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

registration
let P be TolStr ;
let Q be pcs-tol-reflexive TolStr ;
coherence
proof end;
end;

registration
let P be pcs-tol-reflexive TolStr ;
let Q be TolStr ;
coherence
proof end;
end;

registration
let P, Q be pcs-tol-symmetric TolStr ;
coherence
proof end;
end;

definition end;

definition
let P be pcs-Str ;
attr P is pcs-compatible means :Def22: :: PCS_0:def 22
for p, p9, q, q9 being Element of P st p (--) q & p9 <= p & 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 & p9 <= p & q9 <= q holds
p9 (--) q9 );

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

:: deftheorem defines pcs-like PCS_0:def 23 :
for P being pcs-Str holds
( P is pcs-like iff ( P is reflexive & P is transitive & P is pcs-tol-reflexive & P is pcs-tol-symmetric & P is pcs-compatible ) );

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

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

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

:: deftheorem defines pcs-total PCS_0:def 25 :
for D being set holds pcs-total D = pcs-Str(# D,(),() #);

registration
let D be set ;
coherence ;
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 ;
coherence
proof end;
end;

registration
let D be set ;
coherence
proof end;
end;

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

registration
existence
ex b1 being pcs-Str st
( b1 is strict & not b1 is empty & b1 is pcs-like )
proof end;
existence
ex b1 being pcs-Str st
( b1 is strict & not b1 is empty & b1 is anti-pcs-like )
proof end;
end;

definition end;

definition
coherence ;
end;

:: deftheorem defines pcs-empty PCS_0:def 26 :

registration
coherence ;
end;

definition
let p be set ;
coherence ;
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 ;
coherence
( pcs-singleton p is strict & not pcs-singleton p is empty & pcs-singleton p is pcs-like )
;
end;

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

:: deftheorem 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 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 :: 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 )
proof end;
redefine attr f is pcs-yielding means :: 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 )
proof end;
end;

:: deftheorem 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 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 attr f 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;
:: original: pcs-yielding
redefine attr f 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;
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
coherence
for b1 being Relation st b1 is pcs-Str-yielding holds
( b1 is TolStr-yielding & b1 is RelStr-yielding )
proof end;
coherence
for b1 being Relation st b1 is pcs-yielding holds
b1 is pcs-Str-yielding
;
coherence
for b1 being Relation st b1 is pcs-yielding holds
( b1 is reflexive-yielding & b1 is transitive-yielding & b1 is pcs-tol-reflexive-yielding & b1 is pcs-tol-symmetric-yielding )
;
end;

registration
let I be set ;
let P be pcs;
cluster I --> P -> () for ManySortedSet of I;
coherence
for b1 being ManySortedSet of I st b1 = I --> P holds
b1 is pcs-yielding
by FUNCOP_1:7;
end;

registration
let I be set ;
existence
not for b1 being ManySortedSet of I holds b1 is ()
proof end;
end;

definition
let I be non empty set ;
let C be () ManySortedSet of I;
let i be Element of I;
:: original: .
redefine func C . 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 func C . i -> pcs;
coherence
C . i is pcs
by Def33;
end;

:: Union of PCS's
definition
let P, Q be pcs-Str ;
pred P c= Q means :: PCS_0:def 34
( 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
for P being pcs-Str holds
( the carrier of P c= the carrier of P & the InternalRel of P c= the InternalRel of P & the ToleranceRel of P c= the ToleranceRel of P )
;
end;

:: deftheorem 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 & the InternalRel of P c= the InternalRel of Q & the ToleranceRel of P c= the ToleranceRel of Q ) );

theorem :: 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 & p = p1 & q = q1 & p <= q holds
p1 <= q1 ;

theorem :: 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 & p = p1 & q = q1 & p (--) q holds
p1 (--) q1 ;

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

;

definition
let C be Relation;
attr C is pcs-chain-like means :Def35: :: PCS_0:def 35
for P, Q being pcs-Str st P in rng C & Q in rng C & 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 & Q in rng C & not P c= Q holds
Q c= P );

registration
let I be set ;
let P be pcs-Str ;
cluster I --> 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
proof end;
end;

registration
existence
ex b1 being Function st
( b1 is pcs-chain-like & b1 is pcs-yielding )
proof end;
end;

registration
let I be set ;
existence
ex b1 being ManySortedSet of I st
( b1 is pcs-chain-like & b1 is () )
proof end;
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 () & the InternalRel of it = Union () & the ToleranceRel of it = Union );
existence
ex b1 being strict pcs-Str st
( the carrier of b1 = Union () & the InternalRel of b1 = Union () & the ToleranceRel of b1 = Union )
proof end;
uniqueness
for b1, b2 being strict pcs-Str st the carrier of b1 = Union () & the InternalRel of b1 = Union () & the ToleranceRel of b1 = Union & the carrier of b2 = Union () & the InternalRel of b2 = Union () & the ToleranceRel of b2 = Union 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 () & the InternalRel of b3 = Union () & the ToleranceRel of b3 = Union ) );

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

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

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

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

registration
let I be set ;
let C be reflexive-yielding () ManySortedSet of I;
coherence
proof end;
end;

registration
let I be set ;
let C be pcs-tol-reflexive-yielding () ManySortedSet of I;
coherence
proof end;
end;

registration
let I be set ;
let C be pcs-tol-symmetric-yielding () ManySortedSet of I;
coherence
proof end;
end;

registration
let I be set ;
let C be pcs-Chain of I;
coherence
proof end;
end;

:: Direct Sum of PCS's
definition
let p, q be set ;
func <%p,q%> -> ManySortedSet of {0,1} equals :: PCS_0:def 37
<%p,q%>;
coherence
<%p,q%> is ManySortedSet of {0,1}
by CARD_1:50;
end;

:: deftheorem defines <% PCS_0:def 37 :
for p, q being set holds <%p,q%> = <%p,q%>;

registration
let P, Q be 1-sorted ;
coherence
proof end;
end;

Lm3: now :: thesis: for a, b being object holds rng <%a,b%> = {a,b}
let a, b be object ; :: 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 ;
coherence
<%P,Q%> is RelStr-yielding
proof end;
end;

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

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

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

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

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

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

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

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

:: deftheorem PCS_0:def 38 :
canceled;

:: deftheorem defines pcs-sum PCS_0:def 39 :
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 & 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 end;

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) #)
proof end;

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 & q9 = q & p9 <= q9 ) or ex p9, q9 being Element of Q st
( p9 = p & q9 = q & p9 <= q9 ) ) )
proof end;

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 & q9 = q & p9 (--) q9 ) or ex p9, q9 being Element of Q st
( p9 = p & q9 = q & p9 (--) q9 ) ) )
proof end;

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
proof end;

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

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

:: Extension
definition
let P be pcs-Str ;
let a be set ;
func pcs-extension (P,a) -> strict pcs-Str means :Def39: :: PCS_0:def 40
( 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
ex b1 being strict pcs-Str st
( the carrier of b1 = {a} \/ the carrier of P & the InternalRel of b1 = [:{a}, the carrier of b1:] \/ the InternalRel of P & the ToleranceRel of b1 = ([:{a}, the carrier of b1:] \/ [: the carrier of b1,{a}:]) \/ the ToleranceRel of P )
proof end;
uniqueness
for b1, b2 being strict pcs-Str st the carrier of b1 = {a} \/ the carrier of P & the InternalRel of b1 = [:{a}, the carrier of b1:] \/ the InternalRel of P & the ToleranceRel of b1 = ([:{a}, the carrier of b1:] \/ [: the carrier of b1,{a}:]) \/ the ToleranceRel of P & the carrier of b2 = {a} \/ the carrier of P & the InternalRel of b2 = [:{a}, the carrier of b2:] \/ the InternalRel of P & 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 40 :
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 & the InternalRel of b3 = [:{a}, the carrier of b3:] \/ the InternalRel of P & 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
proof end;
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)) & 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 end;

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
proof end;

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 & q = q1 & p <= q holds
p1 <= q1
proof end;

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 & p <> a & p1 <= q1 & not a in the carrier of P holds
( q1 in the carrier of P & q1 <> a )
proof end;

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
proof end;

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 & q = q1 & p <> a & p1 <= q1 holds
p <= q
proof end;

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 & q (--) p )
proof end;

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 & q = q1 & p (--) q holds
p1 (--) q1
proof end;

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 & q = q1 & p <> a & q <> a & p1 (--) q1 holds
p (--) q
proof end;

registration
let P be reflexive pcs-Str ;
let a be set ;
coherence
pcs-extension (P,a) is reflexive
proof end;
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
proof end;

registration
let P be pcs-tol-reflexive pcs-Str ;
let a be set ;
coherence
pcs-extension (P,a) is pcs-tol-reflexive
proof end;
end;

registration
let P be pcs-tol-symmetric pcs-Str ;
let a be set ;
coherence
pcs-extension (P,a) is pcs-tol-symmetric
proof end;
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
proof end;

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
proof end;

:: Reverse
definition
let P be pcs-Str ;
func pcs-reverse P -> strict pcs-Str means :Def40: :: PCS_0:def 41
( 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
ex b1 being strict pcs-Str st
( the carrier of b1 = the carrier of P & the InternalRel of b1 = the InternalRel of P ~ & the ToleranceRel of b1 = the ToleranceRel of P  )
proof end;
uniqueness
for b1, b2 being strict pcs-Str st the carrier of b1 = the carrier of P & the InternalRel of b1 = the InternalRel of P ~ & the ToleranceRel of b1 = the ToleranceRel of P  & the carrier of b2 = the carrier of P & the InternalRel of b2 = the InternalRel of P ~ & the ToleranceRel of b2 = the ToleranceRel of P  holds
b1 = b2
;
end;

:: deftheorem Def40 defines pcs-reverse PCS_0:def 41 :
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 & the InternalRel of b2 = the InternalRel of P ~ & the ToleranceRel of b2 = the ToleranceRel of P ` ) );

registration
let P be non empty pcs-Str ;
coherence
not pcs-reverse P is empty
proof end;
end;

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

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

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 () st p = p9 & q = q9 & not p9 (--) q9 holds
p (--) q
proof end;

registration
let P be reflexive pcs-Str ;
coherence
proof end;
end;

registration
let P be transitive pcs-Str ;
coherence
proof end;
end;

registration
let P be pcs-tol-reflexive pcs-Str ;
coherence
proof end;
end;

registration
let P be pcs-tol-irreflexive pcs-Str ;
coherence
proof end;
end;

registration
let P be pcs-tol-symmetric pcs-Str ;
coherence
proof end;
end;

registration
let P be pcs-compatible pcs-Str ;
coherence
proof end;
end;

:: Times
definition
let P, Q be pcs-Str ;
func P pcs-times Q -> pcs-Str equals :: PCS_0:def 42
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 42 :
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 ;
coherence
P pcs-times Q is strict
;
end;

registration
let P, Q be non empty pcs-Str ;
cluster P 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 ()
for p1, p2 being Element of P
for q1, q2 being Element of Q st p = [p1,q1] & q = [p2,q2] holds
( p <= q iff ( p1 <= p2 & q1 <= q2 ) )
proof end;

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

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

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

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

registration
let P be pcs-Str ;
let Q be pcs-tol-reflexive pcs-Str ;
coherence
proof end;
end;

registration
let P be pcs-tol-reflexive pcs-Str ;
let Q be pcs-Str ;
coherence
proof end;
end;

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

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

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

:: deftheorem defines --> PCS_0:def 43 :
for P, Q being pcs-Str holds P --> Q = () pcs-times Q;

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

registration
let P, Q be non empty pcs-Str ;
cluster P --> 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] & q = [p2,q2] holds
( p <= q iff ( p2 <= p1 & q1 <= q2 ) )
proof end;

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] & q = [p2,q2] & p (--) q & p1 (--) p2 holds
q1 (--) q2
proof end;

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] & q = [p2,q2] & ( not p1 (--) p2 or q1 (--) q2 ) holds
p (--) q
proof end;

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

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

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

registration
let P be pcs-tol-irreflexive pcs-Str ;
let Q be pcs-Str ;
coherence ;
end;

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

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

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

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

:: deftheorem defines pcs-self-coherent PCS_0:def 44 :
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 & 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
;
end;

definition
let P be TolStr ;
let F be Subset-Family of P;
attr F is pcs-self-coherent-membered means :Def44: :: PCS_0:def 45
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 45 :
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 & b1 is pcs-self-coherent-membered )
proof end;
end;

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

:: deftheorem Def45 defines pcs-general-power-IR PCS_0:def 46 :
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 & B in D & ( for a being set st a in A holds
ex b being set st
( b in B & [a,b] in the InternalRel of P ) ) ) ) );

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

:: deftheorem Def46 defines pcs-general-power-TR PCS_0:def 47 :
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 & B in D & ( for a, b being set st a in A & 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 & B in D & ( for a being Element of P st a in A holds
ex b being Element of P st
( b in B & a <= b ) ) ) )
proof end;

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 & B in D & ( for a, b being Element of P st a in A & b in B holds
a (--) b ) ) )
proof end;

definition
let P be pcs-Str ;
let D be set ;
func pcs-general-power (P,D) -> pcs-Str equals :: PCS_0:def 48
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 48 :
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 & p9 <= q9 )
proof end;

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

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 & q9 in q holds
p9 (--) q9 by Def46;

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

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;
coherence
proof end;
end;

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

registration
let P be pcs-tol-reflexive pcs-Str ;
let D be pcs-self-coherent-membered Subset-Family of P;
coherence
proof end;
end;

registration
let P be pcs-tol-symmetric pcs-Str ;
let D be Subset-Family of P;
coherence
proof end;
end;

registration
let P be pcs-compatible pcs-Str ;
let D be Subset-Family of P;
coherence
proof end;
end;

definition
let P be pcs-Str ;
func pcs-coherent-power P -> set equals :: PCS_0:def 49
{ 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 49 :
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
proof end;
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
proof end;

registration
let P be pcs-Str ;
coherence
not pcs-coherent-power P is empty
proof end;
end;

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

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

definition
let P be pcs-Str ;
coherence ;
end;

:: deftheorem defines pcs-power PCS_0:def 50 :
for P being pcs-Str holds pcs-power P = pcs-general-power ;

registration
let P be pcs-Str ;
coherence ;
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 ;
coherence ;
end;

registration
let P be transitive pcs-Str ;
coherence ;
end;

registration
let P be pcs-tol-reflexive pcs-Str ;
coherence ;
end;

registration
let P be pcs-tol-symmetric pcs-Str ;
coherence ;
end;

registration
let P be pcs-compatible pcs-Str ;
coherence ;
end;

registration
let P be pcs;
coherence ;
end;