let X be non empty TopSpace; :: thesis: for X0, X1, X2 being non empty SubSpace of X st X1 is SubSpace of X0 & X2 is SubSpace of X0 holds

X1 union X2 is SubSpace of X0

let X0, X1, X2 be non empty SubSpace of X; :: thesis: ( X1 is SubSpace of X0 & X2 is SubSpace of X0 implies X1 union X2 is SubSpace of X0 )

assume ( X1 is SubSpace of X0 & X2 is SubSpace of X0 ) ; :: thesis: X1 union X2 is SubSpace of X0

then ( the carrier of X1 c= the carrier of X0 & the carrier of X2 c= the carrier of X0 ) by TSEP_1:4;

then the carrier of X1 \/ the carrier of X2 c= the carrier of X0 by XBOOLE_1:8;

then the carrier of (X1 union X2) c= the carrier of X0 by TSEP_1:def 2;

hence X1 union X2 is SubSpace of X0 by TSEP_1:4; :: thesis: verum

X1 union X2 is SubSpace of X0

let X0, X1, X2 be non empty SubSpace of X; :: thesis: ( X1 is SubSpace of X0 & X2 is SubSpace of X0 implies X1 union X2 is SubSpace of X0 )

assume ( X1 is SubSpace of X0 & X2 is SubSpace of X0 ) ; :: thesis: X1 union X2 is SubSpace of X0

then ( the carrier of X1 c= the carrier of X0 & the carrier of X2 c= the carrier of X0 ) by TSEP_1:4;

then the carrier of X1 \/ the carrier of X2 c= the carrier of X0 by XBOOLE_1:8;

then the carrier of (X1 union X2) c= the carrier of X0 by TSEP_1:def 2;

hence X1 union X2 is SubSpace of X0 by TSEP_1:4; :: thesis: verum