let a, b be Element of TopRelStr(# {x},R,T #); :: according to STRUCT_0:def 10 :: thesis: a = b
( a = x & b = x ) by TARSKI:def 1;
hence a = b ; :: thesis: verum