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

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