let T be non empty TopSpace; :: thesis: for P, Q being Subset of T holds
( T | P is SubSpace of T | (P \/ Q) & T | Q is SubSpace of T | (P \/ Q) )
let P, Q be Subset of T; :: thesis: ( T | P is SubSpace of T | (P \/ Q) & T | Q is SubSpace of T | (P \/ Q) )
( [#] (T | P) = P & [#] (T | (P \/ Q)) = P \/ Q ) by PRE_TOPC:def 5;
hence T | P is SubSpace of T | (P \/ Q) by Th3, XBOOLE_1:7; :: thesis: T | Q is SubSpace of T | (P \/ Q)
( [#] (T | Q) = Q & [#] (T | (P \/ Q)) = P \/ Q ) by PRE_TOPC:def 5;
hence T | Q is SubSpace of T | (P \/ Q) by Th3, XBOOLE_1:7; :: thesis: verum