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

( 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