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) )
thus T | P is SubSpace of T | (P \/ Q) :: thesis: T | Q is SubSpace of T | (P \/ Q)

proof

A1: [#] (T | P) = P by PRE_TOPC:def 10;
[#] (T | (P \/ Q)) = P \/ Q by PRE_TOPC:def 10;
hence T | P is SubSpace of T | (P \/ Q) by A1, Th4, XBOOLE_1:7; :: thesis: verum

end;

A2: [#] (T | Q) = Q by PRE_TOPC:def 10;
[#] (T | (P \/ Q)) = P \/ Q by PRE_TOPC:def 10;
hence T | Q is SubSpace of T | (P \/ Q) by A2, Th4, XBOOLE_1:7; :: thesis: verum