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