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 ; :: according to PCS_0:def 22 :: thesis: for p', q, q' being Element of st p (--) q & p' <= p & q' <= q holds
p' (--) q'
thus for p', q, q' being Element of st p (--) q & p' <= p & q' <= q holds
p' (--) q' by Def7; :: thesis: verum