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

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