let T be non empty TopSpace; :: thesis: for A, B being Subset of T st A c= B holds
T | A is SubSpace of T | B
let A, B be Subset of T; :: thesis: ( A c= B implies T | A is SubSpace of T | B )
assume A c= B ; :: thesis: T | A is SubSpace of T | B
then A \/ B = B by XBOOLE_1:12;
hence T | A is SubSpace of T | B by Th4; :: thesis: verum