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

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