let X be non empty TopSpace; :: thesis: for X1 being open SubSpace of X
for X2 being non empty SubSpace of X st the carrier of X1 c= the carrier of X2 holds
X1 is open SubSpace of X2
let X1 be open 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 open SubSpace of X2
let X2 be non empty SubSpace of X; :: thesis: ( the carrier of X1 c= the carrier of X2 implies X1 is open SubSpace of X2 )
assume the carrier of X1 c= the carrier of X2 ; :: thesis: X1 is open 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 open

let C be Subset of X2; :: thesis: ( C = the carrier of X1 implies C is open )
assume A1: C = the carrier of X1 ; :: thesis: C is open
then reconsider A = C as Subset of X by BORSUK_1:1;
A2: A /\ ([#] X2) = C by XBOOLE_1:28;
A is open by A1, Th16;
hence C is open by A2, TOPS_2:24; :: thesis: verum

end;

then B is open ;
hence X1 is open SubSpace of X2 by Th4, Th16; :: thesis: verum