let X be non empty TopSpace; :: thesis: for X1, X2, X0 being non empty SubSpace of X holds
( ( X1 union X2 misses X0 implies ( X1 misses X0 & X2 misses X0 ) ) & ( X1 misses X0 & X2 misses X0 implies X1 union X2 misses X0 ) & ( X0 misses X1 union X2 implies ( X0 misses X1 & X0 misses X2 ) ) & ( X0 misses X1 & X0 misses X2 implies X0 misses X1 union X2 ) )
let X1, X2, X0 be non empty SubSpace of X; :: thesis: ( ( X1 union X2 misses X0 implies ( X1 misses X0 & X2 misses X0 ) ) & ( X1 misses X0 & X2 misses X0 implies X1 union X2 misses X0 ) & ( X0 misses X1 union X2 implies ( X0 misses X1 & X0 misses X2 ) ) & ( X0 misses X1 & X0 misses X2 implies X0 misses X1 union X2 ) )
reconsider A0 = the carrier of X0 as Subset of X by TSEP_1:1;
reconsider A1 = the carrier of X1 as Subset of X by TSEP_1:1;
reconsider A2 = the carrier of X2 as Subset of X by TSEP_1:1;
thus ( X1 union X2 misses X0 iff ( X1 misses X0 & X2 misses X0 ) ) :: thesis: ( X0 misses X1 union X2 iff ( X0 misses X1 & X0 misses X2 ) )

proof

thus ( X1 union X2 misses X0 implies ( X1 misses X0 & X2 misses X0 ) ) :: thesis: ( X1 misses X0 & X2 misses X0 implies X1 union X2 misses X0 )

proof

assume X1 union X2 misses X0 ; :: thesis: ( X1 misses X0 & X2 misses X0 )
then the carrier of (X1 union X2) misses A0 by TSEP_1:def 3;
then the carrier of (X1 union X2) /\ A0 = {} by XBOOLE_0:def 7;
then (A1 \/ A2) /\ A0 = {} by TSEP_1:def 2;
then (A1 /\ A0) \/ (A2 /\ A0) = {} by XBOOLE_1:23;
then ( A1 /\ A0 = {} & A2 /\ A0 = {} ) ;
then ( A1 misses A0 & A2 misses A0 ) by XBOOLE_0:def 7;
hence ( X1 misses X0 & X2 misses X0 ) by TSEP_1:def 3; :: thesis: verum

end;

thus ( X1 misses X0 & X2 misses X0 implies X1 union X2 misses X0 ) :: thesis: verum

proof

assume ( X1 misses X0 & X2 misses X0 ) ; :: thesis: X1 union X2 misses X0
then ( A1 misses A0 & A2 misses A0 ) by TSEP_1:def 3;
then ( A1 /\ A0 = {} & A2 /\ A0 = {} ) by XBOOLE_0:def 7;
then (A1 /\ A0) \/ (A2 /\ A0) = {} ;
then (A1 \/ A2) /\ A0 = {} by XBOOLE_1:23;
then the carrier of (X1 union X2) /\ A0 = {} by TSEP_1:def 2;
then the carrier of (X1 union X2) misses A0 by XBOOLE_0:def 7;
hence X1 union X2 misses X0 by TSEP_1:def 3; :: thesis: verum

end;

end;

hence ( X0 misses X1 union X2 iff ( X0 misses X1 & X0 misses X2 ) ) ; :: thesis: verum