let x, y be Element of (1TopSp {a}); :: according to STRUCT_0:def 10 :: thesis: x = y
a = x by TARSKI:def 1;
hence x = y by TARSKI:def 1; :: thesis: verum