let X be non empty TopSpace; :: thesis: for X0, X1, X2 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 X0, X1, X2 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;

A1: ( X1 union X2 misses X0 implies ( X1 misses X0 & X2 misses X0 ) )

thus ( X0 misses X1 union X2 iff ( X0 misses X1 & X0 misses X2 ) ) by A1, A4; :: thesis: verum

( ( 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 X0, X1, X2 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;

A1: ( X1 union X2 misses X0 implies ( X1 misses X0 & X2 misses X0 ) )

proof

A4:
( X1 misses X0 & X2 misses X0 implies X1 union X2 misses X0 )
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 (A1 \/ A2) /\ A0 = {} by TSEP_1:def 2;

then A2: (A1 /\ A0) \/ (A2 /\ A0) = {} by XBOOLE_1:23;

then A3: A2 misses A0 ;

A1 /\ A0 = {} by A2;

then A1 misses A0 ;

hence ( X1 misses X0 & X2 misses X0 ) by A3, TSEP_1:def 3; :: thesis: verum

end;then the carrier of (X1 union X2) misses A0 by TSEP_1:def 3;

then (A1 \/ A2) /\ A0 = {} by TSEP_1:def 2;

then A2: (A1 /\ A0) \/ (A2 /\ A0) = {} by XBOOLE_1:23;

then A3: A2 misses A0 ;

A1 /\ A0 = {} by A2;

then A1 misses A0 ;

hence ( X1 misses X0 & X2 misses X0 ) by A3, TSEP_1:def 3; :: thesis: verum

proof

hence
( X1 union X2 misses X0 iff ( X1 misses X0 & X2 misses X0 ) )
by A1; :: thesis: ( X0 misses X1 union X2 iff ( X0 misses X1 & X0 misses X2 ) )
assume that

A5: X1 misses X0 and

A6: X2 misses X0 ; :: thesis: X1 union X2 misses X0

A1 misses A0 by A5, TSEP_1:def 3;

then A7: A1 /\ A0 = {} ;

A2 misses A0 by A6, TSEP_1:def 3;

then (A1 /\ A0) \/ (A2 /\ A0) = {} by A7;

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 ;

hence X1 union X2 misses X0 by TSEP_1:def 3; :: thesis: verum

end;A5: X1 misses X0 and

A6: X2 misses X0 ; :: thesis: X1 union X2 misses X0

A1 misses A0 by A5, TSEP_1:def 3;

then A7: A1 /\ A0 = {} ;

A2 misses A0 by A6, TSEP_1:def 3;

then (A1 /\ A0) \/ (A2 /\ A0) = {} by A7;

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 ;

hence X1 union X2 misses X0 by TSEP_1:def 3; :: thesis: verum

thus ( X0 misses X1 union X2 iff ( X0 misses X1 & X0 misses X2 ) ) by A1, A4; :: thesis: verum