take s = TheEqSymbOf S; :: thesis: s is relational
thus s is relational ; :: thesis: verum