let X be non empty TopSpace; :: thesis: for X0 being non empty SubSpace of X holds X0 meet X0 = TopStruct(# the carrier of X0, the topology of X0 #)

let X0 be non empty SubSpace of X; :: thesis: X0 meet X0 = TopStruct(# the carrier of X0, the topology of X0 #)

A1: X0 is SubSpace of X0 by TSEP_1:2;

then X0 meets X0 by Th17;

hence X0 meet X0 = TopStruct(# the carrier of X0, the topology of X0 #) by A1, TSEP_1:28; :: thesis: verum

let X0 be non empty SubSpace of X; :: thesis: X0 meet X0 = TopStruct(# the carrier of X0, the topology of X0 #)

A1: X0 is SubSpace of X0 by TSEP_1:2;

then X0 meets X0 by Th17;

hence X0 meet X0 = TopStruct(# the carrier of X0, the topology of X0 #) by A1, TSEP_1:28; :: thesis: verum