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