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