take IT = the E -respecting Element of U -InterpretersOf S; :: thesis: IT is E -respecting
thus IT is E -respecting ; :: thesis: verum