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