let X be non empty TopSpace; :: thesis: for X1, Y1, X2, Y2 being non empty SubSpace of X st X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & ( Y1 misses Y2 or Y1 meet Y2 misses X1 union X2 ) holds
( Y1 misses X2 & Y2 misses X1 )
let X1, Y1, X2, Y2 be non empty SubSpace of X; :: thesis: ( X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & ( Y1 misses Y2 or Y1 meet Y2 misses X1 union X2 ) implies ( Y1 misses X2 & Y2 misses X1 ) )
assume A1: ( X1 is SubSpace of Y1 & X2 is SubSpace of Y2 ) ; :: thesis: ( ( not Y1 misses Y2 & not Y1 meet Y2 misses X1 union X2 ) or ( Y1 misses X2 & Y2 misses X1 ) )
assume A2: ( Y1 misses Y2 or Y1 meet Y2 misses X1 union X2 ) ; :: thesis: ( Y1 misses X2 & Y2 misses X1 )

now

assume A3: not Y1 misses Y2 ; :: thesis: ( Y1 misses X2 & Y2 misses X1 )

A4: now

assume Y1 meets X2 ; :: thesis: contradiction
then ( Y1 meet Y2 meets X2 & X2 is SubSpace of X1 union X2 ) by A1, Th34, TSEP_1:22;
hence contradiction by A2, A3, Th23; :: thesis: verum

end;

now

assume Y2 meets X1 ; :: thesis: contradiction
then ( Y1 meet Y2 meets X1 & X1 is SubSpace of X1 union X2 ) by A1, Th34, TSEP_1:22;
hence contradiction by A2, A3, Th23; :: thesis: verum

end;

hence ( Y1 misses X2 & Y2 misses X1 ) by A4; :: thesis: verum

end;

hence ( Y1 misses X2 & Y2 misses X1 ) by A1, Th24; :: thesis: verum