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 ; :: thesis: verum