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