let z1, z2 be Element of RelStr(# {x},R #); :: according to STRUCT_0:def 10 :: thesis: z1 = z2
z1 = x by TARSKI:def 1;
hence z1 = z2 by TARSKI:def 1; :: thesis: verum