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

Y1 union Y2 is SubSpace of X1 union X2

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

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

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

then the carrier of Y1 \/ the carrier of Y2 c= the carrier of X1 \/ the carrier of X2 by XBOOLE_1:13;

then the carrier of (Y1 union Y2) c= the carrier of X1 \/ the carrier of X2 by TSEP_1:def 2;

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

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

Y1 union Y2 is SubSpace of X1 union X2

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

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

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

then the carrier of Y1 \/ the carrier of Y2 c= the carrier of X1 \/ the carrier of X2 by XBOOLE_1:13;

then the carrier of (Y1 union Y2) c= the carrier of X1 \/ the carrier of X2 by TSEP_1:def 2;

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

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