let X be non empty TopSpace; :: thesis: for X0, X1, X2 being non empty SubSpace of X st X0 is SubSpace of X1 & ( X1 misses X2 or X2 misses X1 ) holds
( X0 misses X2 & X2 misses X0 )
let X0, X1, X2 be non empty SubSpace of X; :: thesis: ( X0 is SubSpace of X1 & ( X1 misses X2 or X2 misses X1 ) implies ( X0 misses X2 & X2 misses X0 ) )
reconsider A0 = the carrier of X0, A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by TSEP_1:1;
assume X0 is SubSpace of X1 ; :: thesis: ( ( not X1 misses X2 & not X2 misses X1 ) or ( X0 misses X2 & X2 misses X0 ) )
then A1: A0 c= A1 by TSEP_1:4;

A2: now :: thesis: ( X1 misses X2 & ( X1 misses X2 or X2 misses X1 ) implies ( X0 misses X2 & X2 misses X0 ) )

assume X1 misses X2 ; :: thesis: ( ( not X1 misses X2 & not X2 misses X1 ) or ( X0 misses X2 & X2 misses X0 ) )
then A2 misses A1 by TSEP_1:def 3;
hence ( ( not X1 misses X2 & not X2 misses X1 ) or ( X0 misses X2 & X2 misses X0 ) ) by TSEP_1:def 3, A1, XBOOLE_1:63; :: thesis: verum

end;

assume ( X1 misses X2 or X2 misses X1 ) ; :: thesis: ( X0 misses X2 & X2 misses X0 )
hence ( X0 misses X2 & X2 misses X0 ) by A2; :: thesis: verum