let L be RelStr ; :: thesis: ex f being Function of L,L st f is isomorphic
take id L ; :: thesis: id L is isomorphic
thus id L is isomorphic ; :: thesis: verum