let X be non empty TopSpace; :: thesis: for Y0 being SubSpace of X
for A being Subset of X
for B being Subset of Y0 st A c= B holds
Int A c= Int B
let Y0 be SubSpace of X; :: thesis: for A being Subset of X
for B being Subset of Y0 st A c= B holds
Int A c= Int B
let A be Subset of X; :: thesis: for B being Subset of Y0 st A c= B holds
Int A c= Int B
let B be Subset of Y0; :: thesis: ( A c= B implies Int A c= Int B )
A1: Int A c= A by TOPS_1:16;
assume A c= B ; :: thesis: Int A c= Int B
then A2: Int A c= B by A1, XBOOLE_1:1;
then reconsider C = Int A as Subset of Y0 by XBOOLE_1:1;
C is open by TOPS_2:25;
hence Int A c= Int B by A2, TOPS_1:24; :: thesis: verum