:: PCS_0 semantic presentation 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 proof dom (R \/ S) = (dom R) \/ (dom S) by RELAT_1:1 .= R1 \/ (dom S) by PARTFUN1:def_2 .= R1 \/ S1 by PARTFUN1:def_2 ; hence for b1 being Relation of (R1 \/ S1) st b1 = R \/ S holds b1 is total by PARTFUN1:def_2; ::_thesis: verum end; 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 proof let R1, S1 be set ; ::_thesis: for R being transitive Relation of R1 for S being transitive Relation of S1 st R1 misses S1 holds R \/ S is transitive let R be transitive Relation of R1; ::_thesis: for S being transitive Relation of S1 st R1 misses S1 holds R \/ S is transitive let S be transitive Relation of S1; ::_thesis: ( R1 misses S1 implies R \/ S is transitive ) assume A1: R1 misses S1 ; ::_thesis: R \/ S is transitive let p1, p2, p3 be set ; :: according to RELAT_2:def_8,RELAT_2:def_16 ::_thesis: ( not p1 in field (R \/ S) or not p2 in field (R \/ S) or not p3 in field (R \/ S) or not [^,^] in R \/ S or not [^,^] in R \/ S or [^,^] in R \/ S ) set RS = R \/ S; set D = field (R \/ S); assume that p1 in field (R \/ S) and p2 in field (R \/ S) and A2: p3 in field (R \/ S) and A3: [p1,p2] in R \/ S and A4: [p2,p3] in R \/ S ; ::_thesis: [^,^] in R \/ S percases ( p3 in R1 or p3 in S1 ) by A2, XBOOLE_0:def_3; supposeA5: p3 in R1 ; ::_thesis: [^,^] in R \/ S then p2 in R1 by A1, A4, Lm1; then A6: [p1,p2] in R by A1, A3, Lm1; [p2,p3] in R by A1, A4, A5, Lm1; then [p1,p3] in R by A6, RELAT_2:31; hence [^,^] in R \/ S by XBOOLE_0:def_3; ::_thesis: verum end; supposeA7: p3 in S1 ; ::_thesis: [^,^] in R \/ S then p2 in S1 by A1, A4, Lm1; then A8: [p1,p2] in S by A1, A3, Lm1; [p2,p3] in S by A1, A4, A7, Lm1; then [p1,p3] in S by A8, RELAT_2:31; hence [^,^] in R \/ S by XBOOLE_0:def_3; ::_thesis: verum end; end; end; 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) ) proof let X be ManySortedSet of I; ::_thesis: ( X = Carrier C iff for i being Element of I holds X . i = the carrier of (C . i) ) thus ( X = Carrier C implies for i being Element of I holds X . i = the carrier of (C . i) ) ::_thesis: ( ( for i being Element of I holds X . i = the carrier of (C . i) ) implies X = Carrier C ) proof assume A1: X = Carrier C ; ::_thesis: for i being Element of I holds X . i = the carrier of (C . i) let i be Element of I; ::_thesis: X . i = the carrier of (C . i) ex P being 1-sorted st ( P = C . i & X . i = the carrier of P ) by A1, PRALG_1:def_13; hence X . i = the carrier of (C . i) ; ::_thesis: verum end; assume A2: for i being Element of I holds X . i = the carrier of (C . i) ; ::_thesis: X = Carrier C for i being set st i in I holds ex P being 1-sorted st ( P = C . i & X . i = the carrier of P ) proof let i be set ; ::_thesis: ( i in I implies ex P being 1-sorted st ( P = C . i & X . i = the carrier of P ) ) assume i in I ; ::_thesis: ex P being 1-sorted st ( P = C . i & X . i = the carrier of P ) then reconsider i = i as Element of I ; take C . i ; ::_thesis: ( C . i = C . i & X . i = the carrier of (C . i) ) thus ( C . i = C . i & X . i = the carrier of (C . i) ) by A2; ::_thesis: verum end; hence X = Carrier C by PRALG_1:def_13; ::_thesis: verum 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 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 ) ) ) proof consider Q being Relation of [:R1,S1:],[:R2,S2:] such that A1: for x, y being set holds ( [x,y] in Q iff ( x in [:R1,S1:] & y in [:R2,S2:] & S1[x,y] ) ) from RELSET_1:sch_1(); take Q ; ::_thesis: for x, y being set holds ( [x,y] in Q 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 ) ) ) let x, y be set ; ::_thesis: ( [x,y] in Q 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 ) ) ) thus ( [x,y] in Q implies S1[x,y] ) by A1; ::_thesis: ( 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 ) ) implies [x,y] in Q ) given r1, s1, r2, s2 being set such that A2: x = [r1,s1] and A3: y = [r2,s2] and A4: r1 in R1 and A5: s1 in S1 and A6: r2 in R2 and A7: s2 in S2 and A8: ( [r1,r2] in R or [s1,s2] in S ) ; ::_thesis: [x,y] in Q A9: x in [:R1,S1:] by A2, A4, A5, ZFMISC_1:87; y in [:R2,S2:] by A3, A6, A7, ZFMISC_1:87; hence [x,y] in Q by A1, A2, A3, A4, A5, A6, A7, A8, A9; ::_thesis: verum end; 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 proof let A, B be Relation of [:R1,S1:],[:R2,S2:]; ::_thesis: ( ( for x, y being set holds ( [x,y] in A 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 B 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 ) ) ) ) implies A = B ) assume that A10: for x, y being set holds ( [x,y] in A iff S1[x,y] ) and A11: for x, y being set holds ( [x,y] in B iff S1[x,y] ) ; ::_thesis: A = B thus A = B from RELAT_1:sch_2(A10, A11); ::_thesis: verum 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 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 ) ) ) proof let f be Relation of [:R1,S1:],[:R2,S2:]; ::_thesis: ( f = [^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 f iff ( [r1,r2] in R or [s1,s2] in S ) ) ) thus ( f = [^R,S^] implies 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 f iff ( [r1,r2] in R or [s1,s2] in S ) ) ) ::_thesis: ( ( 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 f iff ( [r1,r2] in R or [s1,s2] in S ) ) ) implies f = [^R,S^] ) proof assume A1: f = [^R,S^] ; ::_thesis: 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 f iff ( [r1,r2] in R or [s1,s2] in S ) ) let r1 be Element of R1; ::_thesis: for r2 being Element of R2 for s1 being Element of S1 for s2 being Element of S2 holds ( [[r1,s1],[r2,s2]] in f iff ( [r1,r2] in R or [s1,s2] in S ) ) let r2 be Element of R2; ::_thesis: for s1 being Element of S1 for s2 being Element of S2 holds ( [[r1,s1],[r2,s2]] in f iff ( [r1,r2] in R or [s1,s2] in S ) ) let s1 be Element of S1; ::_thesis: for s2 being Element of S2 holds ( [[r1,s1],[r2,s2]] in f iff ( [r1,r2] in R or [s1,s2] in S ) ) let s2 be Element of S2; ::_thesis: ( [[r1,s1],[r2,s2]] in f iff ( [r1,r2] in R or [s1,s2] in S ) ) hereby ::_thesis: ( ( [r1,r2] in R or [s1,s2] in S ) implies [[r1,s1],[r2,s2]] in f ) assume [[r1,s1],[r2,s2]] in f ; ::_thesis: ( [r1,r2] in R or [s1,s2] in S ) then consider r19, s19, r29, s29 being set such that A2: [r1,s1] = [r19,s19] and A3: [r2,s2] = [r29,s29] and r19 in R1 and s19 in S1 and r29 in R2 and s29 in S2 and A4: ( [r19,r29] in R or [s19,s29] in S ) by A1, Def2; A5: r1 = r19 by A2, XTUPLE_0:1; s1 = s19 by A2, XTUPLE_0:1; hence ( [r1,r2] in R or [s1,s2] in S ) by A3, A4, A5, XTUPLE_0:1; ::_thesis: verum end; thus ( ( [r1,r2] in R or [s1,s2] in S ) implies [[r1,s1],[r2,s2]] in f ) by A1, Def2; ::_thesis: verum end; assume A6: 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 f iff ( [r1,r2] in R or [s1,s2] in S ) ) ; ::_thesis: f = [^R,S^] for x, y being set holds ( [x,y] in f iff [x,y] in [^R,S^] ) proof let x, y be set ; ::_thesis: ( [x,y] in f iff [x,y] in [^R,S^] ) thus ( [x,y] in f implies [x,y] in [^R,S^] ) ::_thesis: ( [x,y] in [^R,S^] implies [x,y] in f ) proof assume A7: [x,y] in f ; ::_thesis: [x,y] in [^R,S^] then x in dom f by XTUPLE_0:def_12; then consider x1, x2 being set such that A8: x1 in R1 and A9: x2 in S1 and A10: x = [x1,x2] by ZFMISC_1:def_2; y in rng f by A7, XTUPLE_0:def_13; then consider y1, y2 being set such that A11: y1 in R2 and A12: y2 in S2 and A13: y = [y1,y2] by ZFMISC_1:def_2; ( [x1,y1] in R or [x2,y2] in S ) by A6, A7, A8, A9, A10, A11, A12, A13; hence [x,y] in [^R,S^] by A8, A9, A10, A11, A12, A13, Def2; ::_thesis: verum end; assume [x,y] in [^R,S^] ; ::_thesis: [x,y] in f then ex r1, s1, r2, s2 being set st ( x = [r1,s1] & y = [r2,s2] & r1 in R1 & s1 in S1 & r2 in R2 & s2 in S2 & ( [r1,r2] in R or [s1,s2] in S ) ) by Def2; hence [x,y] in f by A6; ::_thesis: verum end; hence f = [^R,S^] by RELAT_1:def_2; ::_thesis: verum 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 thus dom [^R,S^] c= [:R1,S1:] ; :: according to PARTFUN1:def_2,XBOOLE_0:def_10 ::_thesis: [:R1,S1:] c= dom [^R,S^] let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in [:R1,S1:] or z in dom [^R,S^] ) assume z in [:R1,S1:] ; ::_thesis: z in dom [^R,S^] then consider x, y being set such that A1: x in R1 and A2: y in S1 and A3: z = [x,y] by ZFMISC_1:def_2; dom R = R1 by PARTFUN1:def_2; then consider a being set such that A4: [x,a] in R by A1, XTUPLE_0:def_12; dom S = S1 by PARTFUN1:def_2; then consider b being set such that A5: [y,b] in S by A2, XTUPLE_0:def_12; A6: a in R1 by A4, ZFMISC_1:87; b in S1 by A5, ZFMISC_1:87; then [[x,y],[a,b]] in [^R,S^] by A1, A2, A4, A6, Def2; hence z in dom [^R,S^] by A3, XTUPLE_0:def_12; ::_thesis: verum 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 let x be set ; :: according to RELAT_2:def_1,RELAT_2:def_9 ::_thesis: ( not x in field [^R,S^] or [^,^] in [^R,S^] ) assume A1: x in field [^R,S^] ; ::_thesis: [^,^] in [^R,S^] A2: R is_reflexive_in field R by RELAT_2:def_9; A3: S is_reflexive_in field S by RELAT_2:def_9; percases ( x in dom [^R,S^] or x in rng [^R,S^] ) by A1, XBOOLE_0:def_3; suppose x in dom [^R,S^] ; ::_thesis: [^,^] in [^R,S^] then consider y being set such that A4: [x,y] in [^R,S^] by XTUPLE_0:def_12; consider p, q, s, t being set such that A5: x = [p,q] and y = [s,t] and A6: p in R1 and A7: q in S1 and s in R1 and t in S1 and A8: ( [p,s] in R or [q,t] in S ) by A4, Def2; percases ( [p,s] in R or [q,t] in S ) by A8; suppose [p,s] in R ; ::_thesis: [^,^] in [^R,S^] then p in field R by RELAT_1:15; then [p,p] in R by A2, RELAT_2:def_1; hence [^,^] in [^R,S^] by A5, A6, A7, Def2; ::_thesis: verum end; suppose [q,t] in S ; ::_thesis: [^,^] in [^R,S^] then q in field S by RELAT_1:15; then [q,q] in S by A3, RELAT_2:def_1; hence [^,^] in [^R,S^] by A5, A6, A7, Def2; ::_thesis: verum end; end; end; suppose x in rng [^R,S^] ; ::_thesis: [^,^] in [^R,S^] then consider y being set such that A9: [y,x] in [^R,S^] by XTUPLE_0:def_13; consider p, q, s, t being set such that y = [p,q] and A10: x = [s,t] and p in R1 and q in S1 and A11: s in R1 and A12: t in S1 and A13: ( [p,s] in R or [q,t] in S ) by A9, Def2; percases ( [p,s] in R or [q,t] in S ) by A13; suppose [p,s] in R ; ::_thesis: [^,^] in [^R,S^] then s in field R by RELAT_1:15; then [s,s] in R by A2, RELAT_2:def_1; hence [^,^] in [^R,S^] by A10, A11, A12, Def2; ::_thesis: verum end; suppose [q,t] in S ; ::_thesis: [^,^] in [^R,S^] then t in field S by RELAT_1:15; then [t,t] in S by A3, RELAT_2:def_1; hence [^,^] in [^R,S^] by A10, A11, A12, Def2; ::_thesis: verum end; end; end; end; end; end; registration let R1, S1 be set ; let R be Relation of R1; let S be total reflexive Relation of S1; cluster[^R,S^] -> reflexive ; coherence [^R,S^] is reflexive proof let x be set ; :: according to RELAT_2:def_1,RELAT_2:def_9 ::_thesis: ( not x in field [^R,S^] or [^,^] in [^R,S^] ) assume x in field [^R,S^] ; ::_thesis: [^,^] in [^R,S^] then consider x1, x2 being set such that A1: x1 in R1 and A2: x2 in S1 and A3: x = [x1,x2] by ZFMISC_1:def_2; S1 = field S by ORDERS_1:12; then S is_reflexive_in S1 by RELAT_2:def_9; then [x2,x2] in S by A2, RELAT_2:def_1; hence [^,^] in [^R,S^] by A1, A2, A3, Def3; ::_thesis: verum 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 let x be set ; :: according to RELAT_2:def_1,RELAT_2:def_9 ::_thesis: ( not x in field [^R,S^] or [^,^] in [^R,S^] ) assume x in field [^R,S^] ; ::_thesis: [^,^] in [^R,S^] then consider x1, x2 being set such that A1: x1 in R1 and A2: x2 in S1 and A3: x = [x1,x2] by ZFMISC_1:def_2; R1 = field R by ORDERS_1:12; then R is_reflexive_in R1 by RELAT_2:def_9; then [x1,x1] in R by A1, RELAT_2:def_1; hence [^,^] in [^R,S^] by A1, A2, A3, Def3; ::_thesis: verum 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 let x, y be set ; :: according to RELAT_2:def_3,RELAT_2:def_11 ::_thesis: ( not x in field [^R,S^] or not y in field [^R,S^] or not [^,^] in [^R,S^] or [^,^] in [^R,S^] ) assume that x in field [^R,S^] and y in field [^R,S^] ; ::_thesis: ( not [^,^] in [^R,S^] or [^,^] in [^R,S^] ) assume [x,y] in [^R,S^] ; ::_thesis: [^,^] in [^R,S^] then consider p, q, s, t being set such that A1: x = [p,q] and A2: y = [s,t] and A3: p in R1 and A4: q in S1 and A5: s in R1 and A6: t in S1 and A7: ( [p,s] in R or [q,t] in S ) by Def2; A8: R is_symmetric_in field R by RELAT_2:def_11; A9: S is_symmetric_in field S by RELAT_2:def_11; percases ( [p,s] in R or [q,t] in S ) by A7; supposeA10: [p,s] in R ; ::_thesis: [^,^] in [^R,S^] then A11: p in field R by RELAT_1:15; s in field R by A10, RELAT_1:15; then [s,p] in R by A8, A10, A11, RELAT_2:def_3; hence [^,^] in [^R,S^] by A1, A2, A3, A4, A5, A6, Def2; ::_thesis: verum end; supposeA12: [q,t] in S ; ::_thesis: [^,^] in [^R,S^] then A13: q in field S by RELAT_1:15; t in field S by A12, RELAT_1:15; then [t,q] in S by A9, A12, A13, RELAT_2:def_3; hence [^,^] in [^R,S^] by A1, A2, A3, A4, A5, A6, Def2; ::_thesis: verum end; end; end; end; begin registration cluster empty -> total for RelStr ; coherence for b1 being RelStr st b1 is empty holds b1 is total proof let P be RelStr ; ::_thesis: ( P is empty implies P is total ) assume the carrier of P is empty ; :: according to STRUCT_0:def_1 ::_thesis: P is total hence dom the InternalRel of P = the carrier of P ; :: according to PARTFUN1:def_2,ORDERS_2:def_1 ::_thesis: verum end; 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 proof let R be Relation; ::_thesis: ( R is Poset-yielding implies R is transitive-yielding ) assume A1: R is Poset-yielding ; ::_thesis: R is transitive-yielding let S be RelStr ; :: according to PCS_0:def_4 ::_thesis: ( S in rng R implies S is transitive ) thus ( S in rng R implies S is transitive ) by A1, YELLOW16:def_5; ::_thesis: verum end; end; registration cluster Relation-like Function-like Poset-yielding for set ; existence ex b1 being Function st b1 is Poset-yielding proof set f = the Poset-yielding ManySortedSet of 0 ; take the Poset-yielding ManySortedSet of 0 ; ::_thesis: the Poset-yielding ManySortedSet of 0 is Poset-yielding thus the Poset-yielding ManySortedSet of 0 is Poset-yielding ; ::_thesis: verum end; 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 proof set f = the Poset-yielding ManySortedSet of I; take the Poset-yielding ManySortedSet of I ; ::_thesis: the Poset-yielding ManySortedSet of I is Poset-yielding thus the Poset-yielding ManySortedSet of I is Poset-yielding ; ::_thesis: verum 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 defpred S1[ set , set ] means ex R being RelStr st ( R = C . $1 & $2 = the InternalRel of R ); A1: for i being set st i in I holds ex j being set st S1[i,j] proof let i be set ; ::_thesis: ( i in I implies ex j being set st S1[i,j] ) assume A2: i in I ; ::_thesis: ex j being set st S1[i,j] then reconsider I = I as non empty set ; reconsider B = C as RelStr-yielding ManySortedSet of I ; reconsider i9 = i as Element of I by A2; take the InternalRel of (B . i9) ; ::_thesis: S1[i, the InternalRel of (B . i9)] take B . i9 ; ::_thesis: ( B . i9 = C . i & the InternalRel of (B . i9) = the InternalRel of (B . i9) ) thus ( B . i9 = C . i & the InternalRel of (B . i9) = the InternalRel of (B . i9) ) ; ::_thesis: verum end; consider M being Function such that A3: dom M = I and A4: for i being set st i in I holds S1[i,M . i] from CLASSES1:sch_1(A1); M is ManySortedSet of I by A3, PARTFUN1:def_2, RELAT_1:def_18; hence 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 ) by A4; ::_thesis: verum 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 let X, Y be ManySortedSet of I; ::_thesis: ( ( for i being set st i in I holds ex P being RelStr st ( P = C . i & X . i = the InternalRel of P ) ) & ( for i being set st i in I holds ex P being RelStr st ( P = C . i & Y . i = the InternalRel of P ) ) implies X = Y ) assume that A5: for j being set st j in I holds ex R being RelStr st ( R = C . j & X . j = the InternalRel of R ) and A6: for j being set st j in I holds ex R being RelStr st ( R = C . j & Y . j = the InternalRel of R ) ; ::_thesis: X = Y for i being set st i in I holds X . i = Y . i proof let i be set ; ::_thesis: ( i in I implies X . i = Y . i ) assume A7: i in I ; ::_thesis: X . i = Y . i then A8: ex R being RelStr st ( R = C . i & X . i = the InternalRel of R ) by A5; ex R being RelStr st ( R = C . i & Y . i = the InternalRel of R ) by A6, A7; hence X . i = Y . i by A8; ::_thesis: verum end; hence X = Y by PBOOLE:3; ::_thesis: verum 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 let X be ManySortedSet of I; ::_thesis: ( X = pcs-InternalRels C iff for i being Element of I holds X . i = the InternalRel of (C . i) ) thus ( X = pcs-InternalRels C implies for i being Element of I holds X . i = the InternalRel of (C . i) ) ::_thesis: ( ( for i being Element of I holds X . i = the InternalRel of (C . i) ) implies X = pcs-InternalRels C ) proof assume A1: X = pcs-InternalRels C ; ::_thesis: for i being Element of I holds X . i = the InternalRel of (C . i) let i be Element of I; ::_thesis: X . i = the InternalRel of (C . i) ex P being RelStr st ( P = C . i & X . i = the InternalRel of P ) by A1, Def5; hence X . i = the InternalRel of (C . i) ; ::_thesis: verum end; assume A2: for i being Element of I holds X . i = the InternalRel of (C . i) ; ::_thesis: X = pcs-InternalRels C for i being set st i in I holds ex P being RelStr st ( P = C . i & X . i = the InternalRel of P ) proof let i be set ; ::_thesis: ( i in I implies ex P being RelStr st ( P = C . i & X . i = the InternalRel of P ) ) assume i in I ; ::_thesis: ex P being RelStr st ( P = C . i & X . i = the InternalRel of P ) then reconsider i = i as Element of I ; take C . i ; ::_thesis: ( C . i = C . i & X . i = the InternalRel of (C . i) ) thus ( C . i = C . i & X . i = the InternalRel of (C . i) ) by A2; ::_thesis: verum end; hence X = pcs-InternalRels C by Def5; ::_thesis: verum 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; cluster pcs-InternalRels C -> Relation-yielding ; coherence pcs-InternalRels C is Relation-yielding proof set IR = pcs-InternalRels C; let i be set ; :: according to FUNCOP_1:def_11 ::_thesis: ( not i in proj1 (pcs-InternalRels C) or (pcs-InternalRels C) . i is set ) assume i in dom (pcs-InternalRels C) ; ::_thesis: (pcs-InternalRels C) . i is set then ex P being RelStr st ( P = C . i & (pcs-InternalRels C) . i = the InternalRel of P ) by Def5; hence (pcs-InternalRels C) . i is set ; ::_thesis: verum 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; clusterC . i -> transitive for RelStr ; coherence for b1 being RelStr st b1 = C . i holds b1 is transitive proof dom C = I by PARTFUN1:def_2; then C . i in rng C by FUNCT_1:3; hence for b1 being RelStr st b1 = C . i holds b1 is transitive by Def4; ::_thesis: verum end; 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 proof let P be TolStr ; ::_thesis: ( P is empty implies TolStr(# the carrier of P, the ToleranceRel of P #) = emptyTolStr ) assume P is empty ; ::_thesis: TolStr(# the carrier of P, the ToleranceRel of P #) = emptyTolStr then the carrier of P = {} ; hence TolStr(# the carrier of P, the ToleranceRel of P #) = emptyTolStr ; ::_thesis: verum end; 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 proof let P be TolStr ; ::_thesis: ( P is pcs-tol-reflexive implies P is pcs-tol-total ) assume P is pcs-tol-reflexive ; ::_thesis: P is pcs-tol-total then the ToleranceRel of P is_reflexive_in the carrier of P by Def9; then dom the ToleranceRel of P = the carrier of P by ORDERS_1:13; hence the ToleranceRel of P is total by PARTFUN1:def_2; :: according to PCS_0:def_8 ::_thesis: verum end; 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 ) proof let P be TolStr ; ::_thesis: ( P is empty implies ( P is pcs-tol-reflexive & P is pcs-tol-irreflexive & P is pcs-tol-symmetric ) ) assume A1: P is empty ; ::_thesis: ( P is pcs-tol-reflexive & P is pcs-tol-irreflexive & P is pcs-tol-symmetric ) then TolStr(# the carrier of P, the ToleranceRel of P #) = emptyTolStr by Th2; then A2: the carrier of P = field the ToleranceRel of P ; hence the ToleranceRel of P is_reflexive_in the carrier of P by A1, RELAT_2:def_9; :: according to PCS_0:def_9 ::_thesis: ( P is pcs-tol-irreflexive & P is pcs-tol-symmetric ) thus the ToleranceRel of P is_irreflexive_in the carrier of P by A1, A2, RELAT_2:def_10; :: according to PCS_0:def_10 ::_thesis: P is pcs-tol-symmetric thus the ToleranceRel of P is_symmetric_in the carrier of P by A1, A2, RELAT_2:def_11; :: according to PCS_0:def_11 ::_thesis: verum end; end; registration cluster empty strict for TolStr ; existence ex b1 being TolStr st ( b1 is empty & b1 is strict ) proof take emptyTolStr ; ::_thesis: ( emptyTolStr is empty & emptyTolStr is strict ) thus ( emptyTolStr is empty & emptyTolStr is strict ) ; ::_thesis: verum 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 set TR = the ToleranceRel of P; A1: field the ToleranceRel of P = the carrier of P by ORDERS_1:12; the ToleranceRel of P is_reflexive_in the carrier of P by Def9; hence the ToleranceRel of P is reflexive by A1, RELAT_2:def_9; ::_thesis: verum end; end; registration let P be pcs-tol-irreflexive TolStr ; cluster the ToleranceRel of P -> irreflexive ; coherence the ToleranceRel of P is irreflexive proof set TR = the ToleranceRel of P; A1: the ToleranceRel of P is_irreflexive_in the carrier of P by Def10; let x be set ; :: according to RELAT_2:def_2,RELAT_2:def_10 ::_thesis: ( not x in field the ToleranceRel of P or not [^,^] in the ToleranceRel of P ) assume x in field the ToleranceRel of P ; ::_thesis: not [^,^] in the ToleranceRel of P assume A2: [x,x] in the ToleranceRel of P ; ::_thesis: contradiction then x in dom the ToleranceRel of P by XTUPLE_0:def_12; hence contradiction by A1, A2, RELAT_2:def_2; ::_thesis: verum end; end; registration let P be pcs-tol-symmetric TolStr ; cluster the ToleranceRel of P -> symmetric ; coherence the ToleranceRel of P is symmetric proof set TR = the ToleranceRel of P; A1: the ToleranceRel of P is_symmetric_in the carrier of P by Def11; let x, y be set ; :: according to RELAT_2:def_3,RELAT_2:def_11 ::_thesis: ( not x in field the ToleranceRel of P or not y in field the ToleranceRel of P or not [^,^] in the ToleranceRel of P or [^,^] in the ToleranceRel of P ) assume that x in field the ToleranceRel of P and y in field the ToleranceRel of P ; ::_thesis: ( not [^,^] in the ToleranceRel of P or [^,^] in the ToleranceRel of P ) assume A2: [x,y] in the ToleranceRel of P ; ::_thesis: [^,^] in the ToleranceRel of P then A3: x in dom the ToleranceRel of P by XTUPLE_0:def_12; y in rng the ToleranceRel of P by A2, XTUPLE_0:def_13; hence [^,^] in the ToleranceRel of P by A1, A2, A3, RELAT_2:def_3; ::_thesis: verum 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 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) proof let x, y be Element of P; ::_thesis: ( (P,x,y) implies (P,y,x) ) assume A1: [x,y] in the ToleranceRel of P ; :: according to PCS_0:def_7 ::_thesis: (P,y,x) then A2: x in the carrier of P by ZFMISC_1:87; the ToleranceRel of P is_symmetric_in the carrier of P by Def11; hence [y,x] in the ToleranceRel of P by A1, A2, RELAT_2:def_3; :: according to PCS_0:def_7 ::_thesis: verum end; 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 ) proof set P = TolStr(# D,(nabla D) #); set TR = the ToleranceRel of TolStr(# D,(nabla D) #); A1: field the ToleranceRel of TolStr(# D,(nabla D) #) = the carrier of TolStr(# D,(nabla D) #) by ORDERS_1:12; hence the ToleranceRel of TolStr(# D,(nabla D) #) is_reflexive_in the carrier of TolStr(# D,(nabla D) #) by RELAT_2:def_9; :: according to PCS_0:def_9 ::_thesis: TolStr(# D,(nabla D) #) is pcs-tol-symmetric thus the ToleranceRel of TolStr(# D,(nabla D) #) is_symmetric_in the carrier of TolStr(# D,(nabla D) #) by A1, RELAT_2:def_11; :: according to PCS_0:def_11 ::_thesis: verum 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 set P = TolStr(# D,({} (D,D)) #); thus the ToleranceRel of TolStr(# D,({} (D,D)) #) is_irreflexive_in the carrier of TolStr(# D,({} (D,D)) #) :: according to PCS_0:def_10 ::_thesis: TolStr(# D,({} (D,D)) #) is pcs-tol-symmetric proof let x be set ; :: according to RELAT_2:def_2 ::_thesis: ( not x in the carrier of TolStr(# D,({} (D,D)) #) or not [^,^] in the ToleranceRel of TolStr(# D,({} (D,D)) #) ) thus ( not x in the carrier of TolStr(# D,({} (D,D)) #) or not [^,^] in the ToleranceRel of TolStr(# D,({} (D,D)) #) ) ; ::_thesis: verum end; let x be set ; :: according to RELAT_2:def_3,PCS_0:def_11 ::_thesis: for b1 being set holds ( not x in the carrier of TolStr(# D,({} (D,D)) #) or not b1 in the carrier of TolStr(# D,({} (D,D)) #) or not [^,^] in the ToleranceRel of TolStr(# D,({} (D,D)) #) or [^,^] in the ToleranceRel of TolStr(# D,({} (D,D)) #) ) thus for b1 being set holds ( not x in the carrier of TolStr(# D,({} (D,D)) #) or not b1 in the carrier of TolStr(# D,({} (D,D)) #) or not [^,^] in the ToleranceRel of TolStr(# D,({} (D,D)) #) or [^,^] in the ToleranceRel of TolStr(# D,({} (D,D)) #) ) ; ::_thesis: verum end; 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 ) proof take P = TolStr(# {{}},(nabla {{}}) #); ::_thesis: ( P is strict & not P is empty & P is pcs-tol-reflexive & P is pcs-tol-symmetric ) thus P is strict ; ::_thesis: ( not P is empty & P is pcs-tol-reflexive & P is pcs-tol-symmetric ) thus not the carrier of P is empty ; :: according to STRUCT_0:def_1 ::_thesis: ( P is pcs-tol-reflexive & P is pcs-tol-symmetric ) thus ( P is pcs-tol-reflexive & P is pcs-tol-symmetric ) ; ::_thesis: verum end; 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 ) proof take P = TolStr(# {{}},({} ({{}},{{}})) #); ::_thesis: ( P is strict & not P is empty & P is pcs-tol-irreflexive & P is pcs-tol-symmetric ) thus P is strict ; ::_thesis: ( not P is empty & P is pcs-tol-irreflexive & P is pcs-tol-symmetric ) thus not the carrier of P is empty ; :: according to STRUCT_0:def_1 ::_thesis: ( P is pcs-tol-irreflexive & P is pcs-tol-symmetric ) thus ( P is pcs-tol-irreflexive & P is pcs-tol-symmetric ) ; ::_thesis: verum end; 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 ) proof hereby ::_thesis: ( ( for x being set st x in dom f holds f . x is TolStr ) implies f is TolStr-yielding ) assume A1: f is TolStr-yielding ; ::_thesis: for x being set st x in dom f holds f . x is TolStr let x be set ; ::_thesis: ( x in dom f implies f . x is TolStr ) assume x in dom f ; ::_thesis: f . x is TolStr then f . x in rng f by FUNCT_1:3; hence f . x is TolStr by A1, Def13; ::_thesis: verum end; assume A2: for x being set st x in dom f holds f . x is TolStr ; ::_thesis: f is TolStr-yielding let P be set ; :: according to PCS_0:def_13 ::_thesis: ( P in rng f implies P is TolStr ) assume P in rng f ; ::_thesis: P is TolStr then ex x being set st ( x in dom f & f . x = P ) by FUNCT_1:def_3; hence P is TolStr by A2; ::_thesis: verum 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 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 ) proof let f be Relation; ::_thesis: ( f is empty implies ( f is pcs-tol-reflexive-yielding & f is pcs-tol-irreflexive-yielding & f is pcs-tol-symmetric-yielding ) ) assume A1: f is empty ; ::_thesis: ( f is pcs-tol-reflexive-yielding & f is pcs-tol-irreflexive-yielding & f is pcs-tol-symmetric-yielding ) thus f is pcs-tol-reflexive-yielding ::_thesis: ( f is pcs-tol-irreflexive-yielding & f is pcs-tol-symmetric-yielding ) proof let i be set ; :: according to PCS_0:def_16 ::_thesis: ( i is TolStr & i in rng f implies i is pcs-tol-reflexive ) thus ( i is TolStr & i in rng f implies i is pcs-tol-reflexive ) by A1; ::_thesis: verum end; thus f is pcs-tol-irreflexive-yielding ::_thesis: f is pcs-tol-symmetric-yielding proof let i be set ; :: according to PCS_0:def_17 ::_thesis: ( i is TolStr & i in rng f implies i is pcs-tol-irreflexive ) thus ( i is TolStr & i in rng f implies i is pcs-tol-irreflexive ) by A1; ::_thesis: verum end; let i be set ; :: according to PCS_0:def_18 ::_thesis: ( i is TolStr & i in rng f implies i is pcs-tol-symmetric ) thus ( i is TolStr & i in rng f implies i is pcs-tol-symmetric ) by A1; ::_thesis: verum end; 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 proof I --> P is () proof let i be set ; :: according to PCS_0:def_15 ::_thesis: ( i in I implies (I --> P) . i is TolStr ) thus ( i in I implies (I --> P) . i is TolStr ) by FUNCOP_1:7; ::_thesis: verum end; hence for b1 being ManySortedSet of I st b1 = I --> P holds b1 is TolStr-yielding ; ::_thesis: verum end; 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 proof set f = I --> P; I --> P is pcs-tol-reflexive-yielding proof let S be TolStr ; :: according to PCS_0:def_16 ::_thesis: ( S in rng (I --> P) implies S is pcs-tol-reflexive ) assume S in rng (I --> P) ; ::_thesis: S is pcs-tol-reflexive hence S is pcs-tol-reflexive by TARSKI:def_1; ::_thesis: verum end; hence for b1 being ManySortedSet of I st b1 = I --> P holds b1 is pcs-tol-reflexive-yielding ; ::_thesis: verum end; 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 proof set f = I --> P; I --> P is pcs-tol-irreflexive-yielding proof let S be TolStr ; :: according to PCS_0:def_17 ::_thesis: ( S in rng (I --> P) implies S is pcs-tol-irreflexive ) assume S in rng (I --> P) ; ::_thesis: S is pcs-tol-irreflexive hence S is pcs-tol-irreflexive by TARSKI:def_1; ::_thesis: verum end; hence for b1 being ManySortedSet of I st b1 = I --> P holds b1 is pcs-tol-irreflexive-yielding ; ::_thesis: verum end; 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 proof set f = I --> P; I --> P is pcs-tol-symmetric-yielding proof let S be TolStr ; :: according to PCS_0:def_18 ::_thesis: ( S in rng (I --> P) implies S is pcs-tol-symmetric ) assume S in rng (I --> P) ; ::_thesis: S is pcs-tol-symmetric hence S is pcs-tol-symmetric by TARSKI:def_1; ::_thesis: verum end; hence for b1 being ManySortedSet of I st b1 = I --> P holds b1 is pcs-tol-symmetric-yielding ; ::_thesis: verum end; 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 proof let f be Function; ::_thesis: ( f is TolStr-yielding implies f is 1-sorted-yielding ) assume A1: f is TolStr-yielding ; ::_thesis: f is 1-sorted-yielding let x be set ; :: according to PRALG_1:def_11 ::_thesis: ( not x in proj1 f or f . x is 1-sorted ) thus ( not x in proj1 f or f . x is 1-sorted ) by A1, Def14; ::_thesis: verum end; 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 () ) proof take I --> TolStr(# 0,(nabla 0) #) ; ::_thesis: ( I --> TolStr(# 0,(nabla 0) #) is pcs-tol-reflexive-yielding & I --> TolStr(# 0,(nabla 0) #) is pcs-tol-symmetric-yielding & I --> TolStr(# 0,(nabla 0) #) is () ) thus ( I --> TolStr(# 0,(nabla 0) #) is pcs-tol-reflexive-yielding & I --> TolStr(# 0,(nabla 0) #) is pcs-tol-symmetric-yielding & I --> TolStr(# 0,(nabla 0) #) is () ) ; ::_thesis: verum end; 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 () ) proof take I --> TolStr(# 0,({} (0,0)) #) ; ::_thesis: ( I --> TolStr(# 0,({} (0,0)) #) is pcs-tol-irreflexive-yielding & I --> TolStr(# 0,({} (0,0)) #) is pcs-tol-symmetric-yielding & I --> TolStr(# 0,({} (0,0)) #) is () ) thus ( I --> TolStr(# 0,({} (0,0)) #) is pcs-tol-irreflexive-yielding & I --> TolStr(# 0,({} (0,0)) #) is pcs-tol-symmetric-yielding & I --> TolStr(# 0,({} (0,0)) #) is () ) ; ::_thesis: verum end; 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 () proof set R = the TolStr ; take I --> the TolStr ; ::_thesis: I --> the TolStr is () thus I --> the TolStr is () ; ::_thesis: verum end; 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 proof dom C = I by PARTFUN1:def_2; hence C . i is TolStr by Def14; ::_thesis: verum 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 defpred S1[ set , set ] means ex R being TolStr st ( R = C . $1 & $2 = the ToleranceRel of R ); A1: for i being set st i in I holds ex j being set st S1[i,j] proof let i be set ; ::_thesis: ( i in I implies ex j being set st S1[i,j] ) assume A2: i in I ; ::_thesis: ex j being set st S1[i,j] then reconsider I = I as non empty set ; reconsider B = C as () ManySortedSet of I ; reconsider i9 = i as Element of I by A2; take the ToleranceRel of (B . i9) ; ::_thesis: S1[i, the ToleranceRel of (B . i9)] take B . i9 ; ::_thesis: ( B . i9 = C . i & the ToleranceRel of (B . i9) = the ToleranceRel of (B . i9) ) thus ( B . i9 = C . i & the ToleranceRel of (B . i9) = the ToleranceRel of (B . i9) ) ; ::_thesis: verum end; consider M being Function such that A3: dom M = I and A4: for i being set st i in I holds S1[i,M . i] from CLASSES1:sch_1(A1); M is ManySortedSet of I by A3, PARTFUN1:def_2, RELAT_1:def_18; hence 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 ) by A4; ::_thesis: verum 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 let X, Y be ManySortedSet of I; ::_thesis: ( ( for i being set st i in I holds ex P being TolStr st ( P = C . i & X . i = the ToleranceRel of P ) ) & ( for i being set st i in I holds ex P being TolStr st ( P = C . i & Y . i = the ToleranceRel of P ) ) implies X = Y ) assume that A5: for j being set st j in I holds ex R being TolStr st ( R = C . j & X . j = the ToleranceRel of R ) and A6: for j being set st j in I holds ex R being TolStr st ( R = C . j & Y . j = the ToleranceRel of R ) ; ::_thesis: X = Y for i being set st i in I holds X . i = Y . i proof let i be set ; ::_thesis: ( i in I implies X . i = Y . i ) assume A7: i in I ; ::_thesis: X . i = Y . i then A8: ex R being TolStr st ( R = C . i & X . i = the ToleranceRel of R ) by A5; ex R being TolStr st ( R = C . i & Y . i = the ToleranceRel of R ) by A6, A7; hence X . i = Y . i by A8; ::_thesis: verum end; hence X = Y by PBOOLE:3; ::_thesis: verum 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 let X be ManySortedSet of I; ::_thesis: ( X = pcs-ToleranceRels C iff for i being Element of I holds X . i = the ToleranceRel of (C . i) ) thus ( X = pcs-ToleranceRels C implies for i being Element of I holds X . i = the ToleranceRel of (C . i) ) ::_thesis: ( ( for i being Element of I holds X . i = the ToleranceRel of (C . i) ) implies X = pcs-ToleranceRels C ) proof assume A1: X = pcs-ToleranceRels C ; ::_thesis: for i being Element of I holds X . i = the ToleranceRel of (C . i) let i be Element of I; ::_thesis: X . i = the ToleranceRel of (C . i) ex P being TolStr st ( P = C . i & X . i = the ToleranceRel of P ) by A1, Def19; hence X . i = the ToleranceRel of (C . i) ; ::_thesis: verum end; assume A2: for i being Element of I holds X . i = the ToleranceRel of (C . i) ; ::_thesis: X = pcs-ToleranceRels C for i being set st i in I holds ex P being TolStr st ( P = C . i & X . i = the ToleranceRel of P ) proof let i be set ; ::_thesis: ( i in I implies ex P being TolStr st ( P = C . i & X . i = the ToleranceRel of P ) ) assume i in I ; ::_thesis: ex P being TolStr st ( P = C . i & X . i = the ToleranceRel of P ) then reconsider i = i as Element of I ; take C . i ; ::_thesis: ( C . i = C . i & X . i = the ToleranceRel of (C . i) ) thus ( C . i = C . i & X . i = the ToleranceRel of (C . i) ) by A2; ::_thesis: verum end; hence X = pcs-ToleranceRels C by Def19; ::_thesis: verum 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; cluster pcs-ToleranceRels C -> Relation-yielding ; coherence pcs-ToleranceRels C is Relation-yielding proof set TR = pcs-ToleranceRels C; let i be set ; :: according to FUNCOP_1:def_11 ::_thesis: ( not i in proj1 (pcs-ToleranceRels C) or (pcs-ToleranceRels C) . i is set ) assume i in dom (pcs-ToleranceRels C) ; ::_thesis: (pcs-ToleranceRels C) . i is set then ex P being TolStr st ( P = C . i & (pcs-ToleranceRels C) . i = the ToleranceRel of P ) by Def19; hence (pcs-ToleranceRels C) . i is set ; ::_thesis: verum 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; clusterC . i -> pcs-tol-reflexive for TolStr ; coherence for b1 being TolStr st b1 = C . i holds b1 is pcs-tol-reflexive proof dom C = I by PARTFUN1:def_2; then C . i in rng C by FUNCT_1:3; hence for b1 being TolStr st b1 = C . i holds b1 is pcs-tol-reflexive by Def16; ::_thesis: verum 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; clusterC . i -> pcs-tol-irreflexive for TolStr ; coherence for b1 being TolStr st b1 = C . i holds b1 is pcs-tol-irreflexive proof dom C = I by PARTFUN1:def_2; then C . i in rng C by FUNCT_1:3; hence for b1 being TolStr st b1 = C . i holds b1 is pcs-tol-irreflexive by Def17; ::_thesis: verum 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; clusterC . i -> pcs-tol-symmetric for TolStr ; coherence for b1 being TolStr st b1 = C . i holds b1 is pcs-tol-symmetric proof dom C = I by PARTFUN1:def_2; then C . i in rng C by FUNCT_1:3; hence for b1 being TolStr st b1 = C . i holds b1 is pcs-tol-symmetric by Def18; ::_thesis: verum 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 proof let P, Q be TolStr ; ::_thesis: ( TolStr(# the carrier of P, the ToleranceRel of P #) = TolStr(# the carrier of Q, the ToleranceRel of Q #) & P is pcs-tol-reflexive implies Q is pcs-tol-reflexive ) assume that A1: TolStr(# the carrier of P, the ToleranceRel of P #) = TolStr(# the carrier of Q, the ToleranceRel of Q #) and A2: the ToleranceRel of P is_reflexive_in the carrier of P ; :: according to PCS_0:def_9 ::_thesis: Q is pcs-tol-reflexive let x be set ; :: according to RELAT_2:def_1,PCS_0:def_9 ::_thesis: ( not x in the carrier of Q or [^,^] in the ToleranceRel of Q ) assume x in the carrier of Q ; ::_thesis: [^,^] in the ToleranceRel of Q hence [^,^] in the ToleranceRel of Q by A1, A2, RELAT_2:def_1; ::_thesis: verum end; 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 proof let P, Q be TolStr ; ::_thesis: ( TolStr(# the carrier of P, the ToleranceRel of P #) = TolStr(# the carrier of Q, the ToleranceRel of Q #) & P is pcs-tol-irreflexive implies Q is pcs-tol-irreflexive ) assume that A1: TolStr(# the carrier of P, the ToleranceRel of P #) = TolStr(# the carrier of Q, the ToleranceRel of Q #) and A2: the ToleranceRel of P is_irreflexive_in the carrier of P ; :: according to PCS_0:def_10 ::_thesis: Q is pcs-tol-irreflexive let x be set ; :: according to RELAT_2:def_2,PCS_0:def_10 ::_thesis: ( not x in the carrier of Q or not [^,^] in the ToleranceRel of Q ) assume x in the carrier of Q ; ::_thesis: not [^,^] in the ToleranceRel of Q hence not [^,^] in the ToleranceRel of Q by A1, A2, RELAT_2:def_2; ::_thesis: verum end; 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 proof let P, Q be TolStr ; ::_thesis: ( TolStr(# the carrier of P, the ToleranceRel of P #) = TolStr(# the carrier of Q, the ToleranceRel of Q #) & P is pcs-tol-symmetric implies Q is pcs-tol-symmetric ) assume that A1: TolStr(# the carrier of P, the ToleranceRel of P #) = TolStr(# the carrier of Q, the ToleranceRel of Q #) and A2: the ToleranceRel of P is_symmetric_in the carrier of P ; :: according to PCS_0:def_11 ::_thesis: Q is pcs-tol-symmetric let x, y be set ; :: according to RELAT_2:def_3,PCS_0:def_11 ::_thesis: ( not x in the carrier of Q or not y in the carrier of Q or not [^,^] in the ToleranceRel of Q or [^,^] in the ToleranceRel of Q ) assume x in the carrier of Q ; ::_thesis: ( not y in the carrier of Q or not [^,^] in the ToleranceRel of Q or [^,^] in the ToleranceRel of Q ) hence ( not y in the carrier of Q or not [^,^] in the ToleranceRel of Q or [^,^] in the ToleranceRel of Q ) by A1, A2, RELAT_2:def_3; ::_thesis: verum end; 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 [p,q] is Element of [^P,Q^] ; hence [^,^] is Element of [^P,Q^] ; ::_thesis: verum 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 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 ) ) proof let S1, S2 be non empty TolStr ; ::_thesis: 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 ) ) let a, c be Element of S1; ::_thesis: for b, d being Element of S2 holds ( [^a,b^] (--) [^c,d^] iff ( a (--) c or b (--) d ) ) let b, d be Element of S2; ::_thesis: ( [^a,b^] (--) [^c,d^] iff ( a (--) c or b (--) d ) ) set I1 = the ToleranceRel of S1; set I2 = the ToleranceRel of S2; set x = [[a,b],[c,d]]; thus ( not [^a,b^] (--) [^c,d^] or a (--) c or b (--) d ) ::_thesis: ( ( a (--) c or b (--) d ) implies [^a,b^] (--) [^c,d^] ) proof assume [^a,b^] (--) [^c,d^] ; ::_thesis: ( a (--) c or b (--) d ) then [[a,b],[c,d]] in the ToleranceRel of [^S1,S2^] by Def7; then ( [a,c] in the ToleranceRel of S1 or [b,d] in the ToleranceRel of S2 ) by Def3; hence ( a (--) c or b (--) d ) by Def7; ::_thesis: verum end; assume ( a (--) c or b (--) d ) ; ::_thesis: [^a,b^] (--) [^c,d^] then ( [(([[a,b],[c,d]] `1) `1),(([[a,b],[c,d]] `2) `1)] in the ToleranceRel of S1 or [(([[a,b],[c,d]] `1) `2),(([[a,b],[c,d]] `2) `2)] in the ToleranceRel of S2 ) by Def7; hence [[a,b],[c,d]] in the ToleranceRel of [^S1,S2^] by Def3; :: according to PCS_0:def_7 ::_thesis: verum end; 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 let S1, S2 be non empty TolStr ; ::_thesis: for x, y being Element of [^S1,S2^] holds ( x (--) y iff ( x ^`1 (--) y ^`1 or x ^`2 (--) y ^`2 ) ) let x, y be Element of [^S1,S2^]; ::_thesis: ( x (--) y iff ( x ^`1 (--) y ^`1 or x ^`2 (--) y ^`2 ) ) A1: ex a, b being set st ( a in the carrier of S1 & b in the carrier of S2 & x = [a,b] ) by ZFMISC_1:def_2; A2: ex c, d being set st ( c in the carrier of S1 & d in the carrier of S2 & y = [c,d] ) by ZFMISC_1:def_2; A3: x = [(x ^`1),(x ^`2)] by A1, MCART_1:8; y = [(y ^`1),(y ^`2)] by A2, MCART_1:8; hence ( x (--) y iff ( x ^`1 (--) y ^`1 or x ^`2 (--) y ^`2 ) ) by A3, Th6; ::_thesis: verum end; 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 proof let x be set ; :: according to RELAT_2:def_1,PCS_0:def_9 ::_thesis: ( not x in the carrier of [^P,Q^] or [^,^] in the ToleranceRel of [^P,Q^] ) assume x in the carrier of [^P,Q^] ; ::_thesis: [^,^] in the ToleranceRel of [^P,Q^] then consider x1, x2 being set such that A1: x1 in the carrier of P and A2: x2 in the carrier of Q and A3: x = [x1,x2] by ZFMISC_1:def_2; reconsider D2 = the carrier of Q as non empty set by A2; reconsider TQ = the ToleranceRel of Q as Relation of D2 ; D2 = field TQ by ORDERS_1:12; then TQ is_reflexive_in D2 by RELAT_2:def_9; then [x2,x2] in TQ by A2, RELAT_2:def_1; hence [^,^] in the ToleranceRel of [^P,Q^] by A1, A2, A3, Def3; ::_thesis: verum end; 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 proof let x be set ; :: according to RELAT_2:def_1,PCS_0:def_9 ::_thesis: ( not x in the carrier of [^P,Q^] or [^,^] in the ToleranceRel of [^P,Q^] ) assume x in the carrier of [^P,Q^] ; ::_thesis: [^,^] in the ToleranceRel of [^P,Q^] then consider x1, x2 being set such that A1: x1 in the carrier of P and A2: x2 in the carrier of Q and A3: x = [x1,x2] by ZFMISC_1:def_2; reconsider D1 = the carrier of P as non empty set by A1; reconsider TP = the ToleranceRel of P as Relation of D1 ; D1 = field TP by ORDERS_1:12; then TP is_reflexive_in D1 by RELAT_2:def_9; then [x1,x1] in TP by A1, RELAT_2:def_1; hence [^,^] in the ToleranceRel of [^P,Q^] by A1, A2, A3, Def3; ::_thesis: verum end; end; registration let P, Q be pcs-tol-symmetric TolStr ; cluster[^P,Q^] -> pcs-tol-symmetric ; coherence [^P,Q^] is pcs-tol-symmetric proof set R = [^P,Q^]; set TR = the ToleranceRel of [^P,Q^]; A1: the ToleranceRel of [^P,Q^] is_symmetric_in field the ToleranceRel of [^P,Q^] by RELAT_2:def_11; let x, y be set ; :: according to RELAT_2:def_3,PCS_0:def_11 ::_thesis: ( not x in the carrier of [^P,Q^] or not y in the carrier of [^P,Q^] or not [^,^] in the ToleranceRel of [^P,Q^] or [^,^] in the ToleranceRel of [^P,Q^] ) assume that x in the carrier of [^P,Q^] and y in the carrier of [^P,Q^] ; ::_thesis: ( not [^,^] in the ToleranceRel of [^P,Q^] or [^,^] in the ToleranceRel of [^P,Q^] ) assume A2: [x,y] in the ToleranceRel of [^P,Q^] ; ::_thesis: [^,^] in the ToleranceRel of [^P,Q^] then A3: x in field the ToleranceRel of [^P,Q^] by RELAT_1:15; y in field the ToleranceRel of [^P,Q^] by A2, RELAT_1:15; hence [^,^] in the ToleranceRel of [^P,Q^] by A1, A2, A3, RELAT_2:def_3; ::_thesis: verum end; 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 & 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 ; attrP is pcs-like means :Def23: :: PCS_0:def 23 ( P is reflexive & P is transitive & P is pcs-tol-reflexive & P is pcs-tol-symmetric & P is pcs-compatible ); attrP is anti-pcs-like means :Def24: :: 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 Def23 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 Def24 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 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 & b1 is transitive & b1 is pcs-tol-reflexive & b1 is pcs-tol-symmetric & 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 & b1 is transitive & b1 is pcs-tol-reflexive & b1 is pcs-tol-symmetric & 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 & b1 is transitive & b1 is pcs-tol-irreflexive & b1 is pcs-tol-symmetric & 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 & b1 is transitive & b1 is pcs-tol-irreflexive & b1 is pcs-tol-symmetric & 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 & pcs-total D is transitive & pcs-total D is pcs-tol-reflexive & pcs-total D is pcs-tol-symmetric ) proof set P = pcs-total D; set IR = the InternalRel of (pcs-total D); set TR = the ToleranceRel of (pcs-total D); A1: field the InternalRel of (pcs-total D) = the carrier of (pcs-total D) by ORDERS_1:12; hence the InternalRel of (pcs-total D) is_reflexive_in the carrier of (pcs-total D) by RELAT_2:def_9; :: according to ORDERS_2:def_2 ::_thesis: ( pcs-total D is transitive & pcs-total D is pcs-tol-reflexive & pcs-total D is pcs-tol-symmetric ) thus the InternalRel of (pcs-total D) is_transitive_in the carrier of (pcs-total D) by A1, RELAT_2:def_16; :: according to ORDERS_2:def_3 ::_thesis: ( pcs-total D is pcs-tol-reflexive & pcs-total D is pcs-tol-symmetric ) thus the ToleranceRel of (pcs-total D) is_reflexive_in the carrier of (pcs-total D) by A1, RELAT_2:def_9; :: according to PCS_0:def_9 ::_thesis: pcs-total D is pcs-tol-symmetric thus the ToleranceRel of (pcs-total D) is_symmetric_in the carrier of (pcs-total D) by A1, RELAT_2:def_11; :: according to PCS_0:def_11 ::_thesis: verum end; end; registration let D be set ; cluster pcs-total D -> pcs-like ; coherence pcs-total D is pcs-like proof set P = pcs-total D; thus ( pcs-total D is reflexive & pcs-total D is transitive ) ; :: according to PCS_0:def_23 ::_thesis: ( pcs-total D is pcs-tol-reflexive & pcs-total D is pcs-tol-symmetric & pcs-total D is pcs-compatible ) thus ( pcs-total D is pcs-tol-reflexive & pcs-total D is pcs-tol-symmetric ) ; ::_thesis: pcs-total D is pcs-compatible let p, p9, q, q9 be Element of (pcs-total D); :: according to PCS_0:def_22 ::_thesis: ( p (--) q & p9 <= p & q9 <= q implies p9 (--) q9 ) assume p (--) q ; ::_thesis: ( not p9 <= p or not q9 <= q or p9 (--) q9 ) assume that A1: p9 <= p and q9 <= q ; ::_thesis: p9 (--) q9 [p9,p] in [:D,D:] by A1, ORDERS_2:def_5; then p9 in the carrier of (pcs-total D) by ZFMISC_1:87; hence [p9,q9] in the ToleranceRel of (pcs-total D) by ZFMISC_1:87; :: according to PCS_0:def_7 ::_thesis: verum end; 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 proof set P = pcs-Str(# D,(nabla D),({} (D,D)) #); A1: RelStr(# the carrier of pcs-Str(# D,(nabla D),({} (D,D)) #), the InternalRel of pcs-Str(# D,(nabla D),({} (D,D)) #) #) = RelStr(# the carrier of RelStr(# D,(nabla D) #), the InternalRel of RelStr(# D,(nabla D) #) #) ; hence pcs-Str(# D,(nabla D),({} (D,D)) #) is reflexive by WAYBEL_8:12; :: according to PCS_0:def_24 ::_thesis: ( pcs-Str(# D,(nabla D),({} (D,D)) #) is transitive & pcs-Str(# D,(nabla D),({} (D,D)) #) is pcs-tol-irreflexive & pcs-Str(# D,(nabla D),({} (D,D)) #) is pcs-tol-symmetric & pcs-Str(# D,(nabla D),({} (D,D)) #) is pcs-compatible ) thus pcs-Str(# D,(nabla D),({} (D,D)) #) is transitive by A1, WAYBEL_8:13; ::_thesis: ( pcs-Str(# D,(nabla D),({} (D,D)) #) is pcs-tol-irreflexive & pcs-Str(# D,(nabla D),({} (D,D)) #) is pcs-tol-symmetric & pcs-Str(# D,(nabla D),({} (D,D)) #) is pcs-compatible ) A2: TolStr(# the carrier of pcs-Str(# D,(nabla D),({} (D,D)) #), the ToleranceRel of pcs-Str(# D,(nabla D),({} (D,D)) #) #) = TolStr(# the carrier of TolStr(# D,({} (D,D)) #), the ToleranceRel of TolStr(# D,({} (D,D)) #) #) ; hence pcs-Str(# D,(nabla D),({} (D,D)) #) is pcs-tol-irreflexive by Th4; ::_thesis: ( pcs-Str(# D,(nabla D),({} (D,D)) #) is pcs-tol-symmetric & pcs-Str(# D,(nabla D),({} (D,D)) #) is pcs-compatible ) thus pcs-Str(# D,(nabla D),({} (D,D)) #) is pcs-tol-symmetric by A2, Th5; ::_thesis: pcs-Str(# D,(nabla D),({} (D,D)) #) is pcs-compatible let p be Element of pcs-Str(# D,(nabla D),({} (D,D)) #); :: according to PCS_0:def_22 ::_thesis: for p9, q, q9 being Element of pcs-Str(# D,(nabla D),({} (D,D)) #) st p (--) q & p9 <= p & q9 <= q holds p9 (--) q9 thus for p9, q, q9 being Element of pcs-Str(# D,(nabla D),({} (D,D)) #) st p (--) q & p9 <= p & q9 <= q holds p9 (--) q9 by Def7; ::_thesis: verum end; end; registration cluster non empty strict pcs-like for pcs-Str ; existence ex b1 being pcs-Str st ( b1 is strict & not b1 is empty & b1 is pcs-like ) proof take P = pcs-total {{}}; ::_thesis: ( P is strict & not P is empty & P is pcs-like ) thus P is strict ; ::_thesis: ( not P is empty & P is pcs-like ) thus not the carrier of P is empty ; :: according to STRUCT_0:def_1 ::_thesis: P is pcs-like thus P is pcs-like ; ::_thesis: verum end; cluster non empty strict anti-pcs-like for pcs-Str ; existence ex b1 being pcs-Str st ( b1 is strict & not b1 is empty & b1 is anti-pcs-like ) proof take P = pcs-Str(# {{}},(nabla {{}}),({} ({{}},{{}})) #); ::_thesis: ( P is strict & not P is empty & P is anti-pcs-like ) thus P is strict ; ::_thesis: ( not P is empty & P is anti-pcs-like ) thus not the carrier of P is empty ; :: according to STRUCT_0:def_1 ::_thesis: P is anti-pcs-like thus P is anti-pcs-like ; ::_thesis: verum end; end; definition mode pcs is pcs-like pcs-Str ; mode anti-pcs is anti-pcs-like pcs-Str ; end; definition func pcs-empty -> pcs-Str equals :: PCS_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 & pcs-empty is empty & 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 & not pcs-singleton p is empty & 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 ) proof hereby ::_thesis: ( ( for x being set st x in dom f holds f . x is pcs-Str ) implies f is pcs-Str-yielding ) assume A1: f is pcs-Str-yielding ; ::_thesis: for x being set st x in dom f holds f . x is pcs-Str let x be set ; ::_thesis: ( x in dom f implies f . x is pcs-Str ) assume x in dom f ; ::_thesis: f . x is pcs-Str then f . x in rng f by FUNCT_1:3; hence f . x is pcs-Str by A1, Def28; ::_thesis: verum end; assume A2: for x being set st x in dom f holds f . x is pcs-Str ; ::_thesis: f is pcs-Str-yielding let P be set ; :: according to PCS_0:def_28 ::_thesis: ( P in rng f implies P is pcs-Str ) assume P in rng f ; ::_thesis: P is pcs-Str then ex x being set st ( x in dom f & f . x = P ) by FUNCT_1:def_3; hence P is pcs-Str by A2; ::_thesis: verum end; 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 ) proof hereby ::_thesis: ( ( for x being set st x in dom f holds f . x is pcs ) implies f is pcs-yielding ) assume A3: f is pcs-yielding ; ::_thesis: for x being set st x in dom f holds f . x is pcs let x be set ; ::_thesis: ( x in dom f implies f . x is pcs ) assume x in dom f ; ::_thesis: f . x is pcs then f . x in rng f by FUNCT_1:3; hence f . x is pcs by A3, Def29; ::_thesis: verum end; assume A4: for x being set st x in dom f holds f . x is pcs ; ::_thesis: f is pcs-yielding let P be set ; :: according to PCS_0:def_29 ::_thesis: ( P in rng f implies P is pcs ) assume P in rng f ; ::_thesis: P is pcs then ex x being set st ( x in dom f & f . x = P ) by FUNCT_1:def_3; hence P is pcs by A4; ::_thesis: verum end; 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 & b1 is RelStr-yielding ) proof let f be Relation; ::_thesis: ( f is pcs-Str-yielding implies ( f is TolStr-yielding & f is RelStr-yielding ) ) assume A1: f is pcs-Str-yielding ; ::_thesis: ( f is TolStr-yielding & f is RelStr-yielding ) thus f is TolStr-yielding ::_thesis: f is RelStr-yielding proof let y be set ; :: according to PCS_0:def_13 ::_thesis: ( y in rng f implies y is TolStr ) thus ( y in rng f implies y is TolStr ) by A1, Def28; ::_thesis: verum end; let y be set ; :: according to YELLOW_1:def_3 ::_thesis: ( not y in proj2 f or y is RelStr ) thus ( not y in proj2 f or y is RelStr ) by A1, Def28; ::_thesis: verum end; 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 proof let f be Relation; ::_thesis: ( f is pcs-yielding implies f is pcs-Str-yielding ) assume A2: f is pcs-yielding ; ::_thesis: f is pcs-Str-yielding let y be set ; :: according to PCS_0:def_28 ::_thesis: ( y in rng f implies y is pcs-Str ) thus ( y in rng f implies y is pcs-Str ) by A2, Def29; ::_thesis: verum end; 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 & b1 is transitive-yielding & b1 is pcs-tol-reflexive-yielding & b1 is pcs-tol-symmetric-yielding ) proof let f be Relation; ::_thesis: ( f is pcs-yielding implies ( f is reflexive-yielding & f is transitive-yielding & f is pcs-tol-reflexive-yielding & f is pcs-tol-symmetric-yielding ) ) assume A3: f is pcs-yielding ; ::_thesis: ( f is reflexive-yielding & f is transitive-yielding & f is pcs-tol-reflexive-yielding & f is pcs-tol-symmetric-yielding ) thus f is reflexive-yielding ::_thesis: ( f is transitive-yielding & f is pcs-tol-reflexive-yielding & f is pcs-tol-symmetric-yielding ) proof let y be RelStr ; :: according to WAYBEL_3:def_8 ::_thesis: ( not y in proj2 f or y is reflexive ) thus ( not y in proj2 f or y is reflexive ) by A3, Def29; ::_thesis: verum end; thus f is transitive-yielding ::_thesis: ( f is pcs-tol-reflexive-yielding & f is pcs-tol-symmetric-yielding ) proof let y be RelStr ; :: according to PCS_0:def_4 ::_thesis: ( y in rng f implies y is transitive ) thus ( y in rng f implies y is transitive ) by A3, Def29; ::_thesis: verum end; thus f is pcs-tol-reflexive-yielding ::_thesis: f is pcs-tol-symmetric-yielding proof let y be TolStr ; :: according to PCS_0:def_16 ::_thesis: ( y in rng f implies y is pcs-tol-reflexive ) thus ( y in rng f implies y is pcs-tol-reflexive ) by A3, Def29; ::_thesis: verum end; let y be TolStr ; :: according to PCS_0:def_18 ::_thesis: ( y in rng f implies y is pcs-tol-symmetric ) thus ( y in rng f implies y is pcs-tol-symmetric ) by A3, Def29; ::_thesis: verum end; 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 proof I --> P is () proof let i be set ; :: according to PCS_0:def_33 ::_thesis: ( i in I implies (I --> P) . i is pcs ) thus ( i in I implies (I --> P) . i is pcs ) by FUNCOP_1:7; ::_thesis: verum end; hence for b1 being ManySortedSet of I st b1 = I --> P holds b1 is pcs-yielding ; ::_thesis: verum end; 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 () proof take I --> pcs-empty ; ::_thesis: I --> pcs-empty is () thus I --> pcs-empty is () ; ::_thesis: verum end; 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; 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 & 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 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 & the InternalRel of P c= the InternalRel of Q & 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 & p = p1 & q = q1 & p <= q holds p1 <= q1 proof let P, Q be RelStr ; ::_thesis: 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 let p, q be Element of P; ::_thesis: 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 let p1, q1 be Element of Q; ::_thesis: ( the InternalRel of P c= the InternalRel of Q & p = p1 & q = q1 & p <= q implies p1 <= q1 ) assume that A1: the InternalRel of P c= the InternalRel of Q and A2: p = p1 and A3: q = q1 and A4: [p,q] in the InternalRel of P ; :: according to ORDERS_2:def_5 ::_thesis: p1 <= q1 thus [p1,q1] in the InternalRel of Q by A1, A2, A3, A4; :: according to ORDERS_2:def_5 ::_thesis: verum end; 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 & p = p1 & q = q1 & p (--) q holds p1 (--) q1 proof let P, Q be TolStr ; ::_thesis: 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 let p, q be Element of P; ::_thesis: 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 let p1, q1 be Element of Q; ::_thesis: ( the ToleranceRel of P c= the ToleranceRel of Q & p = p1 & q = q1 & p (--) q implies p1 (--) q1 ) assume that A1: the ToleranceRel of P c= the ToleranceRel of Q and A2: p = p1 and A3: q = q1 and A4: [p,q] in the ToleranceRel of P ; :: according to PCS_0:def_7 ::_thesis: p1 (--) q1 thus [p1,q1] in the ToleranceRel of Q by A1, A2, A3, A4; :: according to PCS_0:def_7 ::_thesis: verum end; Lm2: for P, Q being pcs-Str for p being set st p in the carrier of P & P c= Q holds p is Element of Q proof let P, Q be pcs-Str ; ::_thesis: for p being set st p in the carrier of P & P c= Q holds p is Element of Q let p be set ; ::_thesis: ( p in the carrier of P & P c= Q implies p is Element of Q ) assume A1: p in the carrier of P ; ::_thesis: ( not P c= Q or p is Element of Q ) assume P c= Q ; ::_thesis: p is Element of Q then the carrier of P c= the carrier of Q by Def34; hence p is Element of Q by A1; ::_thesis: verum end; 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 & 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 ; 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 proof set f = I --> P; I --> P is pcs-chain-like proof let R, S be pcs-Str ; :: according to PCS_0:def_35 ::_thesis: ( R in rng (I --> P) & S in rng (I --> P) & not R c= S implies S c= R ) assume that A1: R in rng (I --> P) and A2: S in rng (I --> P) ; ::_thesis: ( R c= S or S c= R ) ( ( P = R & P = S ) or rng (I --> P) = {} ) by A1, A2, TARSKI:def_1; hence ( R c= S or S c= R ) by A1; ::_thesis: verum end; hence for b1 being ManySortedSet of I st b1 = I --> P holds b1 is pcs-chain-like ; ::_thesis: verum end; 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 & b1 is pcs-yielding ) proof set P = the pcs; take 0 --> the pcs ; ::_thesis: ( 0 --> the pcs is pcs-chain-like & 0 --> the pcs is pcs-yielding ) thus ( 0 --> the pcs is pcs-chain-like & 0 --> the pcs is pcs-yielding ) ; ::_thesis: verum end; 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 & b1 is () ) proof set P = the pcs; take I --> the pcs ; ::_thesis: ( I --> the pcs is pcs-chain-like & I --> the pcs is () ) thus ( I --> the pcs is pcs-chain-like & I --> the pcs is () ) ; ::_thesis: verum 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 (Carrier C) & the InternalRel of it = Union (pcs-InternalRels C) & the ToleranceRel of it = Union (pcs-ToleranceRels C) ); existence ex b1 being strict pcs-Str st ( the carrier of b1 = Union (Carrier C) & the InternalRel of b1 = Union (pcs-InternalRels C) & the ToleranceRel of b1 = Union (pcs-ToleranceRels C) ) proof set CA = Carrier C; set IRA = pcs-InternalRels C; set TRA = pcs-ToleranceRels C; set D = Union (Carrier C); set IR = Union (pcs-InternalRels C); set TR = Union (pcs-ToleranceRels C); A1: dom (Carrier C) = I by PARTFUN1:def_2; Union (pcs-InternalRels C) c= [:(Union (Carrier C)),(Union (Carrier C)):] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Union (pcs-InternalRels C) or x in [:(Union (Carrier C)),(Union (Carrier C)):] ) assume x in Union (pcs-InternalRels C) ; ::_thesis: x in [:(Union (Carrier C)),(Union (Carrier C)):] then consider P being set such that A2: x in P and A3: P in rng (pcs-InternalRels C) by TARSKI:def_4; consider i being set such that A4: i in dom (pcs-InternalRels C) and A5: (pcs-InternalRels C) . i = P by A3, FUNCT_1:def_3; consider R being RelStr such that A6: R = C . i and A7: (pcs-InternalRels C) . i = the InternalRel of R by A4, Def5; consider x1, x2 being set such that A8: x = [x1,x2] and A9: x1 in the carrier of R and A10: x2 in the carrier of R by A2, A5, A7, RELSET_1:2; ex S being 1-sorted st ( S = C . i & (Carrier C) . i = the carrier of S ) by A4, PRALG_1:def_13; then A11: the carrier of R in rng (Carrier C) by A1, A4, A6, FUNCT_1:def_3; then A12: x1 in union (rng (Carrier C)) by A9, TARSKI:def_4; x2 in union (rng (Carrier C)) by A10, A11, TARSKI:def_4; hence x in [:(Union (Carrier C)),(Union (Carrier C)):] by A8, A12, ZFMISC_1:87; ::_thesis: verum end; then reconsider IR = Union (pcs-InternalRels C) as Relation of (Union (Carrier C)) ; Union (pcs-ToleranceRels C) c= [:(Union (Carrier C)),(Union (Carrier C)):] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Union (pcs-ToleranceRels C) or x in [:(Union (Carrier C)),(Union (Carrier C)):] ) assume x in Union (pcs-ToleranceRels C) ; ::_thesis: x in [:(Union (Carrier C)),(Union (Carrier C)):] then consider P being set such that A13: x in P and A14: P in rng (pcs-ToleranceRels C) by TARSKI:def_4; consider i being set such that A15: i in dom (pcs-ToleranceRels C) and A16: (pcs-ToleranceRels C) . i = P by A14, FUNCT_1:def_3; consider R being TolStr such that A17: R = C . i and A18: (pcs-ToleranceRels C) . i = the ToleranceRel of R by A15, Def19; consider x1, x2 being set such that A19: x = [x1,x2] and A20: x1 in the carrier of R and A21: x2 in the carrier of R by A13, A16, A18, RELSET_1:2; ex S being 1-sorted st ( S = C . i & (Carrier C) . i = the carrier of S ) by A15, PRALG_1:def_13; then A22: the carrier of R in rng (Carrier C) by A1, A15, A17, FUNCT_1:def_3; then A23: x1 in union (rng (Carrier C)) by A20, TARSKI:def_4; x2 in union (rng (Carrier C)) by A21, A22, TARSKI:def_4; hence x in [:(Union (Carrier C)),(Union (Carrier C)):] by A19, A23, ZFMISC_1:87; ::_thesis: verum end; then reconsider TR = Union (pcs-ToleranceRels C) as Relation of (Union (Carrier C)) ; take pcs-Str(# (Union (Carrier C)),IR,TR #) ; ::_thesis: ( the carrier of pcs-Str(# (Union (Carrier C)),IR,TR #) = Union (Carrier C) & the InternalRel of pcs-Str(# (Union (Carrier C)),IR,TR #) = Union (pcs-InternalRels C) & the ToleranceRel of pcs-Str(# (Union (Carrier C)),IR,TR #) = Union (pcs-ToleranceRels C) ) thus ( the carrier of pcs-Str(# (Union (Carrier C)),IR,TR #) = Union (Carrier C) & the InternalRel of pcs-Str(# (Union (Carrier C)),IR,TR #) = Union (pcs-InternalRels C) & the ToleranceRel of pcs-Str(# (Union (Carrier C)),IR,TR #) = Union (pcs-ToleranceRels C) ) ; ::_thesis: verum end; uniqueness for b1, b2 being strict pcs-Str st the carrier of b1 = Union (Carrier C) & the InternalRel of b1 = Union (pcs-InternalRels C) & the ToleranceRel of b1 = Union (pcs-ToleranceRels C) & the carrier of b2 = Union (Carrier C) & the InternalRel of b2 = Union (pcs-InternalRels C) & 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) & the InternalRel of b3 = Union (pcs-InternalRels C) & 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 & P = C . i & p9 = p & q9 = q & p9 <= q9 ) ) proof let I be set ; ::_thesis: 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 & P = C . i & p9 = p & q9 = q & p9 <= q9 ) ) let C be () ManySortedSet of I; ::_thesis: 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 & P = C . i & p9 = p & q9 = q & p9 <= q9 ) ) set R = pcs-union C; let p, q be Element of (pcs-union C); ::_thesis: ( p <= q iff ex i being set 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 ) ) A1: dom (pcs-InternalRels C) = I by PARTFUN1:def_2; thus ( p <= q implies ex i being set 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 ) ) ::_thesis: ( ex i being set 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 ) implies p <= q ) proof assume p <= q ; ::_thesis: ex i being set 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 ) then [p,q] in the InternalRel of (pcs-union C) by ORDERS_2:def_5; then [p,q] in Union (pcs-InternalRels C) by Def36; then consider Z being set such that A2: [p,q] in Z and A3: Z in rng (pcs-InternalRels C) by TARSKI:def_4; consider i being set such that A4: i in dom (pcs-InternalRels C) and A5: (pcs-InternalRels C) . i = Z by A3, FUNCT_1:def_3; reconsider I1 = I as non empty set by A4; reconsider A1 = C as () ManySortedSet of I1 ; reconsider i1 = i as Element of I1 by A4; reconsider P = A1 . i1 as pcs-Str ; take i ; ::_thesis: 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 ) take P ; ::_thesis: ex p9, q9 being Element of P st ( i in I & P = C . i & p9 = p & q9 = q & p9 <= q9 ) Z = the InternalRel of (A1 . i1) by A5, Def6; then reconsider p9 = p, q9 = q as Element of P by A2, ZFMISC_1:87; take p9 ; ::_thesis: ex q9 being Element of P st ( i in I & P = C . i & p9 = p & q9 = q & p9 <= q9 ) take q9 ; ::_thesis: ( i in I & P = C . i & p9 = p & q9 = q & p9 <= q9 ) thus i in I by A4; ::_thesis: ( P = C . i & p9 = p & q9 = q & p9 <= q9 ) thus ( P = C . i & p9 = p & q9 = q ) ; ::_thesis: p9 <= q9 thus [p9,q9] in the InternalRel of P by A2, A5, Def6; :: according to ORDERS_2:def_5 ::_thesis: verum end; given i being set , P being pcs-Str , p9, q9 being Element of P such that A6: i in I and A7: P = C . i and A8: p9 = p and A9: q9 = q and A10: p9 <= q9 ; ::_thesis: p <= q A11: [p9,q9] in the InternalRel of P by A10, ORDERS_2:def_5; reconsider I1 = I as non empty set by A6; reconsider i1 = i as Element of I1 by A6; reconsider A1 = C as () ManySortedSet of I1 ; (pcs-InternalRels A1) . i1 = the InternalRel of (A1 . i1) by Def6; then the InternalRel of (A1 . i1) in rng (pcs-InternalRels C) by A1, FUNCT_1:3; then [p,q] in Union (pcs-InternalRels C) by A7, A8, A9, A11, TARSKI:def_4; hence [p,q] in the InternalRel of (pcs-union C) by Def36; :: according to ORDERS_2:def_5 ::_thesis: verum end; 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 & q9 = q & p9 <= q9 ) ) proof let I be non empty set ; ::_thesis: 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 & q9 = q & p9 <= q9 ) ) let C be () ManySortedSet of I; ::_thesis: 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 & q9 = q & p9 <= q9 ) ) let p, q be Element of (pcs-union C); ::_thesis: ( p <= q iff ex i being Element of I ex p9, q9 being Element of (C . i) st ( p9 = p & q9 = q & p9 <= q9 ) ) thus ( p <= q implies ex i being Element of I ex p9, q9 being Element of (C . i) st ( p9 = p & q9 = q & p9 <= q9 ) ) ::_thesis: ( ex i being Element of I ex p9, q9 being Element of (C . i) st ( p9 = p & q9 = q & p9 <= q9 ) implies p <= q ) proof assume p <= q ; ::_thesis: ex i being Element of I ex p9, q9 being Element of (C . i) st ( p9 = p & q9 = q & p9 <= q9 ) then ex i being set 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 ) by Th10; hence ex i being Element of I ex p9, q9 being Element of (C . i) st ( p9 = p & q9 = q & p9 <= q9 ) ; ::_thesis: verum end; thus ( ex i being Element of I ex p9, q9 being Element of (C . i) st ( p9 = p & q9 = q & p9 <= q9 ) implies p <= q ) by Th10; ::_thesis: verum end; 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 & P = C . i & p9 = p & q9 = q & p9 (--) q9 ) ) proof let I be set ; ::_thesis: 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 & P = C . i & p9 = p & q9 = q & p9 (--) q9 ) ) let C be () ManySortedSet of I; ::_thesis: 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 & P = C . i & p9 = p & q9 = q & p9 (--) q9 ) ) set R = pcs-union C; let p, q be Element of (pcs-union C); ::_thesis: ( p (--) q iff ex i being set 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 ) ) A1: dom (pcs-ToleranceRels C) = I by PARTFUN1:def_2; thus ( p (--) q implies ex i being set 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 ) ) ::_thesis: ( ex i being set 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 ) implies p (--) q ) proof assume p (--) q ; ::_thesis: ex i being set 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 ) then [p,q] in the ToleranceRel of (pcs-union C) by Def7; then [p,q] in Union (pcs-ToleranceRels C) by Def36; then consider Z being set such that A2: [p,q] in Z and A3: Z in rng (pcs-ToleranceRels C) by TARSKI:def_4; consider i being set such that A4: i in dom (pcs-ToleranceRels C) and A5: (pcs-ToleranceRels C) . i = Z by A3, FUNCT_1:def_3; reconsider I1 = I as non empty set by A4; reconsider A1 = C as () ManySortedSet of I1 ; reconsider i1 = i as Element of I1 by A4; reconsider P = A1 . i1 as pcs-Str ; take i ; ::_thesis: 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 ) take P ; ::_thesis: ex p9, q9 being Element of P st ( i in I & P = C . i & p9 = p & q9 = q & p9 (--) q9 ) Z = the ToleranceRel of (A1 . i1) by A5, Def20; then reconsider p9 = p, q9 = q as Element of P by A2, ZFMISC_1:87; take p9 ; ::_thesis: ex q9 being Element of P st ( i in I & P = C . i & p9 = p & q9 = q & p9 (--) q9 ) take q9 ; ::_thesis: ( i in I & P = C . i & p9 = p & q9 = q & p9 (--) q9 ) thus i in I by A4; ::_thesis: ( P = C . i & p9 = p & q9 = q & p9 (--) q9 ) thus ( P = C . i & p9 = p & q9 = q ) ; ::_thesis: p9 (--) q9 thus [p9,q9] in the ToleranceRel of P by A2, A5, Def20; :: according to PCS_0:def_7 ::_thesis: verum end; given i being set , P being pcs-Str , p9, q9 being Element of P such that A6: i in I and A7: P = C . i and A8: p9 = p and A9: q9 = q and A10: p9 (--) q9 ; ::_thesis: p (--) q A11: [p9,q9] in the ToleranceRel of P by A10, Def7; reconsider I1 = I as non empty set by A6; reconsider i1 = i as Element of I1 by A6; reconsider A1 = C as () ManySortedSet of I1 ; (pcs-ToleranceRels A1) . i1 = the ToleranceRel of (A1 . i1) by Def20; then the ToleranceRel of (A1 . i1) in rng (pcs-ToleranceRels C) by A1, FUNCT_1:3; then [p,q] in Union (pcs-ToleranceRels C) by A7, A8, A9, A11, TARSKI:def_4; hence [p,q] in the ToleranceRel of (pcs-union C) by Def36; :: according to PCS_0:def_7 ::_thesis: verum end; 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 & q9 = q & p9 (--) q9 ) ) proof let I be non empty set ; ::_thesis: 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 & q9 = q & p9 (--) q9 ) ) let C be () ManySortedSet of I; ::_thesis: 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 & q9 = q & p9 (--) q9 ) ) let p, q be Element of (pcs-union C); ::_thesis: ( p (--) q iff ex i being Element of I ex p9, q9 being Element of (C . i) st ( p9 = p & q9 = q & p9 (--) q9 ) ) thus ( p (--) q implies ex i being Element of I ex p9, q9 being Element of (C . i) st ( p9 = p & q9 = q & p9 (--) q9 ) ) ::_thesis: ( ex i being Element of I ex p9, q9 being Element of (C . i) st ( p9 = p & q9 = q & p9 (--) q9 ) implies p (--) q ) proof assume p (--) q ; ::_thesis: ex i being Element of I ex p9, q9 being Element of (C . i) st ( p9 = p & q9 = q & p9 (--) q9 ) then ex i being set 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 ) by Th12; hence ex i being Element of I ex p9, q9 being Element of (C . i) st ( p9 = p & q9 = q & p9 (--) q9 ) ; ::_thesis: verum end; thus ( ex i being Element of I ex p9, q9 being Element of (C . i) st ( p9 = p & q9 = q & p9 (--) q9 ) implies p (--) q ) by Th12; ::_thesis: verum end; 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 proof set P = pcs-union C; set IR = the InternalRel of (pcs-union C); set CP = the carrier of (pcs-union C); set CA = Carrier C; A1: the carrier of (pcs-union C) = Union (Carrier C) by Def36; A2: the InternalRel of (pcs-union C) = Union (pcs-InternalRels C) by Def36; A3: dom (pcs-InternalRels C) = I by PARTFUN1:def_2; let x be set ; :: according to RELAT_2:def_1,ORDERS_2:def_2 ::_thesis: ( not x in the carrier of (pcs-union C) or [^,^] in the InternalRel of (pcs-union C) ) assume x in the carrier of (pcs-union C) ; ::_thesis: [^,^] in the InternalRel of (pcs-union C) then consider P being set such that A4: x in P and A5: P in rng (Carrier C) by A1, TARSKI:def_4; consider i being set such that A6: i in dom (Carrier C) and A7: (Carrier C) . i = P by A5, FUNCT_1:def_3; A8: ex R being 1-sorted st ( R = C . i & (Carrier C) . i = the carrier of R ) by A6, PRALG_1:def_13; reconsider I = I as non empty set by A6; reconsider i = i as Element of I by A6; reconsider C = C as reflexive-yielding () ManySortedSet of I ; A9: (pcs-InternalRels C) . i = the InternalRel of (C . i) by Def6; the InternalRel of (C . i) is_reflexive_in the carrier of (C . i) by ORDERS_2:def_2; then A10: [x,x] in the InternalRel of (C . i) by A4, A7, A8, RELAT_2:def_1; the InternalRel of (C . i) in rng (pcs-InternalRels C) by A3, A9, FUNCT_1:3; hence [^,^] in the InternalRel of (pcs-union C) by A2, A10, TARSKI:def_4; ::_thesis: verum end; 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 proof set P = pcs-union C; set TR = the ToleranceRel of (pcs-union C); set CP = the carrier of (pcs-union C); set CA = Carrier C; A1: the carrier of (pcs-union C) = Union (Carrier C) by Def36; A2: the ToleranceRel of (pcs-union C) = Union (pcs-ToleranceRels C) by Def36; A3: dom (pcs-ToleranceRels C) = I by PARTFUN1:def_2; let x be set ; :: according to RELAT_2:def_1,PCS_0:def_9 ::_thesis: ( not x in the carrier of (pcs-union C) or [^,^] in the ToleranceRel of (pcs-union C) ) assume x in the carrier of (pcs-union C) ; ::_thesis: [^,^] in the ToleranceRel of (pcs-union C) then consider P being set such that A4: x in P and A5: P in rng (Carrier C) by A1, TARSKI:def_4; consider i being set such that A6: i in dom (Carrier C) and A7: (Carrier C) . i = P by A5, FUNCT_1:def_3; A8: ex R being 1-sorted st ( R = C . i & (Carrier C) . i = the carrier of R ) by A6, PRALG_1:def_13; reconsider I = I as non empty set by A6; reconsider i = i as Element of I by A6; reconsider C = C as pcs-tol-reflexive-yielding () ManySortedSet of I ; A9: (pcs-ToleranceRels C) . i = the ToleranceRel of (C . i) by Def20; the ToleranceRel of (C . i) is_reflexive_in the carrier of (C . i) by Def9; then A10: [x,x] in the ToleranceRel of (C . i) by A4, A7, A8, RELAT_2:def_1; the ToleranceRel of (C . i) in rng (pcs-ToleranceRels C) by A3, A9, FUNCT_1:3; hence [^,^] in the ToleranceRel of (pcs-union C) by A2, A10, TARSKI:def_4; ::_thesis: verum end; 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 proof set P = pcs-union C; set TR = the ToleranceRel of (pcs-union C); set CP = the carrier of (pcs-union C); A1: the ToleranceRel of (pcs-union C) = Union (pcs-ToleranceRels C) by Def36; let x, y be set ; :: according to RELAT_2:def_3,PCS_0:def_11 ::_thesis: ( not x in the carrier of (pcs-union C) or not y in the carrier of (pcs-union C) or not [^,^] in the ToleranceRel of (pcs-union C) or [^,^] in the ToleranceRel of (pcs-union C) ) assume that x in the carrier of (pcs-union C) and y in the carrier of (pcs-union C) ; ::_thesis: ( not [^,^] in the ToleranceRel of (pcs-union C) or [^,^] in the ToleranceRel of (pcs-union C) ) assume [x,y] in the ToleranceRel of (pcs-union C) ; ::_thesis: [^,^] in the ToleranceRel of (pcs-union C) then consider P being set such that A2: [x,y] in P and A3: P in rng (pcs-ToleranceRels C) by A1, TARSKI:def_4; consider i being set such that A4: i in dom (pcs-ToleranceRels C) and A5: (pcs-ToleranceRels C) . i = P by A3, FUNCT_1:def_3; reconsider I = I as non empty set by A4; reconsider C = C as pcs-tol-symmetric-yielding () ManySortedSet of I ; reconsider i = i as Element of I by A4; A6: (pcs-ToleranceRels C) . i = the ToleranceRel of (C . i) by Def20; then A7: x in the carrier of (C . i) by A2, A5, ZFMISC_1:87; A8: y in the carrier of (C . i) by A2, A5, A6, ZFMISC_1:87; the ToleranceRel of (C . i) is_symmetric_in the carrier of (C . i) by Def11; then A9: [y,x] in the ToleranceRel of (C . i) by A2, A5, A6, A7, A8, RELAT_2:def_3; the ToleranceRel of (C . i) in rng (pcs-ToleranceRels C) by A4, A6, FUNCT_1:3; hence [^,^] in the ToleranceRel of (pcs-union C) by A1, A9, TARSKI:def_4; ::_thesis: verum end; 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 & pcs-union C is pcs-compatible ) proof set P = pcs-union C; set IR = the InternalRel of (pcs-union C); set TR = the ToleranceRel of (pcs-union C); set CA = the carrier of (pcs-union C); A1: the InternalRel of (pcs-union C) = Union (pcs-InternalRels C) by Def36; A2: the ToleranceRel of (pcs-union C) = Union (pcs-ToleranceRels C) by Def36; A3: dom C = I by PARTFUN1:def_2; thus pcs-union C is transitive ::_thesis: pcs-union C is pcs-compatible proof let x, y, z be set ; :: according to RELAT_2:def_8,ORDERS_2:def_3 ::_thesis: ( not x in the carrier of (pcs-union C) or not y in the carrier of (pcs-union C) or not z in the carrier of (pcs-union C) or not [^,^] in the InternalRel of (pcs-union C) or not [^,^] in the InternalRel of (pcs-union C) or [^,^] in the InternalRel of (pcs-union C) ) assume that x in the carrier of (pcs-union C) and y in the carrier of (pcs-union C) and z in the carrier of (pcs-union C) ; ::_thesis: ( not [^,^] in the InternalRel of (pcs-union C) or not [^,^] in the InternalRel of (pcs-union C) or [^,^] in the InternalRel of (pcs-union C) ) assume [x,y] in the InternalRel of (pcs-union C) ; ::_thesis: ( not [^,^] in the InternalRel of (pcs-union C) or [^,^] in the InternalRel of (pcs-union C) ) then consider Z1 being set such that A4: [x,y] in Z1 and A5: Z1 in rng (pcs-InternalRels C) by A1, TARSKI:def_4; consider i being set such that A6: i in dom (pcs-InternalRels C) and A7: (pcs-InternalRels C) . i = Z1 by A5, FUNCT_1:def_3; assume [y,z] in the InternalRel of (pcs-union C) ; ::_thesis: [^,^] in the InternalRel of (pcs-union C) then consider Z2 being set such that A8: [y,z] in Z2 and A9: Z2 in rng (pcs-InternalRels C) by A1, TARSKI:def_4; consider j being set such that A10: j in dom (pcs-InternalRels C) and A11: (pcs-InternalRels C) . j = Z2 by A9, FUNCT_1:def_3; reconsider I = I as non empty set by A6; reconsider C = C as pcs-Chain of I ; reconsider i = i, j = j as Element of I by A6, A10; A12: (pcs-InternalRels C) . i = the InternalRel of (C . i) by Def6; then A13: x in the carrier of (C . i) by A4, A7, ZFMISC_1:87; A14: y in the carrier of (C . i) by A4, A7, A12, ZFMISC_1:87; A15: (pcs-InternalRels C) . j = the InternalRel of (C . j) by Def6; A16: C . i in rng C by A3, FUNCT_1:3; A17: C . j in rng C by A3, FUNCT_1:3; A18: the InternalRel of (C . i) is_transitive_in the carrier of (C . i) by ORDERS_2:def_3; A19: the InternalRel of (C . j) is_transitive_in the carrier of (C . j) by ORDERS_2:def_3; percases ( C . i c= C . j or C . j c= C . i ) by A16, A17, Def35; suppose C . i c= C . j ; ::_thesis: [^,^] in the InternalRel of (pcs-union C) then A20: the InternalRel of (C . i) c= the InternalRel of (C . j) by Def34; then A21: [x,y] in the InternalRel of (C . j) by A4, A7, A12; then A22: x in the carrier of (C . j) by ZFMISC_1:87; A23: y in the carrier of (C . j) by A21, ZFMISC_1:87; z in the carrier of (C . j) by A8, A11, A15, ZFMISC_1:87; then A24: [x,z] in the InternalRel of (C . j) by A4, A7, A8, A11, A12, A15, A19, A20, A22, A23, RELAT_2:def_8; the InternalRel of (C . j) c= the InternalRel of (pcs-union C) by A1, A9, A11, A15, ZFMISC_1:74; hence [^,^] in the InternalRel of (pcs-union C) by A24; ::_thesis: verum end; suppose C . j c= C . i ; ::_thesis: [^,^] in the InternalRel of (pcs-union C) then A25: the InternalRel of (C . j) c= the InternalRel of (C . i) by Def34; then [y,z] in the InternalRel of (C . i) by A8, A11, A15; then z in the carrier of (C . i) by ZFMISC_1:87; then A26: [x,z] in the InternalRel of (C . i) by A4, A7, A8, A11, A12, A13, A14, A15, A18, A25, RELAT_2:def_8; the InternalRel of (C . i) c= the InternalRel of (pcs-union C) by A1, A5, A7, A12, ZFMISC_1:74; hence [^,^] in the InternalRel of (pcs-union C) by A26; ::_thesis: verum end; end; end; let p, p9, q, q9 be Element of (pcs-union C); :: according to PCS_0:def_22 ::_thesis: ( p (--) q & p9 <= p & q9 <= q implies p9 (--) q9 ) assume that A27: p (--) q and A28: p9 <= p and A29: q9 <= q ; ::_thesis: p9 (--) q9 [p9,p] in the InternalRel of (pcs-union C) by A28, ORDERS_2:def_5; then consider Z1 being set such that A30: [p9,p] in Z1 and A31: Z1 in rng (pcs-InternalRels C) by A1, TARSKI:def_4; consider i being set such that A32: i in dom (pcs-InternalRels C) and A33: (pcs-InternalRels C) . i = Z1 by A31, FUNCT_1:def_3; reconsider I = I as non empty set by A32; reconsider C = C as pcs-Chain of I ; reconsider i = i as Element of I by A32; A34: (pcs-ToleranceRels C) . i = the ToleranceRel of (C . i) by Def20; A35: (pcs-InternalRels C) . i = the InternalRel of (C . i) by Def6; then reconsider pi1 = p, p9i = p9 as Element of (C . i) by A30, A33, ZFMISC_1:87; [q9,q] in the InternalRel of (pcs-union C) by A29, ORDERS_2:def_5; then consider Z2 being set such that A36: [q9,q] in Z2 and A37: Z2 in rng (pcs-InternalRels C) by A1, TARSKI:def_4; consider j being set such that A38: j in dom (pcs-InternalRels C) and A39: (pcs-InternalRels C) . j = Z2 by A37, FUNCT_1:def_3; reconsider j = j as Element of I by A38; A40: (pcs-ToleranceRels C) . j = the ToleranceRel of (C . j) by Def20; A41: (pcs-InternalRels C) . j = the InternalRel of (C . j) by Def6; then A42: q9 in the carrier of (C . j) by A36, A39, ZFMISC_1:87; A43: q in the carrier of (C . j) by A36, A39, A41, ZFMISC_1:87; reconsider qj = q as Element of (C . j) by A36, A39, A41, ZFMISC_1:87; [p,q] in the ToleranceRel of (pcs-union C) by A27, Def7; then consider Z3 being set such that A44: [p,q] in Z3 and A45: Z3 in rng (pcs-ToleranceRels C) by A2, TARSKI:def_4; consider k being set such that A46: k in dom (pcs-ToleranceRels C) and A47: (pcs-ToleranceRels C) . k = Z3 by A45, FUNCT_1:def_3; reconsider k = k as Element of I by A46; A48: (pcs-ToleranceRels C) . k = the ToleranceRel of (C . k) by Def20; then reconsider pk = p, qk = q as Element of (C . k) by A44, A47, ZFMISC_1:87; A49: C . i in rng C by A3, FUNCT_1:3; A50: C . j in rng C by A3, FUNCT_1:3; A51: C . k in rng C by A3, FUNCT_1:3; A52: dom (pcs-ToleranceRels C) = I by PARTFUN1:def_2; then A53: the ToleranceRel of (C . i) c= the ToleranceRel of (pcs-union C) by A2, A34, FUNCT_1:3, ZFMISC_1:74; A54: the ToleranceRel of (C . j) c= the ToleranceRel of (pcs-union C) by A2, A40, A52, FUNCT_1:3, ZFMISC_1:74; A55: the ToleranceRel of (C . k) c= the ToleranceRel of (pcs-union C) by A2, A45, A47, A48, ZFMISC_1:74; percases ( ( C . i c= C . j & C . j c= C . k ) or ( C . j c= C . i & C . i c= C . k ) or ( C . i c= C . k & C . k c= C . j ) or ( C . k c= C . i & C . i c= C . j ) or ( C . k c= C . j & C . j c= C . i ) or ( C . j c= C . k & C . k c= C . i ) ) by A49, A50, A51, Def35; supposethat A56: C . i c= C . j and A57: C . j c= C . k ; ::_thesis: p9 (--) q9 A58: the InternalRel of (C . j) c= the InternalRel of (C . k) by A57, Def34; the InternalRel of (C . i) c= the InternalRel of (C . j) by A56, Def34; then A59: [p9,p] in the InternalRel of (C . j) by A30, A33, A35; then [p9,p] in the InternalRel of (C . k) by A58; then reconsider p9k = p9 as Element of (C . k) by ZFMISC_1:87; [q9,q] in the InternalRel of (C . k) by A36, A39, A41, A58; then reconsider q9k = q9 as Element of (C . k) by ZFMISC_1:87; A60: p9k <= pk by A58, A59, ORDERS_2:def_5; A61: q9k <= qk by A36, A39, A41, A58, ORDERS_2:def_5; pk (--) qk by A44, A47, A48, Def7; then p9k (--) q9k by A60, A61, Def22; then [p9k,q9k] in the ToleranceRel of (C . k) by Def7; hence [p9,q9] in the ToleranceRel of (pcs-union C) by A55; :: according to PCS_0:def_7 ::_thesis: verum end; supposethat A62: C . j c= C . i and A63: C . i c= C . k ; ::_thesis: p9 (--) q9 A64: the InternalRel of (C . i) c= the InternalRel of (C . k) by A63, Def34; A65: the InternalRel of (C . j) c= the InternalRel of (C . i) by A62, Def34; [p9,p] in the InternalRel of (C . k) by A30, A33, A35, A64; then reconsider p9k = p9 as Element of (C . k) by ZFMISC_1:87; A66: [q9,q] in the InternalRel of (C . i) by A36, A39, A41, A65; then [q9,q] in the InternalRel of (C . k) by A64; then reconsider q9k = q9 as Element of (C . k) by ZFMISC_1:87; A67: p9k <= pk by A30, A33, A35, A64, ORDERS_2:def_5; A68: q9k <= qk by A64, A66, ORDERS_2:def_5; pk (--) qk by A44, A47, A48, Def7; then p9k (--) q9k by A67, A68, Def22; then [p9k,q9k] in the ToleranceRel of (C . k) by Def7; hence [p9,q9] in the ToleranceRel of (pcs-union C) by A55; :: according to PCS_0:def_7 ::_thesis: verum end; supposethat A69: C . i c= C . k and A70: C . k c= C . j ; ::_thesis: p9 (--) q9 A71: the InternalRel of (C . k) c= the InternalRel of (C . j) by A70, Def34; A72: the ToleranceRel of (C . k) c= the ToleranceRel of (C . j) by A70, Def34; the InternalRel of (C . i) c= the InternalRel of (C . k) by A69, Def34; then A73: [p9,p] in the InternalRel of (C . k) by A30, A33, A35; then A74: [p9,p] in the InternalRel of (C . j) by A71; then reconsider p9j = p9 as Element of (C . j) by ZFMISC_1:87; reconsider q9j = q9 as Element of (C . j) by A36, A39, A41, ZFMISC_1:87; reconsider pj = p as Element of (C . j) by A74, ZFMISC_1:87; A75: p9j <= pj by A71, A73, ORDERS_2:def_5; A76: q9j <= qj by A36, A39, A41, ORDERS_2:def_5; pj (--) qj by A44, A47, A48, A72, Def7; then p9j (--) q9j by A75, A76, Def22; then [p9j,q9j] in the ToleranceRel of (C . j) by Def7; hence [p9,q9] in the ToleranceRel of (pcs-union C) by A54; :: according to PCS_0:def_7 ::_thesis: verum end; supposethat A77: C . k c= C . i and A78: C . i c= C . j ; ::_thesis: p9 (--) q9 A79: the InternalRel of (C . i) c= the InternalRel of (C . j) by A78, Def34; A80: the ToleranceRel of (C . i) c= the ToleranceRel of (C . j) by A78, Def34; A81: the ToleranceRel of (C . k) c= the ToleranceRel of (C . i) by A77, Def34; A82: [p9,p] in the InternalRel of (C . j) by A30, A33, A35, A79; then reconsider p9j = p9 as Element of (C . j) by ZFMISC_1:87; reconsider q9j = q9 as Element of (C . j) by A36, A39, A41, ZFMISC_1:87; reconsider pj = p as Element of (C . j) by A82, ZFMISC_1:87; q in the carrier of (C . k) by A44, A47, A48, ZFMISC_1:87; then reconsider qi = q as Element of (C . i) by A77, Lm2; A83: p9j <= pj by A30, A33, A35, A79, ORDERS_2:def_5; A84: q9j <= qj by A36, A39, A41, ORDERS_2:def_5; pi1 (--) qi by A44, A47, A48, A81, Def7; then pj (--) qj by A80, Th9; then p9j (--) q9j by A83, A84, Def22; then [p9j,q9j] in the ToleranceRel of (C . j) by Def7; hence [p9,q9] in the ToleranceRel of (pcs-union C) by A54; :: according to PCS_0:def_7 ::_thesis: verum end; supposethat A85: C . k c= C . j and A86: C . j c= C . i ; ::_thesis: p9 (--) q9 A87: the ToleranceRel of (C . j) c= the ToleranceRel of (C . i) by A86, Def34; A88: the ToleranceRel of (C . k) c= the ToleranceRel of (C . j) by A85, Def34; A89: the InternalRel of (C . j) c= the InternalRel of (C . i) by A86, Def34; reconsider q9i = q9 as Element of (C . i) by A42, A86, Lm2; reconsider qi = q as Element of (C . i) by A43, A86, Lm2; p in the carrier of (C . k) by A44, A47, A48, ZFMISC_1:87; then reconsider pj = p as Element of (C . j) by A85, Lm2; A90: p9i <= pi1 by A30, A33, A35, ORDERS_2:def_5; A91: q9i <= qi by A36, A39, A41, A89, ORDERS_2:def_5; pj (--) qj by A44, A47, A48, A88, Def7; then pi1 (--) qi by A87, Th9; then p9i (--) q9i by A90, A91, Def22; then [p9i,q9i] in the ToleranceRel of (C . i) by Def7; hence [p9,q9] in the ToleranceRel of (pcs-union C) by A53; :: according to PCS_0:def_7 ::_thesis: verum end; supposethat A92: C . j c= C . k and A93: C . k c= C . i ; ::_thesis: p9 (--) q9 A94: the ToleranceRel of (C . k) c= the ToleranceRel of (C . i) by A93, Def34; A95: the InternalRel of (C . k) c= the InternalRel of (C . i) by A93, Def34; A96: the InternalRel of (C . j) c= the InternalRel of (C . k) by A92, Def34; reconsider q9k = q9 as Element of (C . k) by A42, A92, Lm2; A97: the carrier of (C . j) c= the carrier of (C . k) by A92, Def34; then reconsider q9i = q9 as Element of (C . i) by A42, A93, Lm2; reconsider qi = q as Element of (C . i) by A43, A93, A97, Lm2; A98: q9k <= qk by A36, A39, A41, A96, ORDERS_2:def_5; A99: p9i <= pi1 by A30, A33, A35, ORDERS_2:def_5; A100: q9i <= qi by A95, A98, Th8; pi1 (--) qi by A44, A47, A48, A94, Def7; then p9i (--) q9i by A99, A100, Def22; then [p9i,q9i] in the ToleranceRel of (C . i) by Def7; hence [p9,q9] in the ToleranceRel of (pcs-union C) by A53; :: according to PCS_0:def_7 ::_thesis: verum end; end; end; end; registration let p, q be set ; cluster<%p,q%> -> {0,1} -defined ; coherence <%p,q%> is {0,1} -defined proof len <%p,q%> = {0,1} by AFINSQ_1:38, CARD_1:50; hence <%p,q%> is {0,1} -defined by RELAT_1:def_18; ::_thesis: verum end; cluster<%p,q%> -> total ; coherence <%p,q%> is total proof len <%p,q%> = {0,1} by AFINSQ_1:38, CARD_1:50; hence <%p,q%> is total by PARTFUN1:def_2; ::_thesis: verum end; end; registration let P, Q be 1-sorted ; cluster<%P,Q%> -> 1-sorted-yielding ; coherence <%P,Q%> is 1-sorted-yielding proof let x be set ; :: according to PRALG_1:def_11 ::_thesis: ( not x in proj1 <%P,Q%> or <%P,Q%> . x is 1-sorted ) assume x in dom <%P,Q%> ; ::_thesis: <%P,Q%> . x is 1-sorted then x in len <%P,Q%> ; then x in 2 by AFINSQ_1:38; then ( x = 0 or x = 1 ) by CARD_1:50, TARSKI:def_2; hence <%P,Q%> . x is 1-sorted by AFINSQ_1:38; ::_thesis: verum end; 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 proof let x be set ; :: according to YELLOW_1:def_3 ::_thesis: ( not x in proj2 <%P,Q%> or x is RelStr ) assume x in rng <%P,Q%> ; ::_thesis: x is RelStr then x in {P,Q} by Lm3; hence x is RelStr by TARSKI:def_2; ::_thesis: verum end; end; registration let P, Q be TolStr ; cluster<%P,Q%> -> () ; coherence <%P,Q%> is TolStr-yielding proof let x be set ; :: according to PCS_0:def_15 ::_thesis: ( x in {0,1} implies <%P,Q%> . x is TolStr ) assume x in {0,1} ; ::_thesis: <%P,Q%> . x is TolStr then ( x = 0 or x = 1 ) by TARSKI:def_2; hence <%P,Q%> . x is TolStr by AFINSQ_1:38; ::_thesis: verum end; end; registration let P, Q be pcs-Str ; cluster<%P,Q%> -> () ; coherence <%P,Q%> is pcs-Str-yielding proof let x be set ; :: according to PCS_0:def_32 ::_thesis: ( x in {0,1} implies <%P,Q%> . x is pcs-Str ) assume x in {0,1} ; ::_thesis: <%P,Q%> . x is pcs-Str then ( x = 0 or x = 1 ) by TARSKI:def_2; hence <%P,Q%> . x is pcs-Str by AFINSQ_1:38; ::_thesis: verum end; end; registration let P, Q be reflexive pcs-Str ; cluster<%P,Q%> -> reflexive-yielding ; coherence <%P,Q%> is reflexive-yielding proof let x be RelStr ; :: according to WAYBEL_3:def_8 ::_thesis: ( not x in proj2 <%P,Q%> or x is reflexive ) assume x in rng <%P,Q%> ; ::_thesis: x is reflexive then x in {P,Q} by Lm3; hence x is reflexive by TARSKI:def_2; ::_thesis: verum end; end; registration let P, Q be transitive pcs-Str ; cluster<%P,Q%> -> transitive-yielding ; coherence <%P,Q%> is transitive-yielding proof let x be RelStr ; :: according to PCS_0:def_4 ::_thesis: ( x in rng <%P,Q%> implies x is transitive ) assume x in rng <%P,Q%> ; ::_thesis: x is transitive then x in {P,Q} by Lm3; hence x is transitive by TARSKI:def_2; ::_thesis: verum end; 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 proof let x be TolStr ; :: according to PCS_0:def_16 ::_thesis: ( x in rng <%P,Q%> implies x is pcs-tol-reflexive ) assume x in rng <%P,Q%> ; ::_thesis: x is pcs-tol-reflexive then x in {P,Q} by Lm3; hence x is pcs-tol-reflexive by TARSKI:def_2; ::_thesis: verum end; 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 proof let x be TolStr ; :: according to PCS_0:def_18 ::_thesis: ( x in rng <%P,Q%> implies x is pcs-tol-symmetric ) assume x in rng <%P,Q%> ; ::_thesis: x is pcs-tol-symmetric then x in {P,Q} by Lm3; hence x is pcs-tol-symmetric by TARSKI:def_2; ::_thesis: verum end; end; registration let P, Q be pcs; cluster<%P,Q%> -> () ; coherence <%P,Q%> is pcs-yielding proof let x be set ; :: according to PCS_0:def_33 ::_thesis: ( x in {0,1} implies <%P,Q%> . x is pcs ) assume x in {0,1} ; ::_thesis: <%P,Q%> . x is pcs then ( x = 0 or x = 1 ) by TARSKI:def_2; hence <%P,Q%> . x is pcs by AFINSQ_1:38; ::_thesis: verum end; 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 & the InternalRel of (pcs-sum (P,Q)) = the InternalRel of P \/ the InternalRel of Q & the ToleranceRel of (pcs-sum (P,Q)) = the ToleranceRel of P \/ the ToleranceRel of Q ) proof let P, Q be pcs-Str ; ::_thesis: ( 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 ) set S = H1(P,Q); set f = <%P,Q%>; A1: dom (Carrier <%P,Q%>) = {0,1} by PARTFUN1:def_2; A2: dom (pcs-InternalRels <%P,Q%>) = {0,1} by PARTFUN1:def_2; A3: dom (pcs-ToleranceRels <%P,Q%>) = {0,1} by PARTFUN1:def_2; A4: <%P,Q%> . 0 = P by AFINSQ_1:38; A5: <%P,Q%> . 1 = Q by AFINSQ_1:38; A6: the carrier of H1(P,Q) = Union (Carrier <%P,Q%>) proof thus the carrier of H1(P,Q) c= Union (Carrier <%P,Q%>) :: according to XBOOLE_0:def_10 ::_thesis: Union (Carrier <%P,Q%>) c= the carrier of H1(P,Q) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of H1(P,Q) or x in Union (Carrier <%P,Q%>) ) assume x in the carrier of H1(P,Q) ; ::_thesis: x in Union (Carrier <%P,Q%>) then A7: ( x in the carrier of P or x in the carrier of Q ) by XBOOLE_0:def_3; A8: (Carrier <%P,Q%>) . z = the carrier of (<%P,Q%> . z) by Def1; A9: (Carrier <%P,Q%>) . j = the carrier of (<%P,Q%> . j) by Def1; A10: the carrier of P in rng (Carrier <%P,Q%>) by A1, A4, A8, FUNCT_1:3; the carrier of Q in rng (Carrier <%P,Q%>) by A1, A5, A9, FUNCT_1:3; hence x in Union (Carrier <%P,Q%>) by A7, A10, TARSKI:def_4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Union (Carrier <%P,Q%>) or x in the carrier of H1(P,Q) ) assume x in Union (Carrier <%P,Q%>) ; ::_thesis: x in the carrier of H1(P,Q) then consider Z being set such that A11: x in Z and A12: Z in rng (Carrier <%P,Q%>) by TARSKI:def_4; consider i being set such that A13: i in dom (Carrier <%P,Q%>) and A14: (Carrier <%P,Q%>) . i = Z by A12, FUNCT_1:def_3; ( i = 0 or i = 1 ) by A13, TARSKI:def_2; then ( Z = the carrier of (<%P,Q%> . z) or Z = the carrier of (<%P,Q%> . j) ) by A14, Def1; hence x in the carrier of H1(P,Q) by A4, A5, A11, XBOOLE_0:def_3; ::_thesis: verum end; A15: the InternalRel of H1(P,Q) = Union (pcs-InternalRels <%P,Q%>) proof thus the InternalRel of H1(P,Q) c= Union (pcs-InternalRels <%P,Q%>) :: according to XBOOLE_0:def_10 ::_thesis: Union (pcs-InternalRels <%P,Q%>) c= the InternalRel of H1(P,Q) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the InternalRel of H1(P,Q) or x in Union (pcs-InternalRels <%P,Q%>) ) assume x in the InternalRel of H1(P,Q) ; ::_thesis: x in Union (pcs-InternalRels <%P,Q%>) then A16: ( x in the InternalRel of P or x in the InternalRel of Q ) by XBOOLE_0:def_3; A17: (pcs-InternalRels <%P,Q%>) . z = the InternalRel of (<%P,Q%> . z) by Def6; A18: (pcs-InternalRels <%P,Q%>) . j = the InternalRel of (<%P,Q%> . j) by Def6; A19: the InternalRel of P in rng (pcs-InternalRels <%P,Q%>) by A2, A4, A17, FUNCT_1:3; the InternalRel of Q in rng (pcs-InternalRels <%P,Q%>) by A2, A5, A18, FUNCT_1:3; hence x in Union (pcs-InternalRels <%P,Q%>) by A16, A19, TARSKI:def_4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Union (pcs-InternalRels <%P,Q%>) or x in the InternalRel of H1(P,Q) ) assume x in Union (pcs-InternalRels <%P,Q%>) ; ::_thesis: x in the InternalRel of H1(P,Q) then consider Z being set such that A20: x in Z and A21: Z in rng (pcs-InternalRels <%P,Q%>) by TARSKI:def_4; consider i being set such that A22: i in dom (pcs-InternalRels <%P,Q%>) and A23: (pcs-InternalRels <%P,Q%>) . i = Z by A21, FUNCT_1:def_3; ( i = 0 or i = 1 ) by A22, TARSKI:def_2; then ( Z = the InternalRel of (<%P,Q%> . z) or Z = the InternalRel of (<%P,Q%> . j) ) by A23, Def6; hence x in the InternalRel of H1(P,Q) by A4, A5, A20, XBOOLE_0:def_3; ::_thesis: verum end; the ToleranceRel of H1(P,Q) = Union (pcs-ToleranceRels <%P,Q%>) proof thus the ToleranceRel of H1(P,Q) c= Union (pcs-ToleranceRels <%P,Q%>) :: according to XBOOLE_0:def_10 ::_thesis: Union (pcs-ToleranceRels <%P,Q%>) c= the ToleranceRel of H1(P,Q) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the ToleranceRel of H1(P,Q) or x in Union (pcs-ToleranceRels <%P,Q%>) ) assume x in the ToleranceRel of H1(P,Q) ; ::_thesis: x in Union (pcs-ToleranceRels <%P,Q%>) then A24: ( x in the ToleranceRel of P or x in the ToleranceRel of Q ) by XBOOLE_0:def_3; A25: (pcs-ToleranceRels <%P,Q%>) . z = the ToleranceRel of (<%P,Q%> . z) by Def20; A26: (pcs-ToleranceRels <%P,Q%>) . j = the ToleranceRel of (<%P,Q%> . j) by Def20; A27: the ToleranceRel of P in rng (pcs-ToleranceRels <%P,Q%>) by A3, A4, A25, FUNCT_1:3; the ToleranceRel of Q in rng (pcs-ToleranceRels <%P,Q%>) by A3, A5, A26, FUNCT_1:3; hence x in Union (pcs-ToleranceRels <%P,Q%>) by A24, A27, TARSKI:def_4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Union (pcs-ToleranceRels <%P,Q%>) or x in the ToleranceRel of H1(P,Q) ) assume x in Union (pcs-ToleranceRels <%P,Q%>) ; ::_thesis: x in the ToleranceRel of H1(P,Q) then consider Z being set such that A28: x in Z and A29: Z in rng (pcs-ToleranceRels <%P,Q%>) by TARSKI:def_4; consider i being set such that A30: i in dom (pcs-ToleranceRels <%P,Q%>) and A31: (pcs-ToleranceRels <%P,Q%>) . i = Z by A29, FUNCT_1:def_3; ( i = 0 or i = 1 ) by A30, TARSKI:def_2; then ( Z = the ToleranceRel of (<%P,Q%> . z) or Z = the ToleranceRel of (<%P,Q%> . j) ) by A31, Def20; hence x in the ToleranceRel of H1(P,Q) by A4, A5, A28, XBOOLE_0:def_3; ::_thesis: verum end; hence ( 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 ) by A6, A15, Def36; ::_thesis: verum 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 let P, Q be pcs-Str ; ::_thesis: 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) #) A1: the carrier of (pcs-sum (P,Q)) = the carrier of P \/ the carrier of Q by Th14; the InternalRel of (pcs-sum (P,Q)) = the InternalRel of P \/ the InternalRel of Q by Th14; hence 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) #) by A1, Th14; ::_thesis: verum 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 let P, Q be pcs-Str ; ::_thesis: 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 ) ) ) set R = pcs-sum (P,Q); let p, q be Element of (pcs-sum (P,Q)); ::_thesis: ( 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 ) ) ) A1: the InternalRel of (pcs-sum (P,Q)) = the InternalRel of P \/ the InternalRel of Q by Th14; thus ( not p <= q or 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 ) ) ::_thesis: ( ( 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 ) ) implies p <= q ) proof assume A2: [p,q] in the InternalRel of (pcs-sum (P,Q)) ; :: according to ORDERS_2:def_5 ::_thesis: ( 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 ) ) percases ( [p,q] in the InternalRel of P or [p,q] in the InternalRel of Q ) by A1, A2, XBOOLE_0:def_3; supposeA3: [p,q] in the InternalRel of P ; ::_thesis: ( 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 ) ) then reconsider p9 = p, q9 = q as Element of P by ZFMISC_1:87; p9 <= q9 by A3, ORDERS_2:def_5; hence ( 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 ) ) ; ::_thesis: verum end; supposeA4: [p,q] in the InternalRel of Q ; ::_thesis: ( 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 ) ) then reconsider p9 = p, q9 = q as Element of Q by ZFMISC_1:87; p9 <= q9 by A4, ORDERS_2:def_5; hence ( 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 ) ) ; ::_thesis: verum end; end; end; assume A5: ( ex p9, q9 being Element of P st ( p9 = p & q9 = q & p9 <= q9 ) or ex p9, q9 being Element of Q st ( p9 = p & q9 = q & p9 <= q9 ) ) ; ::_thesis: p <= q percases ( 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 ) ) by A5; suppose ex p9, q9 being Element of P st ( p9 = p & q9 = q & p9 <= q9 ) ; ::_thesis: p <= q then consider p9, q9 being Element of P such that A6: p9 = p and A7: q9 = q and A8: p9 <= q9 ; [p9,q9] in the InternalRel of P by A8, ORDERS_2:def_5; hence [p,q] in the InternalRel of (pcs-sum (P,Q)) by A1, A6, A7, XBOOLE_0:def_3; :: according to ORDERS_2:def_5 ::_thesis: verum end; suppose ex p9, q9 being Element of Q st ( p9 = p & q9 = q & p9 <= q9 ) ; ::_thesis: p <= q then consider p9, q9 being Element of Q such that A9: p9 = p and A10: q9 = q and A11: p9 <= q9 ; [p9,q9] in the InternalRel of Q by A11, ORDERS_2:def_5; hence [p,q] in the InternalRel of (pcs-sum (P,Q)) by A1, A9, A10, XBOOLE_0:def_3; :: according to ORDERS_2:def_5 ::_thesis: verum end; end; 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 let P, Q be pcs-Str ; ::_thesis: 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 ) ) ) set R = pcs-sum (P,Q); let p, q be Element of (pcs-sum (P,Q)); ::_thesis: ( 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 ) ) ) A1: the ToleranceRel of (pcs-sum (P,Q)) = the ToleranceRel of P \/ the ToleranceRel of Q by Th14; thus ( not p (--) q or 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 ) ) ::_thesis: ( ( 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 ) ) implies p (--) q ) proof assume A2: [p,q] in the ToleranceRel of (pcs-sum (P,Q)) ; :: according to PCS_0:def_7 ::_thesis: ( 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 ) ) percases ( [p,q] in the ToleranceRel of P or [p,q] in the ToleranceRel of Q ) by A1, A2, XBOOLE_0:def_3; supposeA3: [p,q] in the ToleranceRel of P ; ::_thesis: ( 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 ) ) then reconsider p9 = p, q9 = q as Element of P by ZFMISC_1:87; p9 (--) q9 by A3, Def7; hence ( 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 ) ) ; ::_thesis: verum end; supposeA4: [p,q] in the ToleranceRel of Q ; ::_thesis: ( 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 ) ) then reconsider p9 = p, q9 = q as Element of Q by ZFMISC_1:87; p9 (--) q9 by A4, Def7; hence ( 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 ) ) ; ::_thesis: verum end; end; end; assume A5: ( ex p9, q9 being Element of P st ( p9 = p & q9 = q & p9 (--) q9 ) or ex p9, q9 being Element of Q st ( p9 = p & q9 = q & p9 (--) q9 ) ) ; ::_thesis: p (--) q percases ( 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 ) ) by A5; suppose ex p9, q9 being Element of P st ( p9 = p & q9 = q & p9 (--) q9 ) ; ::_thesis: p (--) q then consider p9, q9 being Element of P such that A6: p9 = p and A7: q9 = q and A8: p9 (--) q9 ; [p9,q9] in the ToleranceRel of P by A8, Def7; hence [p,q] in the ToleranceRel of (pcs-sum (P,Q)) by A1, A6, A7, XBOOLE_0:def_3; :: according to PCS_0:def_7 ::_thesis: verum end; suppose ex p9, q9 being Element of Q st ( p9 = p & q9 = q & p9 (--) q9 ) ; ::_thesis: p (--) q then consider p9, q9 being Element of Q such that A9: p9 = p and A10: q9 = q and A11: p9 (--) q9 ; [p9,q9] in the ToleranceRel of Q by A11, Def7; hence [p,q] in the ToleranceRel of (pcs-sum (P,Q)) by A1, A9, A10, XBOOLE_0:def_3; :: according to PCS_0:def_7 ::_thesis: verum end; end; 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 let P, Q be pcs; ::_thesis: ( P misses Q implies the InternalRel of (pcs-sum (P,Q)) is transitive ) assume A1: the carrier of P misses the carrier of Q ; :: according to TSEP_1:def_3 ::_thesis: the InternalRel of (pcs-sum (P,Q)) is transitive pcs-sum (P,Q) = H1(P,Q) by Th15; hence the InternalRel of (pcs-sum (P,Q)) is transitive by A1, Th1; ::_thesis: verum end; theorem Th19: :: PCS_0:19 for P, Q being pcs st P misses Q holds pcs-sum (P,Q) is pcs-compatible proof let P, Q be pcs; ::_thesis: ( P misses Q implies pcs-sum (P,Q) is pcs-compatible ) set D1 = the carrier of P; set D2 = the carrier of Q; set R1 = the InternalRel of P; set R2 = the InternalRel of Q; set T1 = the ToleranceRel of P; set T2 = the ToleranceRel of Q; set R = the InternalRel of P \/ the InternalRel of Q; set T = the ToleranceRel of P \/ the ToleranceRel of Q; assume A1: the carrier of P misses the carrier of Q ; :: according to TSEP_1:def_3 ::_thesis: pcs-sum (P,Q) is pcs-compatible let p, p9, q, q9 be Element of (pcs-sum (P,Q)); :: according to PCS_0:def_22 ::_thesis: ( p (--) q & p9 <= p & q9 <= q implies p9 (--) q9 ) assume that A2: p (--) q and A3: p9 <= p and A4: q9 <= q ; ::_thesis: p9 (--) q9 A5: pcs-sum (P,Q) = H1(P,Q) by Th15; then A6: [p,q] in the ToleranceRel of P \/ the ToleranceRel of Q by A2, Def7; percases ( [p,q] in the ToleranceRel of P or [p,q] in the ToleranceRel of Q ) by A6, XBOOLE_0:def_3; supposeA7: [p,q] in the ToleranceRel of P ; ::_thesis: p9 (--) q9 then A8: p in the carrier of P by ZFMISC_1:87; A9: q in the carrier of P by A7, ZFMISC_1:87; reconsider p1 = p, q1 = q as Element of P by A7, ZFMISC_1:87; A10: p1 (--) q1 by A7, Def7; A11: [p9,p] in the InternalRel of P \/ the InternalRel of Q by A3, A5, ORDERS_2:def_5; A12: [q9,q] in the InternalRel of P \/ the InternalRel of Q by A4, A5, ORDERS_2:def_5; then reconsider p91 = p9, q91 = q9 as Element of P by A1, A8, A9, A11, Lm1; A13: [p9,p] in the InternalRel of P by A1, A8, A11, Lm1; A14: [q9,q] in the InternalRel of P by A1, A9, A12, Lm1; A15: p91 <= p1 by A13, ORDERS_2:def_5; q91 <= q1 by A14, ORDERS_2:def_5; then p91 (--) q91 by A10, A15, Def22; then [p91,q91] in the ToleranceRel of P by Def7; then [p91,q91] in the ToleranceRel of P \/ the ToleranceRel of Q by XBOOLE_0:def_3; hence p9 (--) q9 by A5, Def7; ::_thesis: verum end; supposeA16: [p,q] in the ToleranceRel of Q ; ::_thesis: p9 (--) q9 then A17: p in the carrier of Q by ZFMISC_1:87; A18: q in the carrier of Q by A16, ZFMISC_1:87; reconsider p1 = p, q1 = q as Element of Q by A16, ZFMISC_1:87; A19: p1 (--) q1 by A16, Def7; A20: [p9,p] in the InternalRel of P \/ the InternalRel of Q by A3, A5, ORDERS_2:def_5; A21: [q9,q] in the InternalRel of P \/ the InternalRel of Q by A4, A5, ORDERS_2:def_5; then reconsider p91 = p9, q91 = q9 as Element of Q by A1, A17, A18, A20, Lm1; A22: [p9,p] in the InternalRel of Q by A1, A17, A20, Lm1; A23: [q9,q] in the InternalRel of Q by A1, A18, A21, Lm1; A24: p91 <= p1 by A22, ORDERS_2:def_5; q91 <= q1 by A23, ORDERS_2:def_5; then p91 (--) q91 by A19, A24, Def22; then [p91,q91] in the ToleranceRel of Q by Def7; then [p91,q91] in the ToleranceRel of P \/ the ToleranceRel of Q by XBOOLE_0:def_3; hence p9 (--) q9 by A5, Def7; ::_thesis: verum end; end; end; theorem :: PCS_0:20 for P, Q being pcs st P misses Q holds pcs-sum (P,Q) is pcs proof let P, Q be pcs; ::_thesis: ( P misses Q implies pcs-sum (P,Q) is pcs ) assume A1: P misses Q ; ::_thesis: pcs-sum (P,Q) is pcs set R = pcs-sum (P,Q); A2: field the InternalRel of (pcs-sum (P,Q)) = the carrier of (pcs-sum (P,Q)) by ORDERS_1:12; the InternalRel of (pcs-sum (P,Q)) is transitive by A1, Th18; then the InternalRel of (pcs-sum (P,Q)) is_transitive_in the carrier of (pcs-sum (P,Q)) by A2, RELAT_2:def_16; then A3: pcs-sum (P,Q) is transitive by ORDERS_2:def_3; pcs-sum (P,Q) is pcs-compatible by A1, Th19; hence pcs-sum (P,Q) is pcs by A3; ::_thesis: verum end; 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 & 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 set D = {a} \/ the carrier of P; set IR = [:{a},({a} \/ the carrier of P):] \/ the InternalRel of P; set TR = ([:({a} \/ the carrier of P),{a}:] \/ [:{a},({a} \/ the carrier of P):]) \/ the ToleranceRel of P; A1: {a} c= {a} \/ the carrier of P by XBOOLE_1:7; then A2: [:{a},({a} \/ the carrier of P):] c= [:({a} \/ the carrier of P),({a} \/ the carrier of P):] by ZFMISC_1:95; the carrier of P c= {a} \/ the carrier of P by XBOOLE_1:7; then A3: [: the carrier of P, the carrier of P:] c= [:({a} \/ the carrier of P),({a} \/ the carrier of P):] by ZFMISC_1:96; then the InternalRel of P c= [:({a} \/ the carrier of P),({a} \/ the carrier of P):] by XBOOLE_1:1; then reconsider IR = [:{a},({a} \/ the carrier of P):] \/ the InternalRel of P as Relation of ({a} \/ the carrier of P) by A2, XBOOLE_1:8; [:({a} \/ the carrier of P),{a}:] c= [:({a} \/ the carrier of P),({a} \/ the carrier of P):] by A1, ZFMISC_1:95; then A4: [:({a} \/ the carrier of P),{a}:] \/ [:{a},({a} \/ the carrier of P):] c= [:({a} \/ the carrier of P),({a} \/ the carrier of P):] by A2, XBOOLE_1:8; the ToleranceRel of P c= [:({a} \/ the carrier of P),({a} \/ the carrier of P):] by A3, XBOOLE_1:1; then reconsider TR = ([:({a} \/ the carrier of P),{a}:] \/ [:{a},({a} \/ the carrier of P):]) \/ the ToleranceRel of P as Relation of ({a} \/ the carrier of P) by A4, XBOOLE_1:8; take pcs-Str(# ({a} \/ the carrier of P),IR,TR #) ; ::_thesis: ( the carrier of pcs-Str(# ({a} \/ the carrier of P),IR,TR #) = {a} \/ the carrier of P & the InternalRel of pcs-Str(# ({a} \/ the carrier of P),IR,TR #) = [:{a}, the carrier of pcs-Str(# ({a} \/ the carrier of P),IR,TR #):] \/ the InternalRel of P & the ToleranceRel of pcs-Str(# ({a} \/ the carrier of P),IR,TR #) = ([:{a}, the carrier of pcs-Str(# ({a} \/ the carrier of P),IR,TR #):] \/ [: the carrier of pcs-Str(# ({a} \/ the carrier of P),IR,TR #),{a}:]) \/ the ToleranceRel of P ) thus ( the carrier of pcs-Str(# ({a} \/ the carrier of P),IR,TR #) = {a} \/ the carrier of P & the InternalRel of pcs-Str(# ({a} \/ the carrier of P),IR,TR #) = [:{a}, the carrier of pcs-Str(# ({a} \/ the carrier of P),IR,TR #):] \/ the InternalRel of P & the ToleranceRel of pcs-Str(# ({a} \/ the carrier of P),IR,TR #) = ([:{a}, the carrier of pcs-Str(# ({a} \/ the carrier of P),IR,TR #):] \/ [: the carrier of pcs-Str(# ({a} \/ the carrier of P),IR,TR #),{a}:]) \/ the ToleranceRel of P ) ; ::_thesis: verum 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_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 & 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 the carrier of (pcs-extension (P,a)) = {a} \/ the carrier of P by Def39; hence not the carrier of (pcs-extension (P,a)) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum 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 let P be pcs-Str ; ::_thesis: 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)) ) let a be set ; ::_thesis: ( 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)) ) set R = pcs-extension (P,a); A1: the carrier of (pcs-extension (P,a)) = {a} \/ the carrier of P by Def39; A2: the InternalRel of (pcs-extension (P,a)) = [:{a}, the carrier of (pcs-extension (P,a)):] \/ the InternalRel of P by Def39; the ToleranceRel of (pcs-extension (P,a)) = ([:{a}, the carrier of (pcs-extension (P,a)):] \/ [: the carrier of (pcs-extension (P,a)),{a}:]) \/ the ToleranceRel of P by Def39; hence ( 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)) ) by A1, A2, XBOOLE_1:7; ::_thesis: verum 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 let P be pcs-Str ; ::_thesis: for a being set for p, q being Element of (pcs-extension (P,a)) st p = a holds p <= q let a be set ; ::_thesis: for p, q being Element of (pcs-extension (P,a)) st p = a holds p <= q set R = pcs-extension (P,a); let p, q be Element of (pcs-extension (P,a)); ::_thesis: ( p = a implies p <= q ) assume A1: p = a ; ::_thesis: p <= q A2: the InternalRel of (pcs-extension (P,a)) = [:{a}, the carrier of (pcs-extension (P,a)):] \/ the InternalRel of P by Def39; [a,q] in [:{a}, the carrier of (pcs-extension (P,a)):] by ZFMISC_1:105; hence [p,q] in the InternalRel of (pcs-extension (P,a)) by A1, A2, XBOOLE_0:def_3; :: according to ORDERS_2:def_5 ::_thesis: verum 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 let P be pcs-Str ; ::_thesis: 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 let a be set ; ::_thesis: 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 let p, q be Element of P; ::_thesis: for p1, q1 being Element of (pcs-extension (P,a)) st p = p1 & q = q1 & p <= q holds p1 <= q1 let p1, q1 be Element of (pcs-extension (P,a)); ::_thesis: ( p = p1 & q = q1 & p <= q implies p1 <= q1 ) assume that A1: p = p1 and A2: q = q1 and A3: [p,q] in the InternalRel of P ; :: according to ORDERS_2:def_5 ::_thesis: p1 <= q1 the InternalRel of P c= the InternalRel of (pcs-extension (P,a)) by Th21; hence [p1,q1] in the InternalRel of (pcs-extension (P,a)) by A1, A2, A3; :: according to ORDERS_2:def_5 ::_thesis: verum 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 let P be pcs-Str ; ::_thesis: 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 ) let a be set ; ::_thesis: 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 ) let p be Element of P; ::_thesis: 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 ) let p1, q1 be Element of (pcs-extension (P,a)); ::_thesis: ( p = p1 & p <> a & p1 <= q1 & not a in the carrier of P implies ( q1 in the carrier of P & q1 <> a ) ) assume that A1: p = p1 and A2: p <> a and A3: p1 <= q1 and A4: not a in the carrier of P ; ::_thesis: ( q1 in the carrier of P & q1 <> a ) set R = pcs-extension (P,a); A5: the InternalRel of (pcs-extension (P,a)) = [:{a}, the carrier of (pcs-extension (P,a)):] \/ the InternalRel of P by Def39; [p1,q1] in the InternalRel of (pcs-extension (P,a)) by A3, ORDERS_2:def_5; then ( [p1,q1] in [:{a}, the carrier of (pcs-extension (P,a)):] or [p1,q1] in the InternalRel of P ) by A5, XBOOLE_0:def_3; hence ( q1 in the carrier of P & q1 <> a ) by A1, A2, A4, ZFMISC_1:87, ZFMISC_1:105; ::_thesis: verum 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 let P be pcs-Str ; ::_thesis: for a being set for p being Element of (pcs-extension (P,a)) st p <> a holds p in the carrier of P let a be set ; ::_thesis: for p being Element of (pcs-extension (P,a)) st p <> a holds p in the carrier of P let p be Element of (pcs-extension (P,a)); ::_thesis: ( p <> a implies p in the carrier of P ) assume A1: p <> a ; ::_thesis: p in the carrier of P the carrier of (pcs-extension (P,a)) = {a} \/ the carrier of P by Def39; then ( p in {a} or p in the carrier of P ) by XBOOLE_0:def_3; hence p in the carrier of P by A1, TARSKI:def_1; ::_thesis: verum 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 let P be pcs-Str ; ::_thesis: 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 let a be set ; ::_thesis: 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 let p, q be Element of P; ::_thesis: for p1, q1 being Element of (pcs-extension (P,a)) st p = p1 & q = q1 & p <> a & p1 <= q1 holds p <= q let p1, q1 be Element of (pcs-extension (P,a)); ::_thesis: ( p = p1 & q = q1 & p <> a & p1 <= q1 implies p <= q ) assume that A1: p = p1 and A2: q = q1 and A3: p <> a and A4: p1 <= q1 ; ::_thesis: p <= q set R = pcs-extension (P,a); A5: the InternalRel of (pcs-extension (P,a)) = [:{a}, the carrier of (pcs-extension (P,a)):] \/ the InternalRel of P by Def39; [p1,q1] in the InternalRel of (pcs-extension (P,a)) by A4, ORDERS_2:def_5; then ( [p1,q1] in [:{a}, the carrier of (pcs-extension (P,a)):] or [p1,q1] in the InternalRel of P ) by A5, XBOOLE_0:def_3; hence [p,q] in the InternalRel of P by A1, A2, A3, ZFMISC_1:105; :: according to ORDERS_2:def_5 ::_thesis: verum 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 let P be pcs-Str ; ::_thesis: for a being set for p, q being Element of (pcs-extension (P,a)) st p = a holds ( p (--) q & q (--) p ) let a be set ; ::_thesis: for p, q being Element of (pcs-extension (P,a)) st p = a holds ( p (--) q & q (--) p ) set R = pcs-extension (P,a); let p, q be Element of (pcs-extension (P,a)); ::_thesis: ( p = a implies ( p (--) q & q (--) p ) ) assume A1: p = a ; ::_thesis: ( p (--) q & q (--) p ) the ToleranceRel of (pcs-extension (P,a)) = ([:{a}, the carrier of (pcs-extension (P,a)):] \/ [: the carrier of (pcs-extension (P,a)),{a}:]) \/ the ToleranceRel of P by Def39; then A2: the ToleranceRel of (pcs-extension (P,a)) = [:{a}, the carrier of (pcs-extension (P,a)):] \/ ([: the carrier of (pcs-extension (P,a)),{a}:] \/ the ToleranceRel of P) by XBOOLE_1:4; A3: [a,q] in [:{a}, the carrier of (pcs-extension (P,a)):] by ZFMISC_1:105; [q,a] in [: the carrier of (pcs-extension (P,a)),{a}:] by ZFMISC_1:106; then [q,a] in [: the carrier of (pcs-extension (P,a)),{a}:] \/ the ToleranceRel of P by XBOOLE_0:def_3; hence ( [p,q] in the ToleranceRel of (pcs-extension (P,a)) & [q,p] in the ToleranceRel of (pcs-extension (P,a)) ) by A1, A2, A3, XBOOLE_0:def_3; :: according to PCS_0:def_7 ::_thesis: verum 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 let P be pcs-Str ; ::_thesis: 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 let a be set ; ::_thesis: 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 let p, q be Element of P; ::_thesis: for p1, q1 being Element of (pcs-extension (P,a)) st p = p1 & q = q1 & p (--) q holds p1 (--) q1 let p1, q1 be Element of (pcs-extension (P,a)); ::_thesis: ( p = p1 & q = q1 & p (--) q implies p1 (--) q1 ) assume that A1: p = p1 and A2: q = q1 and A3: [p,q] in the ToleranceRel of P ; :: according to PCS_0:def_7 ::_thesis: p1 (--) q1 the ToleranceRel of P c= the ToleranceRel of (pcs-extension (P,a)) by Th21; hence [p1,q1] in the ToleranceRel of (pcs-extension (P,a)) by A1, A2, A3; :: according to PCS_0:def_7 ::_thesis: verum 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 let P be pcs-Str ; ::_thesis: 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 let a be set ; ::_thesis: 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 let p, q be Element of P; ::_thesis: for p1, q1 being Element of (pcs-extension (P,a)) st p = p1 & q = q1 & p <> a & q <> a & p1 (--) q1 holds p (--) q let p1, q1 be Element of (pcs-extension (P,a)); ::_thesis: ( p = p1 & q = q1 & p <> a & q <> a & p1 (--) q1 implies p (--) q ) assume that A1: p = p1 and A2: q = q1 and A3: p <> a and A4: q <> a and A5: p1 (--) q1 ; ::_thesis: p (--) q set R = pcs-extension (P,a); A6: the ToleranceRel of (pcs-extension (P,a)) = ([:{a}, the carrier of (pcs-extension (P,a)):] \/ [: the carrier of (pcs-extension (P,a)),{a}:]) \/ the ToleranceRel of P by Def39; [p1,q1] in the ToleranceRel of (pcs-extension (P,a)) by A5, Def7; then ( [p1,q1] in [:{a}, the carrier of (pcs-extension (P,a)):] \/ [: the carrier of (pcs-extension (P,a)),{a}:] or [p1,q1] in the ToleranceRel of P ) by A6, XBOOLE_0:def_3; then ( [p1,q1] in [:{a}, the carrier of (pcs-extension (P,a)):] or [p1,q1] in [: the carrier of (pcs-extension (P,a)),{a}:] or [p1,q1] in the ToleranceRel of P ) by XBOOLE_0:def_3; hence [p,q] in the ToleranceRel of P by A1, A2, A3, A4, ZFMISC_1:105, ZFMISC_1:106; :: according to PCS_0:def_7 ::_thesis: verum end; 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 proof set R = pcs-extension (P,a); A1: the carrier of (pcs-extension (P,a)) = {a} \/ the carrier of P by Def39; A2: the InternalRel of (pcs-extension (P,a)) = [:{a}, the carrier of (pcs-extension (P,a)):] \/ the InternalRel of P by Def39; let p be set ; :: according to RELAT_2:def_1,ORDERS_2:def_2 ::_thesis: ( not p in the carrier of (pcs-extension (P,a)) or [^,^] in the InternalRel of (pcs-extension (P,a)) ) assume A3: p in the carrier of (pcs-extension (P,a)) ; ::_thesis: [^,^] in the InternalRel of (pcs-extension (P,a)) percases ( p in {a} or p in the carrier of P ) by A1, A3, XBOOLE_0:def_3; suppose p in {a} ; ::_thesis: [^,^] in the InternalRel of (pcs-extension (P,a)) then p = a by TARSKI:def_1; then [p,p] in [:{a}, the carrier of (pcs-extension (P,a)):] by A3, ZFMISC_1:105; hence [^,^] in the InternalRel of (pcs-extension (P,a)) by A2, XBOOLE_0:def_3; ::_thesis: verum end; supposeA4: p in the carrier of P ; ::_thesis: [^,^] in the InternalRel of (pcs-extension (P,a)) the InternalRel of P is_reflexive_in the carrier of P by ORDERS_2:def_2; then [p,p] in the InternalRel of P by A4, RELAT_2:def_1; hence [^,^] in the InternalRel of (pcs-extension (P,a)) by A2, XBOOLE_0:def_3; ::_thesis: verum end; end; 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 let P be transitive pcs-Str ; ::_thesis: for a being set st not a in the carrier of P holds pcs-extension (P,a) is transitive let a be set ; ::_thesis: ( not a in the carrier of P implies pcs-extension (P,a) is transitive ) assume A1: not a in the carrier of P ; ::_thesis: pcs-extension (P,a) is transitive set R = pcs-extension (P,a); A2: the InternalRel of (pcs-extension (P,a)) = [:{a}, the carrier of (pcs-extension (P,a)):] \/ the InternalRel of P by Def39; let x, y, z be set ; :: according to RELAT_2:def_8,ORDERS_2:def_3 ::_thesis: ( not x in the carrier of (pcs-extension (P,a)) or not y in the carrier of (pcs-extension (P,a)) or not z in the carrier of (pcs-extension (P,a)) or not [^,^] in the InternalRel of (pcs-extension (P,a)) or not [^,^] in the InternalRel of (pcs-extension (P,a)) or [^,^] in the InternalRel of (pcs-extension (P,a)) ) assume that A3: x in the carrier of (pcs-extension (P,a)) and A4: y in the carrier of (pcs-extension (P,a)) and A5: z in the carrier of (pcs-extension (P,a)) and A6: [x,y] in the InternalRel of (pcs-extension (P,a)) and A7: [y,z] in the InternalRel of (pcs-extension (P,a)) ; ::_thesis: [^,^] in the InternalRel of (pcs-extension (P,a)) A8: [a,z] in [:{a}, the carrier of (pcs-extension (P,a)):] by A5, ZFMISC_1:105; reconsider x = x, y = y, z = z as Element of (pcs-extension (P,a)) by A3, A4, A5; A9: x <= y by A6, ORDERS_2:def_5; A10: y <= z by A7, ORDERS_2:def_5; percases ( x = a or x <> a ) ; suppose x = a ; ::_thesis: [^,^] in the InternalRel of (pcs-extension (P,a)) hence [^,^] in the InternalRel of (pcs-extension (P,a)) by A2, A8, XBOOLE_0:def_3; ::_thesis: verum end; supposeA11: x <> a ; ::_thesis: [^,^] in the InternalRel of (pcs-extension (P,a)) then reconsider x0 = x as Element of P by Th25; A12: x0 <> a by A11; then reconsider y0 = y as Element of P by A1, A9, Th24; y0 <> a by A1, A9, A12, Th24; then reconsider z0 = z as Element of P by A1, A10, Th24; A13: y <> a by A1, A9, A12, Th24; A14: x0 <= y0 by A9, A11, Th26; y0 <= z0 by A10, A13, Th26; then x0 <= z0 by A14, YELLOW_0:def_2; then x <= z by Th23; hence [^,^] in the InternalRel of (pcs-extension (P,a)) by ORDERS_2:def_5; ::_thesis: verum end; end; end; 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 proof set R = pcs-extension (P,a); A1: the carrier of (pcs-extension (P,a)) = {a} \/ the carrier of P by Def39; A2: the ToleranceRel of (pcs-extension (P,a)) = ([:{a}, the carrier of (pcs-extension (P,a)):] \/ [: the carrier of (pcs-extension (P,a)),{a}:]) \/ the ToleranceRel of P by Def39; then A3: the ToleranceRel of (pcs-extension (P,a)) = [:{a}, the carrier of (pcs-extension (P,a)):] \/ ([: the carrier of (pcs-extension (P,a)),{a}:] \/ the ToleranceRel of P) by XBOOLE_1:4; let p be set ; :: according to RELAT_2:def_1,PCS_0:def_9 ::_thesis: ( not p in the carrier of (pcs-extension (P,a)) or [^,^] in the ToleranceRel of (pcs-extension (P,a)) ) assume A4: p in the carrier of (pcs-extension (P,a)) ; ::_thesis: [^,^] in the ToleranceRel of (pcs-extension (P,a)) percases ( p in {a} or p in the carrier of P ) by A1, A4, XBOOLE_0:def_3; suppose p in {a} ; ::_thesis: [^,^] in the ToleranceRel of (pcs-extension (P,a)) then p = a by TARSKI:def_1; then [p,p] in [:{a}, the carrier of (pcs-extension (P,a)):] by A4, ZFMISC_1:105; hence [^,^] in the ToleranceRel of (pcs-extension (P,a)) by A3, XBOOLE_0:def_3; ::_thesis: verum end; supposeA5: p in the carrier of P ; ::_thesis: [^,^] in the ToleranceRel of (pcs-extension (P,a)) the ToleranceRel of P is_reflexive_in the carrier of P by Def9; then [p,p] in the ToleranceRel of P by A5, RELAT_2:def_1; hence [^,^] in the ToleranceRel of (pcs-extension (P,a)) by A2, XBOOLE_0:def_3; ::_thesis: verum end; end; end; 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 proof set R = pcs-extension (P,a); A1: the ToleranceRel of (pcs-extension (P,a)) = ([:{a}, the carrier of (pcs-extension (P,a)):] \/ [: the carrier of (pcs-extension (P,a)),{a}:]) \/ the ToleranceRel of P by Def39; let p, q be set ; :: according to RELAT_2:def_3,PCS_0:def_11 ::_thesis: ( not p in the carrier of (pcs-extension (P,a)) or not q in the carrier of (pcs-extension (P,a)) or not [^,^] in the ToleranceRel of (pcs-extension (P,a)) or [^,^] in the ToleranceRel of (pcs-extension (P,a)) ) assume that p in the carrier of (pcs-extension (P,a)) and q in the carrier of (pcs-extension (P,a)) and A2: [p,q] in the ToleranceRel of (pcs-extension (P,a)) ; ::_thesis: [^,^] in the ToleranceRel of (pcs-extension (P,a)) A3: the ToleranceRel of P is_symmetric_in the carrier of P by Def11; percases ( [p,q] in [:{a}, the carrier of (pcs-extension (P,a)):] \/ [: the carrier of (pcs-extension (P,a)),{a}:] or [p,q] in the ToleranceRel of P ) by A1, A2, XBOOLE_0:def_3; supposeA4: [p,q] in [:{a}, the carrier of (pcs-extension (P,a)):] \/ [: the carrier of (pcs-extension (P,a)),{a}:] ; ::_thesis: [^,^] in the ToleranceRel of (pcs-extension (P,a)) percases ( [p,q] in [:{a}, the carrier of (pcs-extension (P,a)):] or [p,q] in [: the carrier of (pcs-extension (P,a)),{a}:] ) by A4, XBOOLE_0:def_3; supposeA5: [p,q] in [:{a}, the carrier of (pcs-extension (P,a)):] ; ::_thesis: [^,^] in the ToleranceRel of (pcs-extension (P,a)) then A6: p = a by ZFMISC_1:105; q in the carrier of (pcs-extension (P,a)) by A5, ZFMISC_1:105; then [q,p] in [: the carrier of (pcs-extension (P,a)),{a}:] by A6, ZFMISC_1:106; then [q,p] in [:{a}, the carrier of (pcs-extension (P,a)):] \/ [: the carrier of (pcs-extension (P,a)),{a}:] by XBOOLE_0:def_3; hence [^,^] in the ToleranceRel of (pcs-extension (P,a)) by A1, XBOOLE_0:def_3; ::_thesis: verum end; supposeA7: [p,q] in [: the carrier of (pcs-extension (P,a)),{a}:] ; ::_thesis: [^,^] in the ToleranceRel of (pcs-extension (P,a)) then A8: q = a by ZFMISC_1:106; p in the carrier of (pcs-extension (P,a)) by A7, ZFMISC_1:106; then [q,p] in [:{a}, the carrier of (pcs-extension (P,a)):] by A8, ZFMISC_1:105; then [q,p] in [:{a}, the carrier of (pcs-extension (P,a)):] \/ [: the carrier of (pcs-extension (P,a)),{a}:] by XBOOLE_0:def_3; hence [^,^] in the ToleranceRel of (pcs-extension (P,a)) by A1, XBOOLE_0:def_3; ::_thesis: verum end; end; end; supposeA9: [p,q] in the ToleranceRel of P ; ::_thesis: [^,^] in the ToleranceRel of (pcs-extension (P,a)) then A10: p in the carrier of P by ZFMISC_1:87; q in the carrier of P by A9, ZFMISC_1:87; then [q,p] in the ToleranceRel of P by A3, A9, A10, RELAT_2:def_3; hence [^,^] in the ToleranceRel of (pcs-extension (P,a)) by A1, XBOOLE_0:def_3; ::_thesis: verum end; end; 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 let P be pcs-compatible pcs-Str ; ::_thesis: for a being set st not a in the carrier of P holds pcs-extension (P,a) is pcs-compatible let a be set ; ::_thesis: ( not a in the carrier of P implies pcs-extension (P,a) is pcs-compatible ) assume A1: not a in the carrier of P ; ::_thesis: pcs-extension (P,a) is pcs-compatible set R = pcs-extension (P,a); let p, p9, q, q9 be Element of (pcs-extension (P,a)); :: according to PCS_0:def_22 ::_thesis: ( p (--) q & p9 <= p & q9 <= q implies p9 (--) q9 ) assume that A2: p (--) q and A3: p9 <= p and A4: q9 <= q ; ::_thesis: p9 (--) q9 percases ( p9 = a or q9 = a or ( p9 <> a & q9 <> a ) ) ; suppose ( p9 = a or q9 = a ) ; ::_thesis: p9 (--) q9 hence p9 (--) q9 by Th27; ::_thesis: verum end; supposethat A5: p9 <> a and A6: q9 <> a ; ::_thesis: p9 (--) q9 reconsider p90 = p9, q90 = q9 as Element of P by A5, A6, Th25; A7: p90 <> a by A5; A8: q90 <> a by A6; A9: p <> a by A1, A3, A7, Th24; A10: q <> a by A1, A4, A8, Th24; reconsider p0 = p, q0 = q as Element of P by A1, A3, A4, A7, A8, Th24; A11: p0 (--) q0 by A2, A9, A10, Th29; A12: p90 <= p0 by A3, A5, Th26; q90 <= q0 by A4, A6, Th26; then p90 (--) q90 by A11, A12, Def22; hence p9 (--) q9 by Th28; ::_thesis: verum end; end; 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 let P be pcs; ::_thesis: for a being set st not a in the carrier of P holds pcs-extension (P,a) is pcs let a be set ; ::_thesis: ( not a in the carrier of P implies pcs-extension (P,a) is pcs ) assume A1: not a in the carrier of P ; ::_thesis: pcs-extension (P,a) is pcs set R = pcs-extension (P,a); ( pcs-extension (P,a) is reflexive & pcs-extension (P,a) is transitive & pcs-extension (P,a) is pcs-tol-reflexive & pcs-extension (P,a) is pcs-tol-symmetric & pcs-extension (P,a) is pcs-compatible ) by A1, Th30, Th31; hence pcs-extension (P,a) is pcs ; ::_thesis: verum end; 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 & 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 reconsider TR = the ToleranceRel of P ` as Relation of the carrier of P ; take pcs-Str(# the carrier of P,( the InternalRel of P ~),TR #) ; ::_thesis: ( the carrier of pcs-Str(# the carrier of P,( the InternalRel of P ~),TR #) = the carrier of P & the InternalRel of pcs-Str(# the carrier of P,( the InternalRel of P ~),TR #) = the InternalRel of P ~ & the ToleranceRel of pcs-Str(# the carrier of P,( the InternalRel of P ~),TR #) = the ToleranceRel of P ` ) thus ( the carrier of pcs-Str(# the carrier of P,( the InternalRel of P ~),TR #) = the carrier of P & the InternalRel of pcs-Str(# the carrier of P,( the InternalRel of P ~),TR #) = the InternalRel of P ~ & the ToleranceRel of pcs-Str(# the carrier of P,( the InternalRel of P ~),TR #) = the ToleranceRel of P ` ) ; ::_thesis: verum 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_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 & the InternalRel of b2 = the InternalRel of P ~ & 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 proof the carrier of (pcs-reverse P) = the carrier of P by Def40; hence not the carrier of (pcs-reverse P) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum 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 (pcs-reverse P) st p = p9 & q = q9 holds ( p <= q iff q9 <= p9 ) proof let P be pcs-Str ; ::_thesis: for p, q being Element of P for p9, q9 being Element of (pcs-reverse P) st p = p9 & q = q9 holds ( p <= q iff q9 <= p9 ) let p, q be Element of P; ::_thesis: for p9, q9 being Element of (pcs-reverse P) st p = p9 & q = q9 holds ( p <= q iff q9 <= p9 ) set R = pcs-reverse P; let p9, q9 be Element of (pcs-reverse P); ::_thesis: ( p = p9 & q = q9 implies ( p <= q iff q9 <= p9 ) ) assume that A1: p = p9 and A2: q = q9 ; ::_thesis: ( p <= q iff q9 <= p9 ) A3: the InternalRel of (pcs-reverse P) = the InternalRel of P ~ by Def40; thus ( p <= q implies q9 <= p9 ) ::_thesis: ( q9 <= p9 implies p <= q ) proof assume [p,q] in the InternalRel of P ; :: according to ORDERS_2:def_5 ::_thesis: q9 <= p9 hence [q9,p9] in the InternalRel of (pcs-reverse P) by A1, A2, A3, RELAT_1:def_7; :: according to ORDERS_2:def_5 ::_thesis: verum end; assume [q9,p9] in the InternalRel of (pcs-reverse P) ; :: according to ORDERS_2:def_5 ::_thesis: p <= q hence [p,q] in the InternalRel of P by A1, A2, A3, RELAT_1:def_7; :: according to ORDERS_2:def_5 ::_thesis: verum end; 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 & q = q9 & p (--) q holds not p9 (--) q9 proof let P be pcs-Str ; ::_thesis: for p, q being Element of P for p9, q9 being Element of (pcs-reverse P) st p = p9 & q = q9 & p (--) q holds not p9 (--) q9 let p, q be Element of P; ::_thesis: for p9, q9 being Element of (pcs-reverse P) st p = p9 & q = q9 & p (--) q holds not p9 (--) q9 set R = pcs-reverse P; let p9, q9 be Element of (pcs-reverse P); ::_thesis: ( p = p9 & q = q9 & p (--) q implies not p9 (--) q9 ) assume that A1: p = p9 and A2: q = q9 ; ::_thesis: ( not p (--) q or not p9 (--) q9 ) A3: the ToleranceRel of (pcs-reverse P) = the ToleranceRel of P ` by Def40; assume [p,q] in the ToleranceRel of P ; :: according to PCS_0:def_7 ::_thesis: not p9 (--) q9 hence not [p9,q9] in the ToleranceRel of (pcs-reverse P) by A1, A2, A3, XBOOLE_0:def_5; :: according to PCS_0:def_7 ::_thesis: verum 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 (pcs-reverse P) st p = p9 & q = q9 & not p9 (--) q9 holds p (--) q proof let P be non empty pcs-Str ; ::_thesis: for p, q being Element of P for p9, q9 being Element of (pcs-reverse P) st p = p9 & q = q9 & not p9 (--) q9 holds p (--) q let p, q be Element of P; ::_thesis: for p9, q9 being Element of (pcs-reverse P) st p = p9 & q = q9 & not p9 (--) q9 holds p (--) q set R = pcs-reverse P; let p9, q9 be Element of (pcs-reverse P); ::_thesis: ( p = p9 & q = q9 & not p9 (--) q9 implies p (--) q ) assume that A1: p = p9 and A2: q = q9 ; ::_thesis: ( p9 (--) q9 or p (--) q ) A3: the ToleranceRel of (pcs-reverse P) = the ToleranceRel of P ` by Def40; assume A4: not [p9,q9] in the ToleranceRel of (pcs-reverse P) ; :: according to PCS_0:def_7 ::_thesis: p (--) q [p,q] in [: the carrier of P, the carrier of P:] by ZFMISC_1:87; hence [p,q] in the ToleranceRel of P by A1, A2, A3, A4, XBOOLE_0:def_5; :: according to PCS_0:def_7 ::_thesis: verum end; registration let P be reflexive pcs-Str ; cluster pcs-reverse P -> reflexive strict ; coherence pcs-reverse P is reflexive proof set R = pcs-reverse P; A1: the carrier of (pcs-reverse P) = the carrier of P by Def40; A2: the InternalRel of (pcs-reverse P) = the InternalRel of P ~ by Def40; the InternalRel of P is_reflexive_in the carrier of P by ORDERS_2:def_2; hence the InternalRel of (pcs-reverse P) is_reflexive_in the carrier of (pcs-reverse P) by A1, A2, ORDERS_1:79; :: according to ORDERS_2:def_2 ::_thesis: verum end; end; registration let P be transitive pcs-Str ; cluster pcs-reverse P -> transitive strict ; coherence pcs-reverse P is transitive proof set R = pcs-reverse P; A1: the carrier of (pcs-reverse P) = the carrier of P by Def40; A2: the InternalRel of (pcs-reverse P) = the InternalRel of P ~ by Def40; the InternalRel of P is_transitive_in the carrier of P by ORDERS_2:def_3; hence the InternalRel of (pcs-reverse P) is_transitive_in the carrier of (pcs-reverse P) by A1, A2, ORDERS_1:80; :: according to ORDERS_2:def_3 ::_thesis: verum end; 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 proof set R = pcs-reverse P; A1: the carrier of (pcs-reverse P) = the carrier of P by Def40; A2: the ToleranceRel of (pcs-reverse P) = the ToleranceRel of P ` by Def40; A3: the ToleranceRel of P is_reflexive_in the carrier of P by Def9; let x be set ; :: according to RELAT_2:def_2,PCS_0:def_10 ::_thesis: ( not x in the carrier of (pcs-reverse P) or not [^,^] in the ToleranceRel of (pcs-reverse P) ) assume x in the carrier of (pcs-reverse P) ; ::_thesis: not [^,^] in the ToleranceRel of (pcs-reverse P) then [x,x] in the ToleranceRel of P by A1, A3, RELAT_2:def_1; hence not [^,^] in the ToleranceRel of (pcs-reverse P) by A2, XBOOLE_0:def_5; ::_thesis: verum end; 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 proof set R = pcs-reverse P; A1: the carrier of (pcs-reverse P) = the carrier of P by Def40; A2: the ToleranceRel of (pcs-reverse P) = the ToleranceRel of P ` by Def40; A3: the ToleranceRel of P is_irreflexive_in the carrier of P by Def10; let x be set ; :: according to RELAT_2:def_1,PCS_0:def_9 ::_thesis: ( not x in the carrier of (pcs-reverse P) or [^,^] in the ToleranceRel of (pcs-reverse P) ) assume A4: x in the carrier of (pcs-reverse P) ; ::_thesis: [^,^] in the ToleranceRel of (pcs-reverse P) then A5: not [x,x] in the ToleranceRel of P by A1, A3, RELAT_2:def_2; [x,x] in [: the carrier of (pcs-reverse P), the carrier of (pcs-reverse P):] by A4, ZFMISC_1:87; hence [^,^] in the ToleranceRel of (pcs-reverse P) by A1, A2, A5, XBOOLE_0:def_5; ::_thesis: verum end; 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 proof set R = pcs-reverse P; A1: the carrier of (pcs-reverse P) = the carrier of P by Def40; A2: the ToleranceRel of (pcs-reverse P) = the ToleranceRel of P ` by Def40; A3: the ToleranceRel of P is_symmetric_in the carrier of P by Def11; let x, y be set ; :: according to RELAT_2:def_3,PCS_0:def_11 ::_thesis: ( not x in the carrier of (pcs-reverse P) or not y in the carrier of (pcs-reverse P) or not [^,^] in the ToleranceRel of (pcs-reverse P) or [^,^] in the ToleranceRel of (pcs-reverse P) ) assume that A4: x in the carrier of (pcs-reverse P) and A5: y in the carrier of (pcs-reverse P) ; ::_thesis: ( not [^,^] in the ToleranceRel of (pcs-reverse P) or [^,^] in the ToleranceRel of (pcs-reverse P) ) assume [x,y] in the ToleranceRel of (pcs-reverse P) ; ::_thesis: [^,^] in the ToleranceRel of (pcs-reverse P) then not [x,y] in the ToleranceRel of P by A2, XBOOLE_0:def_5; then A6: not [y,x] in the ToleranceRel of P by A1, A3, A4, A5, RELAT_2:def_3; [y,x] in [: the carrier of P, the carrier of P:] by A1, A4, A5, ZFMISC_1:87; hence [^,^] in the ToleranceRel of (pcs-reverse P) by A2, A6, XBOOLE_0:def_5; ::_thesis: verum end; end; registration let P be pcs-compatible pcs-Str ; cluster pcs-reverse P -> strict pcs-compatible ; coherence pcs-reverse P is pcs-compatible proof set R = pcs-reverse P; A1: the carrier of (pcs-reverse P) = the carrier of P by Def40; A2: the InternalRel of (pcs-reverse P) = the InternalRel of P ~ by Def40; A3: the ToleranceRel of (pcs-reverse P) = the ToleranceRel of P ` by Def40; let p, p9, q, q9 be Element of (pcs-reverse P); :: according to PCS_0:def_22 ::_thesis: ( p (--) q & p9 <= p & q9 <= q implies p9 (--) q9 ) assume that A4: [p,q] in the ToleranceRel of (pcs-reverse P) and A5: [p9,p] in the InternalRel of (pcs-reverse P) and A6: [q9,q] in the InternalRel of (pcs-reverse P) ; :: according to ORDERS_2:def_5,PCS_0:def_7 ::_thesis: p9 (--) q9 A7: p9 in the carrier of (pcs-reverse P) by A5, ZFMISC_1:87; reconsider p90 = p9, q90 = q9, p0 = p, q0 = q as Element of P by Def40; not [p0,q0] in the ToleranceRel of P by A3, A4, XBOOLE_0:def_5; then A8: not p0 (--) q0 by Def7; A9: [p0,p90] in the InternalRel of P by A2, A5, RELAT_1:def_7; A10: [q0,q90] in the InternalRel of P by A2, A6, RELAT_1:def_7; A11: p0 <= p90 by A9, ORDERS_2:def_5; q0 <= q90 by A10, ORDERS_2:def_5; then not p90 (--) q90 by A8, A11, Def22; then A12: not [p90,q90] in the ToleranceRel of P by Def7; [p9,q9] in [: the carrier of P, the carrier of P:] by A1, A7, ZFMISC_1:87; hence [p9,q9] in the ToleranceRel of (pcs-reverse P) by A3, A12, XBOOLE_0:def_5; :: according to PCS_0:def_7 ::_thesis: verum end; end; 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] & q = [p2,q2] holds ( p <= q iff ( p1 <= p2 & q1 <= q2 ) ) proof let P, Q be pcs-Str ; ::_thesis: 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] & q = [p2,q2] holds ( p <= q iff ( p1 <= p2 & q1 <= q2 ) ) let p, q be Element of (P pcs-times Q); ::_thesis: 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 ) ) let p1, p2 be Element of P; ::_thesis: for q1, q2 being Element of Q st p = [p1,q1] & q = [p2,q2] holds ( p <= q iff ( p1 <= p2 & q1 <= q2 ) ) let q1, q2 be Element of Q; ::_thesis: ( p = [p1,q1] & q = [p2,q2] implies ( p <= q iff ( p1 <= p2 & q1 <= q2 ) ) ) assume that A1: p = [p1,q1] and A2: q = [p2,q2] ; ::_thesis: ( p <= q iff ( p1 <= p2 & q1 <= q2 ) ) thus ( p <= q implies ( p1 <= p2 & q1 <= q2 ) ) ::_thesis: ( p1 <= p2 & q1 <= q2 implies p <= q ) proof assume p <= q ; ::_thesis: ( p1 <= p2 & q1 <= q2 ) then [p,q] in [" the InternalRel of P, the InternalRel of Q"] by ORDERS_2:def_5; then consider a, b, s, t being set such that A3: p = [a,b] and A4: q = [s,t] and A5: [a,s] in the InternalRel of P and A6: [b,t] in the InternalRel of Q by YELLOW_3:def_1; A7: a = p1 by A1, A3, XTUPLE_0:1; A8: b = q1 by A1, A3, XTUPLE_0:1; thus [p1,p2] in the InternalRel of P by A2, A4, A5, A7, XTUPLE_0:1; :: according to ORDERS_2:def_5 ::_thesis: q1 <= q2 thus [q1,q2] in the InternalRel of Q by A2, A4, A6, A8, XTUPLE_0:1; :: according to ORDERS_2:def_5 ::_thesis: verum end; assume that A9: p1 <= p2 and A10: q1 <= q2 ; ::_thesis: p <= q A11: [p1,p2] in the InternalRel of P by A9, ORDERS_2:def_5; [q1,q2] in the InternalRel of Q by A10, ORDERS_2:def_5; hence [p,q] in the InternalRel of (P pcs-times Q) by A1, A2, A11, YELLOW_3:def_1; :: according to ORDERS_2:def_5 ::_thesis: verum end; 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] & q = [p2,q2] & p (--) q & not p1 (--) p2 holds q1 (--) q2 proof let P, Q be pcs-Str ; ::_thesis: 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] & q = [p2,q2] & p (--) q & not p1 (--) p2 holds q1 (--) q2 let p, q be Element of (P pcs-times Q); ::_thesis: 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 let p1, p2 be Element of P; ::_thesis: for q1, q2 being Element of Q st p = [p1,q1] & q = [p2,q2] & p (--) q & not p1 (--) p2 holds q1 (--) q2 let q1, q2 be Element of Q; ::_thesis: ( p = [p1,q1] & q = [p2,q2] & p (--) q & not p1 (--) p2 implies q1 (--) q2 ) assume that A1: p = [p1,q1] and A2: q = [p2,q2] ; ::_thesis: ( not p (--) q or p1 (--) p2 or q1 (--) q2 ) assume p (--) q ; ::_thesis: ( p1 (--) p2 or q1 (--) q2 ) then [p,q] in [^ the ToleranceRel of P, the ToleranceRel of Q^] by Def7; then consider a, b, c, d being set such that A3: p = [a,b] and A4: q = [c,d] and a in the carrier of P and b in the carrier of Q and c in the carrier of P and d in the carrier of Q and A5: ( [a,c] in the ToleranceRel of P or [b,d] in the ToleranceRel of Q ) by Def2; A6: a = p1 by A1, A3, XTUPLE_0:1; A7: b = q1 by A1, A3, XTUPLE_0:1; A8: c = p2 by A2, A4, XTUPLE_0:1; d = q2 by A2, A4, XTUPLE_0:1; hence ( p1 (--) p2 or q1 (--) q2 ) by A5, A6, A7, A8, Def7; ::_thesis: verum end; 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] & q = [p2,q2] & ( p1 (--) p2 or q1 (--) q2 ) holds p (--) q proof let P, Q be non empty pcs-Str ; ::_thesis: 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] & q = [p2,q2] & ( p1 (--) p2 or q1 (--) q2 ) holds p (--) q let p, q be Element of (P pcs-times Q); ::_thesis: 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 let p1, p2 be Element of P; ::_thesis: for q1, q2 being Element of Q st p = [p1,q1] & q = [p2,q2] & ( p1 (--) p2 or q1 (--) q2 ) holds p (--) q let q1, q2 be Element of Q; ::_thesis: ( p = [p1,q1] & q = [p2,q2] & ( p1 (--) p2 or q1 (--) q2 ) implies p (--) q ) assume that A1: p = [p1,q1] and A2: q = [p2,q2] ; ::_thesis: ( ( not p1 (--) p2 & not q1 (--) q2 ) or p (--) q ) assume ( p1 (--) p2 or q1 (--) q2 ) ; ::_thesis: p (--) q then ( [p1,p2] in the ToleranceRel of P or [q1,q2] in the ToleranceRel of Q ) by Def7; hence [p,q] in the ToleranceRel of (P pcs-times Q) by A1, A2, Def2; :: according to PCS_0:def_7 ::_thesis: verum end; registration let P, Q be reflexive pcs-Str ; clusterP pcs-times Q -> reflexive ; coherence P pcs-times Q is reflexive proof RelStr(# the carrier of (P pcs-times Q), the InternalRel of (P pcs-times Q) #) = [:P,Q:] by YELLOW_3:def_2; hence P pcs-times Q is reflexive by WAYBEL_8:12; ::_thesis: verum end; end; registration let P, Q be transitive pcs-Str ; clusterP pcs-times Q -> transitive ; coherence P pcs-times Q is transitive proof RelStr(# the carrier of (P pcs-times Q), the InternalRel of (P pcs-times Q) #) = [:P,Q:] by YELLOW_3:def_2; hence P pcs-times Q is transitive by WAYBEL_8:13; ::_thesis: verum end; 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 proof TolStr(# the carrier of (P pcs-times Q), the ToleranceRel of (P pcs-times Q) #) = [^P,Q^] ; hence P pcs-times Q is pcs-tol-reflexive by Th3; ::_thesis: verum end; 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 proof TolStr(# the carrier of (P pcs-times Q), the ToleranceRel of (P pcs-times Q) #) = [^P,Q^] ; hence P pcs-times Q is pcs-tol-reflexive by Th3; ::_thesis: verum end; 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 proof TolStr(# the carrier of (P pcs-times Q), the ToleranceRel of (P pcs-times Q) #) = [^P,Q^] ; hence P pcs-times Q is pcs-tol-symmetric by Th5; ::_thesis: verum end; end; registration let P, Q be pcs-compatible pcs-Str ; clusterP pcs-times Q -> pcs-compatible ; coherence P pcs-times Q is pcs-compatible proof set R = P pcs-times Q; set TR = the ToleranceRel of (P pcs-times Q); set D1 = the carrier of P; set D2 = the carrier of Q; let p, p9, q, q9 be Element of (P pcs-times Q); :: according to PCS_0:def_22 ::_thesis: ( p (--) q & p9 <= p & q9 <= q implies p9 (--) q9 ) assume that A1: p (--) q and A2: p9 <= p and A3: q9 <= q ; ::_thesis: p9 (--) q9 A4: [p,q] in the ToleranceRel of (P pcs-times Q) by A1, Def7; then consider a, b, c, d being set such that A5: p = [a,b] and A6: q = [c,d] and A7: a in the carrier of P and A8: b in the carrier of Q and A9: c in the carrier of P and A10: d in the carrier of Q and ( [a,c] in the ToleranceRel of P or [b,d] in the ToleranceRel of Q ) by Def2; A11: [p9,p] in the InternalRel of (P pcs-times Q) by A2, ORDERS_2:def_5; then p9 in the carrier of (P pcs-times Q) by ZFMISC_1:87; then consider e, f being set such that A12: e in the carrier of P and A13: f in the carrier of Q and A14: p9 = [e,f] by ZFMISC_1:def_2; A15: [q9,q] in the InternalRel of (P pcs-times Q) by A3, ORDERS_2:def_5; then q9 in the carrier of (P pcs-times Q) by ZFMISC_1:87; then consider g, h being set such that A16: g in the carrier of P and A17: h in the carrier of Q and A18: q9 = [g,h] by ZFMISC_1:def_2; reconsider P = P, Q = Q as non empty pcs-compatible pcs-Str by A7, A8; reconsider a = a, c = c, e = e, g = g as Element of P by A7, A9, A12, A16; reconsider b = b, d = d, f = f, h = h as Element of Q by A8, A10, A13, A17; [^a,b^] (--) [^c,d^] by A4, A5, A6, Def7; then A19: ( a (--) c or b (--) d ) by Th6; A20: RelStr(# the carrier of (P pcs-times Q), the InternalRel of (P pcs-times Q) #) = [:P,Q:] by YELLOW_3:def_2; then A21: [e,f] <= [a,b] by A5, A11, A14, ORDERS_2:def_5; then A22: e <= a by YELLOW_3:11; A23: f <= b by A21, YELLOW_3:11; A24: [g,h] <= [c,d] by A6, A15, A18, A20, ORDERS_2:def_5; then A25: g <= c by YELLOW_3:11; h <= d by A24, YELLOW_3:11; then ( e (--) g or f (--) h ) by A19, A22, A23, A25, Def22; then A26: ( [e,g] in the ToleranceRel of P or [f,h] in the ToleranceRel of Q ) by Def7; A27: p9 = [e,f] by A14; q9 = [g,h] by A18; hence [p9,q9] in the ToleranceRel of (P pcs-times Q) by A26, A27, Def3; :: according to PCS_0:def_7 ::_thesis: verum end; 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] & q = [p2,q2] holds ( p <= q iff ( p2 <= p1 & q1 <= q2 ) ) proof let P, Q be pcs-Str ; ::_thesis: 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 ) ) let p, q be Element of (P --> Q); ::_thesis: 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 ) ) let p1, p2 be Element of P; ::_thesis: for q1, q2 being Element of Q st p = [p1,q1] & q = [p2,q2] holds ( p <= q iff ( p2 <= p1 & q1 <= q2 ) ) let q1, q2 be Element of Q; ::_thesis: ( p = [p1,q1] & q = [p2,q2] implies ( p <= q iff ( p2 <= p1 & q1 <= q2 ) ) ) assume that A1: p = [p1,q1] and A2: q = [p2,q2] ; ::_thesis: ( p <= q iff ( p2 <= p1 & q1 <= q2 ) ) reconsider r1 = p1, r2 = p2 as Element of (pcs-reverse P) by Def40; thus ( p <= q implies ( p2 <= p1 & q1 <= q2 ) ) ::_thesis: ( p2 <= p1 & q1 <= q2 implies p <= q ) proof assume p <= q ; ::_thesis: ( p2 <= p1 & q1 <= q2 ) then [p,q] in [" the InternalRel of (pcs-reverse P), the InternalRel of Q"] by ORDERS_2:def_5; then consider a, b, s, t being set such that A3: p = [a,b] and A4: q = [s,t] and A5: [a,s] in the InternalRel of (pcs-reverse P) and A6: [b,t] in the InternalRel of Q by YELLOW_3:def_1; A7: a = p1 by A1, A3, XTUPLE_0:1; A8: b = q1 by A1, A3, XTUPLE_0:1; s = p2 by A2, A4, XTUPLE_0:1; then r1 <= r2 by A5, A7, ORDERS_2:def_5; hence p2 <= p1 by Th33; ::_thesis: q1 <= q2 thus [q1,q2] in the InternalRel of Q by A2, A4, A6, A8, XTUPLE_0:1; :: according to ORDERS_2:def_5 ::_thesis: verum end; assume that A9: p2 <= p1 and A10: q1 <= q2 ; ::_thesis: p <= q r1 <= r2 by A9, Th33; then A11: [r1,r2] in the InternalRel of (pcs-reverse P) by ORDERS_2:def_5; [q1,q2] in the InternalRel of Q by A10, ORDERS_2:def_5; hence [p,q] in the InternalRel of (P --> Q) by A1, A2, A11, YELLOW_3:def_1; :: according to ORDERS_2:def_5 ::_thesis: verum 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 let P, Q be pcs-Str ; ::_thesis: 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 let p, q be Element of (P --> Q); ::_thesis: 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 let p1, p2 be Element of P; ::_thesis: for q1, q2 being Element of Q st p = [p1,q1] & q = [p2,q2] & p (--) q & p1 (--) p2 holds q1 (--) q2 let q1, q2 be Element of Q; ::_thesis: ( p = [p1,q1] & q = [p2,q2] & p (--) q & p1 (--) p2 implies q1 (--) q2 ) assume that A1: p = [p1,q1] and A2: q = [p2,q2] ; ::_thesis: ( not p (--) q or not p1 (--) p2 or q1 (--) q2 ) reconsider r1 = p1, r2 = p2 as Element of (pcs-reverse P) by Def40; assume [p,q] in the ToleranceRel of (P --> Q) ; :: according to PCS_0:def_7 ::_thesis: ( not p1 (--) p2 or q1 (--) q2 ) then consider a, b, s, t being set such that A3: p = [a,b] and A4: q = [s,t] and a in the carrier of (pcs-reverse P) and b in the carrier of Q and s in the carrier of (pcs-reverse P) and t in the carrier of Q and A5: ( [a,s] in the ToleranceRel of (pcs-reverse P) or [b,t] in the ToleranceRel of Q ) by Def2; A6: a = p1 by A1, A3, XTUPLE_0:1; A7: b = q1 by A1, A3, XTUPLE_0:1; A8: s = p2 by A2, A4, XTUPLE_0:1; t = q2 by A2, A4, XTUPLE_0:1; then ( r1 (--) r2 or q1 (--) q2 ) by A5, A6, A7, A8, Def7; hence ( not p1 (--) p2 or q1 (--) q2 ) by Th34; ::_thesis: verum 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 let P, Q be non empty pcs-Str ; ::_thesis: 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 let p, q be Element of (P --> Q); ::_thesis: 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 let p1, p2 be Element of P; ::_thesis: for q1, q2 being Element of Q st p = [p1,q1] & q = [p2,q2] & ( not p1 (--) p2 or q1 (--) q2 ) holds p (--) q let q1, q2 be Element of Q; ::_thesis: ( p = [p1,q1] & q = [p2,q2] & ( not p1 (--) p2 or q1 (--) q2 ) implies p (--) q ) assume that A1: p = [p1,q1] and A2: q = [p2,q2] ; ::_thesis: ( ( p1 (--) p2 & not q1 (--) q2 ) or p (--) q ) reconsider r1 = p1, r2 = p2 as Element of (pcs-reverse P) by Def40; reconsider w1 = [r1,q1], w2 = [r2,q2] as Element of ((pcs-reverse P) pcs-times Q) by A1, A2; assume ( not p1 (--) p2 or q1 (--) q2 ) ; ::_thesis: p (--) q then ( r1 (--) r2 or q1 (--) q2 ) by Th35; then w1 (--) w2 by Th38; hence p (--) q by A1, A2; ::_thesis: verum end; 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; 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 & 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 & 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 proof let S be Subset of P; ::_thesis: ( S is empty implies S is pcs-self-coherent ) assume A1: S is empty ; ::_thesis: S is pcs-self-coherent let x be Element of P; :: according to PCS_0:def_43 ::_thesis: for y being Element of P st x in S & y in S holds x (--) y thus for y being Element of P st x in S & y in S holds x (--) y by A1; ::_thesis: verum end; 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 & b1 is pcs-self-coherent-membered ) proof reconsider F = {{}} as Subset-Family of P by SETFAM_1:46; take F ; ::_thesis: ( not F is empty & F is pcs-self-coherent-membered ) thus not F is empty ; ::_thesis: F is pcs-self-coherent-membered let S be Subset of P; :: according to PCS_0:def_44 ::_thesis: ( S in F implies S is pcs-self-coherent ) assume S in F ; ::_thesis: S is pcs-self-coherent then S = {} P by TARSKI:def_1; hence S is pcs-self-coherent ; ::_thesis: verum 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 45 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 consider R being Relation of D such that A1: for x, y being set holds ( [x,y] in R iff ( x in D & y in D & S1[x,y] ) ) from RELSET_1:sch_1(); take R ; ::_thesis: for A, B being set holds ( [A,B] in R 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 ) ) ) ) thus for A, B being set holds ( [A,B] in R 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 ) ) ) ) by A1; ::_thesis: verum 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 let R1, R2 be Relation of D; ::_thesis: ( ( for A, B being set holds ( [A,B] in R1 iff ( A in D & B in D & ( for a being set st a in A 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 R2 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 ) ) ) ) ) implies R1 = R2 ) assume that A2: for A, B being set holds ( [A,B] in R1 iff ( A in D & B in D & ( for a being set st a in A holds ex b being set st ( b in B & [a,b] in the InternalRel of P ) ) ) ) and A3: for A, B being set holds ( [A,B] in R2 iff ( A in D & B in D & ( for a being set st a in A holds ex b being set st ( b in B & [a,b] in the InternalRel of P ) ) ) ) ; ::_thesis: R1 = R2 A4: for a, b being set holds ( [a,b] in R1 iff S1[a,b] ) by A2; A5: for a, b being set holds ( [a,b] in R2 iff S1[a,b] ) by A3; thus R1 = R2 from RELAT_1:sch_2(A4, A5); ::_thesis: verum end; 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 & 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 46 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 consider R being Relation of D such that A1: for x, y being set holds ( [x,y] in R iff ( x in D & y in D & S1[x,y] ) ) from RELSET_1:sch_1(); take R ; ::_thesis: for A, B being set holds ( [A,B] in R 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 ) ) ) thus for A, B being set holds ( [A,B] in R 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 ) ) ) by A1; ::_thesis: verum 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 let R1, R2 be Relation of D; ::_thesis: ( ( for A, B being set holds ( [A,B] in R1 iff ( A in D & B in D & ( for a, b being set st a in A & b in B holds [a,b] in the ToleranceRel of P ) ) ) ) & ( for A, B being set holds ( [A,B] in R2 iff ( A in D & B in D & ( for a, b being set st a in A & b in B holds [a,b] in the ToleranceRel of P ) ) ) ) implies R1 = R2 ) assume that A2: for A, B being set holds ( [A,B] in R1 iff ( A in D & B in D & ( for a, b being set st a in A & b in B holds [a,b] in the ToleranceRel of P ) ) ) and A3: for A, B being set holds ( [A,B] in R2 iff ( A in D & B in D & ( for a, b being set st a in A & b in B holds [a,b] in the ToleranceRel of P ) ) ) ; ::_thesis: R1 = R2 A4: for a, b being set holds ( [a,b] in R1 iff S1[a,b] ) by A2; A5: for a, b being set holds ( [a,b] in R2 iff S1[a,b] ) by A3; thus R1 = R2 from RELAT_1:sch_2(A4, A5); ::_thesis: verum end; 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 & 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 let P be RelStr ; ::_thesis: 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 ) ) ) ) let D be Subset-Family of P; ::_thesis: 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 ) ) ) ) let A, B be set ; ::_thesis: ( [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 ) ) ) ) thus ( [A,B] in pcs-general-power-IR (P,D) implies ( A in D & B in D & ( for a being Element of P st a in A holds ex b being Element of P st ( b in B & a <= b ) ) ) ) ::_thesis: ( 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 ) ) implies [A,B] in pcs-general-power-IR (P,D) ) proof assume A1: [A,B] in pcs-general-power-IR (P,D) ; ::_thesis: ( 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 ) ) ) hence A2: ( A in D & B in D ) by Def45; ::_thesis: for a being Element of P st a in A holds ex b being Element of P st ( b in B & a <= b ) let a be Element of P; ::_thesis: ( a in A implies ex b being Element of P st ( b in B & a <= b ) ) assume a in A ; ::_thesis: ex b being Element of P st ( b in B & a <= b ) then consider b being set such that A3: b in B and A4: [a,b] in the InternalRel of P by A1, Def45; reconsider b = b as Element of P by A2, A3; take b ; ::_thesis: ( b in B & a <= b ) thus ( b in B & a <= b ) by A3, A4, ORDERS_2:def_5; ::_thesis: verum end; assume that A5: A in D and A6: B in D and A7: for a being Element of P st a in A holds ex b being Element of P st ( b in B & a <= b ) ; ::_thesis: [A,B] in pcs-general-power-IR (P,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 let a be set ; ::_thesis: ( a in A implies ex b being set st ( b in B & [a,b] in the InternalRel of P ) ) assume A8: a in A ; ::_thesis: ex b being set st ( b in B & [a,b] in the InternalRel of P ) then reconsider a = a as Element of P by A5; consider b being Element of P such that A9: b in B and A10: a <= b by A7, A8; take b ; ::_thesis: ( b in B & [a,b] in the InternalRel of P ) thus ( b in B & [a,b] in the InternalRel of P ) by A9, A10, ORDERS_2:def_5; ::_thesis: verum end; hence [A,B] in pcs-general-power-IR (P,D) by A5, A6, Def45; ::_thesis: verum 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 let P be TolStr ; ::_thesis: 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 ) ) ) let D be Subset-Family of P; ::_thesis: 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 ) ) ) let A, B be set ; ::_thesis: ( [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 ) ) ) thus ( [A,B] in pcs-general-power-TR (P,D) implies ( A in D & B in D & ( for a, b being Element of P st a in A & b in B holds a (--) b ) ) ) ::_thesis: ( A in D & B in D & ( for a, b being Element of P st a in A & b in B holds a (--) b ) implies [A,B] in pcs-general-power-TR (P,D) ) proof assume A1: [A,B] in pcs-general-power-TR (P,D) ; ::_thesis: ( A in D & B in D & ( for a, b being Element of P st a in A & b in B holds a (--) b ) ) hence ( A in D & B in D ) by Def46; ::_thesis: for a, b being Element of P st a in A & b in B holds a (--) b let a, b be Element of P; ::_thesis: ( a in A & b in B implies a (--) b ) assume that A2: a in A and A3: b in B ; ::_thesis: a (--) b [a,b] in the ToleranceRel of P by A1, A2, A3, Def46; hence a (--) b by Def7; ::_thesis: verum end; assume that A4: A in D and A5: B in D and A6: for a, b being Element of P st a in A & b in B holds a (--) b ; ::_thesis: [A,B] in pcs-general-power-TR (P,D) for a, b being set st a in A & b in B holds [a,b] in the ToleranceRel of P proof let a, b be set ; ::_thesis: ( a in A & b in B implies [a,b] in the ToleranceRel of P ) assume that A7: a in A and A8: b in B ; ::_thesis: [a,b] in the ToleranceRel of P reconsider a = a, b = b as Element of P by A4, A5, A7, A8; a (--) b by A6, A7, A8; hence [a,b] in the ToleranceRel of P by Def7; ::_thesis: verum end; hence [A,B] in pcs-general-power-TR (P,D) by A4, A5, Def46; ::_thesis: verum end; 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 & p9 <= q9 ) proof let P be pcs-Str ; ::_thesis: 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 ) let D be set ; ::_thesis: 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 ) set R = pcs-general-power (P,D); let p, q be Element of (pcs-general-power (P,D)); ::_thesis: ( p <= q implies for p9 being Element of P st p9 in p holds ex q9 being Element of P st ( q9 in q & p9 <= q9 ) ) assume A1: [p,q] in the InternalRel of (pcs-general-power (P,D)) ; :: according to ORDERS_2:def_5 ::_thesis: for p9 being Element of P st p9 in p holds ex q9 being Element of P st ( q9 in q & p9 <= q9 ) let p9 be Element of P; ::_thesis: ( p9 in p implies ex q9 being Element of P st ( q9 in q & p9 <= q9 ) ) assume p9 in p ; ::_thesis: ex q9 being Element of P st ( q9 in q & p9 <= q9 ) then consider b being set such that A2: b in q and A3: [p9,b] in the InternalRel of P by A1, Def45; reconsider b = b as Element of P by A3, ZFMISC_1:87; take b ; ::_thesis: ( b in q & p9 <= b ) thus ( b in q & [p9,b] in the InternalRel of P ) by A2, A3; :: according to ORDERS_2:def_5 ::_thesis: verum 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 (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 & p9 <= q9 ) ) holds p <= q proof let P be pcs-Str ; ::_thesis: 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 & p9 <= q9 ) ) holds p <= q let D be non empty Subset-Family of P; ::_thesis: 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 & p9 <= q9 ) ) holds p <= q set R = pcs-general-power D; let p, q be Element of (pcs-general-power D); ::_thesis: ( ( for p9 being Element of P st p9 in p holds ex q9 being Element of P st ( q9 in q & p9 <= q9 ) ) implies p <= q ) assume A1: for p9 being Element of P st p9 in p holds ex q9 being Element of P st ( q9 in q & p9 <= q9 ) ; ::_thesis: p <= q A2: p in D ; for a being set st a in p holds ex b being set st ( b in q & [a,b] in the InternalRel of P ) proof let a be set ; ::_thesis: ( a in p implies ex b being set st ( b in q & [a,b] in the InternalRel of P ) ) assume A3: a in p ; ::_thesis: ex b being set st ( b in q & [a,b] in the InternalRel of P ) then reconsider a = a as Element of P by A2; consider q9 being Element of P such that A4: q9 in q and A5: a <= q9 by A1, A3; take q9 ; ::_thesis: ( q9 in q & [a,q9] in the InternalRel of P ) thus ( q9 in q & [a,q9] in the InternalRel of P ) by A4, A5, ORDERS_2:def_5; ::_thesis: verum end; hence [p,q] in the InternalRel of (pcs-general-power D) by Def45; :: according to ORDERS_2:def_5 ::_thesis: verum 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 proof let P be pcs-Str ; ::_thesis: 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 let D be set ; ::_thesis: 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 set R = pcs-general-power (P,D); let p, q be Element of (pcs-general-power (P,D)); ::_thesis: ( p (--) q implies for p9, q9 being Element of P st p9 in p & q9 in q holds p9 (--) q9 ) assume A1: [p,q] in the ToleranceRel of (pcs-general-power (P,D)) ; :: according to PCS_0:def_7 ::_thesis: for p9, q9 being Element of P st p9 in p & q9 in q holds p9 (--) q9 let p9, q9 be Element of P; ::_thesis: ( p9 in p & q9 in q implies p9 (--) q9 ) assume that A2: p9 in p and A3: q9 in q ; ::_thesis: p9 (--) q9 thus [p9,q9] in the ToleranceRel of P by A1, A2, A3, Def46; :: according to PCS_0:def_7 ::_thesis: verum end; 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 & q9 in q holds p9 (--) q9 ) holds p (--) q proof let P be pcs-Str ; ::_thesis: 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 & q9 in q holds p9 (--) q9 ) holds p (--) q let D be non empty Subset-Family of P; ::_thesis: for p, q being Element of (pcs-general-power D) st ( for p9, q9 being Element of P st p9 in p & q9 in q holds p9 (--) q9 ) holds p (--) q set R = pcs-general-power D; let p, q be Element of (pcs-general-power D); ::_thesis: ( ( for p9, q9 being Element of P st p9 in p & q9 in q holds p9 (--) q9 ) implies p (--) q ) assume A1: for p9, q9 being Element of P st p9 in p & q9 in q holds p9 (--) q9 ; ::_thesis: p (--) q A2: p in D ; A3: q in D ; now__::_thesis:_for_a,_b_being_set_st_a_in_p_&_b_in_q_holds_ [a,b]_in_the_ToleranceRel_of_P let a, b be set ; ::_thesis: ( a in p & b in q implies [a,b] in the ToleranceRel of P ) assume that A4: a in p and A5: b in q ; ::_thesis: [a,b] in the ToleranceRel of P reconsider a1 = a, b1 = b as Element of P by A2, A3, A4, A5; a1 (--) b1 by A1, A4, A5; hence [a,b] in the ToleranceRel of P by Def7; ::_thesis: verum end; hence [p,q] in the ToleranceRel of (pcs-general-power D) by Def46; :: according to PCS_0:def_7 ::_thesis: verum 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; cluster pcs-general-power (P,D) -> reflexive ; coherence pcs-general-power D is reflexive proof set R = pcs-general-power D; let x be set ; :: according to RELAT_2:def_1,ORDERS_2:def_2 ::_thesis: ( not x in the carrier of (pcs-general-power D) or [^,^] in the InternalRel of (pcs-general-power D) ) assume A1: x in the carrier of (pcs-general-power D) ; ::_thesis: [^,^] in the InternalRel of (pcs-general-power D) for a being set st a in x holds ex b being set st ( b in x & [a,b] in the InternalRel of P ) proof let a be set ; ::_thesis: ( a in x implies ex b being set st ( b in x & [a,b] in the InternalRel of P ) ) assume A2: a in x ; ::_thesis: ex b being set st ( b in x & [a,b] in the InternalRel of P ) take a ; ::_thesis: ( a in x & [a,a] in the InternalRel of P ) thus a in x by A2; ::_thesis: [a,a] in the InternalRel of P field the InternalRel of P = the carrier of P by ORDERS_1:12; then the InternalRel of P is_reflexive_in the carrier of P by RELAT_2:def_9; hence [a,a] in the InternalRel of P by A1, A2, RELAT_2:def_1; ::_thesis: verum end; hence [^,^] in the InternalRel of (pcs-general-power D) by A1, Def45; ::_thesis: verum end; 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 proof set R = pcs-general-power (P,D); set IR = the InternalRel of (pcs-general-power (P,D)); let x, y, z be set ; :: according to RELAT_2:def_8,ORDERS_2:def_3 ::_thesis: ( not x in the carrier of (pcs-general-power (P,D)) or not y in the carrier of (pcs-general-power (P,D)) or not z in the carrier of (pcs-general-power (P,D)) or not [^,^] in the InternalRel of (pcs-general-power (P,D)) or not [^,^] in the InternalRel of (pcs-general-power (P,D)) or [^,^] in the InternalRel of (pcs-general-power (P,D)) ) assume that A1: x in the carrier of (pcs-general-power (P,D)) and y in the carrier of (pcs-general-power (P,D)) and A2: z in the carrier of (pcs-general-power (P,D)) and A3: [x,y] in the InternalRel of (pcs-general-power (P,D)) and A4: [y,z] in the InternalRel of (pcs-general-power (P,D)) ; ::_thesis: [^,^] in the InternalRel of (pcs-general-power (P,D)) for a being set st a in x holds ex b being set st ( b in z & [a,b] in the InternalRel of P ) proof let a be set ; ::_thesis: ( a in x implies ex b being set st ( b in z & [a,b] in the InternalRel of P ) ) assume a in x ; ::_thesis: ex b being set st ( b in z & [a,b] in the InternalRel of P ) then consider b being set such that A5: b in y and A6: [a,b] in the InternalRel of P by A3, Def45; consider c being set such that A7: c in z and A8: [b,c] in the InternalRel of P by A4, A5, Def45; take c ; ::_thesis: ( c in z & [a,c] in the InternalRel of P ) thus c in z by A7; ::_thesis: [a,c] in the InternalRel of P A9: the InternalRel of P is_transitive_in the carrier of P by ORDERS_2:def_3; A10: a in the carrier of P by A6, ZFMISC_1:87; A11: b in the carrier of P by A6, ZFMISC_1:87; c in the carrier of P by A8, ZFMISC_1:87; hence [a,c] in the InternalRel of P by A6, A8, A9, A10, A11, RELAT_2:def_8; ::_thesis: verum end; hence [^,^] in the InternalRel of (pcs-general-power (P,D)) by A1, A2, Def45; ::_thesis: verum end; 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 proof let x be set ; :: according to RELAT_2:def_1,PCS_0:def_9 ::_thesis: ( not x in the carrier of (pcs-general-power D) or [^,^] in the ToleranceRel of (pcs-general-power D) ) assume A1: x in the carrier of (pcs-general-power D) ; ::_thesis: [^,^] in the ToleranceRel of (pcs-general-power D) then reconsider x = x as Subset of P ; A2: x is pcs-self-coherent by A1, Def44; now__::_thesis:_for_a,_b_being_set_st_a_in_x_&_b_in_x_holds_ [a,b]_in_the_ToleranceRel_of_P let a, b be set ; ::_thesis: ( a in x & b in x implies [a,b] in the ToleranceRel of P ) assume that A3: a in x and A4: b in x ; ::_thesis: [a,b] in the ToleranceRel of P reconsider a1 = a, b1 = b as Element of P by A3, A4; a1 (--) b1 by A2, A3, A4, Def43; hence [a,b] in the ToleranceRel of P by Def7; ::_thesis: verum end; hence [^,^] in the ToleranceRel of (pcs-general-power D) by A1, Def46; ::_thesis: verum end; 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 proof set R = pcs-general-power D; let x, y be set ; :: according to RELAT_2:def_3,PCS_0:def_11 ::_thesis: ( not x in the carrier of (pcs-general-power D) or not y in the carrier of (pcs-general-power D) or not [^,^] in the ToleranceRel of (pcs-general-power D) or [^,^] in the ToleranceRel of (pcs-general-power D) ) assume A1: x in the carrier of (pcs-general-power D) ; ::_thesis: ( not y in the carrier of (pcs-general-power D) or not [^,^] in the ToleranceRel of (pcs-general-power D) or [^,^] in the ToleranceRel of (pcs-general-power D) ) assume A2: y in the carrier of (pcs-general-power D) ; ::_thesis: ( not [^,^] in the ToleranceRel of (pcs-general-power D) or [^,^] in the ToleranceRel of (pcs-general-power D) ) assume A3: [x,y] in the ToleranceRel of (pcs-general-power D) ; ::_thesis: [^,^] in the ToleranceRel of (pcs-general-power D) now__::_thesis:_for_a,_b_being_set_st_a_in_y_&_b_in_x_holds_ [a,b]_in_the_ToleranceRel_of_P let a, b be set ; ::_thesis: ( a in y & b in x implies [a,b] in the ToleranceRel of P ) assume that A4: a in y and A5: b in x ; ::_thesis: [a,b] in the ToleranceRel of P reconsider a1 = a, b1 = b as Element of P by A1, A2, A4, A5; [b,a] in the ToleranceRel of P by A3, A4, A5, Def46; then b1 (--) a1 by Def7; hence [a,b] in the ToleranceRel of P by Def7; ::_thesis: verum end; hence [^,^] in the ToleranceRel of (pcs-general-power D) by A1, A2, Def46; ::_thesis: verum end; 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 proof set R = pcs-general-power D; let p, p9, q, q9 be Element of (pcs-general-power D); :: according to PCS_0:def_22 ::_thesis: ( p (--) q & p9 <= p & q9 <= q implies p9 (--) q9 ) assume that A1: p (--) q and A2: p9 <= p and A3: q9 <= q ; ::_thesis: p9 (--) q9 A4: [p9,p] in the InternalRel of (pcs-general-power D) by A2, ORDERS_2:def_5; A5: [q9,q] in the InternalRel of (pcs-general-power D) by A3, ORDERS_2:def_5; A6: p9 in the carrier of (pcs-general-power D) by A4, ZFMISC_1:87; A7: q9 in the carrier of (pcs-general-power D) by A5, ZFMISC_1:87; now__::_thesis:_for_a,_b_being_set_st_a_in_p9_&_b_in_q9_holds_ [a,b]_in_the_ToleranceRel_of_P let a, b be set ; ::_thesis: ( a in p9 & b in q9 implies [a,b] in the ToleranceRel of P ) assume that A8: a in p9 and A9: b in q9 ; ::_thesis: [a,b] in the ToleranceRel of P reconsider a1 = a, b1 = b as Element of P by A6, A7, A8, A9; consider p1 being Element of P such that A10: p1 in p and A11: a1 <= p1 by A2, A8, Th44; consider q1 being Element of P such that A12: q1 in q and A13: b1 <= q1 by A3, A9, Th44; p1 (--) q1 by A1, A10, A12, Th46; then a1 (--) b1 by A11, A13, Def22; hence [a,b] in the ToleranceRel of P by Def7; ::_thesis: verum end; hence [p9,q9] in the ToleranceRel of (pcs-general-power D) by A6, Def46; :: according to PCS_0:def_7 ::_thesis: verum end; 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 proof take {} P ; ::_thesis: {} P is pcs-self-coherent thus {} P is pcs-self-coherent ; ::_thesis: verum 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 let P be pcs-Str ; ::_thesis: for X being set st X in pcs-coherent-power P holds X is pcs-self-coherent Subset of P let X be set ; ::_thesis: ( X in pcs-coherent-power P implies X is pcs-self-coherent Subset of P ) assume X in pcs-coherent-power P ; ::_thesis: X is pcs-self-coherent Subset of P then ex Y being Subset of P st ( X = Y & Y is pcs-self-coherent ) ; hence X is pcs-self-coherent Subset of P ; ::_thesis: verum end; registration let P be pcs-Str ; cluster pcs-coherent-power P -> non empty ; coherence not pcs-coherent-power P is empty proof {} P in pcs-coherent-power P ; hence not pcs-coherent-power P is empty ; ::_thesis: verum end; 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 proof pcs-coherent-power P c= bool the carrier of P proof let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in pcs-coherent-power P or X in bool the carrier of P ) assume X in pcs-coherent-power P ; ::_thesis: X in bool the carrier of P then X is Subset of P by Th48; hence X in bool the carrier of P ; ::_thesis: verum end; hence pcs-coherent-power P is Subset-Family of P ; ::_thesis: verum end; 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 proof pcs-coherent-power P is pcs-self-coherent-membered proof let S be Subset of P; :: according to PCS_0:def_44 ::_thesis: ( S in pcs-coherent-power P implies S is pcs-self-coherent ) thus ( S in pcs-coherent-power P implies S is pcs-self-coherent ) by Th48; ::_thesis: verum end; hence for b1 being Subset-Family of P st b1 = pcs-coherent-power P holds b1 is pcs-self-coherent-membered ; ::_thesis: verum end; 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;