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