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