let X be non empty TopSpace; :: thesis: for X1 being non empty closed SubSpace of X
for X2 being non empty SubSpace of X st the carrier of X1 c= the carrier of X2 holds
X1 is non empty closed SubSpace of X2
let X1 be non empty closed SubSpace of X; :: thesis: for X2 being non empty SubSpace of X st the carrier of X1 c= the carrier of X2 holds
X1 is non empty closed SubSpace of X2
let X2 be non empty SubSpace of X; :: thesis: ( the carrier of X1 c= the carrier of X2 implies X1 is non empty closed SubSpace of X2 )
assume the carrier of X1 c= the carrier of X2 ; :: thesis: X1 is non empty closed SubSpace of X2
then reconsider B = the carrier of X1 as Subset of X2 ;
now :: thesis: for C being Subset of X2 st C = the carrier of X1 holds
C is closed
let C be Subset of X2; :: thesis: ( C = the carrier of X1 implies C is closed )
assume A1: C = the carrier of X1 ; :: thesis: C is closed
then reconsider A = C as Subset of X by BORSUK_1:1;
A2: A /\ ([#] X2) = C by XBOOLE_1:28;
A is closed by A1, Th11;
hence C is closed by A2, PRE_TOPC:13; :: thesis: verum
end;
then B is closed ;
hence X1 is non empty closed SubSpace of X2 by Th4, Th11; :: thesis: verum