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