let X be non empty TopSpace; :: thesis: for X1, X2 being non empty SubSpace of X st X1 is SubSpace of X2 holds
for x1 being Point of X1 ex x2 being Point of X2 st x2 = x1
let X1, X2 be non empty SubSpace of X; :: thesis: ( X1 is SubSpace of X2 implies for x1 being Point of X1 ex x2 being Point of X2 st x2 = x1 )
assume X1 is SubSpace of X2 ; :: thesis: for x1 being Point of X1 ex x2 being Point of X2 st x2 = x1
then A1: the carrier of X1 c= the carrier of X2 by TSEP_1:4;
let x1 be Point of X1; :: thesis: ex x2 being Point of X2 st x2 = x1
x1 in the carrier of X1 ;
then reconsider x2 = x1 as Point of X2 by A1;
take x2 ; :: thesis: x2 = x1
thus x2 = x1 ; :: thesis: verum