let X be non empty TopSpace; :: thesis: for X0 being non empty SubSpace of X holds X0 union X0 = TopStruct(# the carrier of X0, the topology of X0 #)
let X0 be non empty SubSpace of X; :: thesis: X0 union X0 = TopStruct(# the carrier of X0, the topology of X0 #)
X0 is SubSpace of X0 by TSEP_1:2;
hence X0 union X0 = TopStruct(# the carrier of X0, the topology of X0 #) by TSEP_1:23; :: thesis: verum