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