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