take {<*1*>} ; :: thesis: ( {<*1*>} is R-orthonormal & not {<*1*>} is empty )
thus ( {<*1*>} is R-orthonormal & not {<*1*>} is empty ) ; :: thesis: verum