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;

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

( 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 or X2 misses X1 )
; :: thesis: ( 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;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

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