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

A1: X1 is SubSpace of Y1 and

A2: 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 A3: ( Y1 misses Y2 or Y1 meet Y2 misses X1 union X2 ) ; :: thesis: ( Y1 misses X2 & Y2 misses X1 )

( Y1 misses X2 & Y2 misses X1 )

let X1, X2, Y1, 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 that

A1: X1 is SubSpace of Y1 and

A2: 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 A3: ( Y1 misses Y2 or Y1 meet Y2 misses X1 union X2 ) ; :: thesis: ( Y1 misses X2 & Y2 misses X1 )

now :: thesis: ( not Y1 misses Y2 implies ( Y1 misses X2 & Y2 misses X1 ) )

hence
( Y1 misses X2 & Y2 misses X1 )
by A1, A2, Th19; :: thesis: verumassume A4:
not Y1 misses Y2
; :: thesis: ( Y1 misses X2 & Y2 misses X1 )

end;A5: now :: thesis: not Y2 meets X1

assume
Y2 meets X1
; :: thesis: contradiction

then A6: Y1 meet Y2 meets X1 by A1, Th29;

X1 is SubSpace of X1 union X2 by TSEP_1:22;

hence contradiction by A3, A4, A6, Th18; :: thesis: verum

end;then A6: Y1 meet Y2 meets X1 by A1, Th29;

X1 is SubSpace of X1 union X2 by TSEP_1:22;

hence contradiction by A3, A4, A6, Th18; :: thesis: verum

now :: thesis: not Y1 meets X2

hence
( Y1 misses X2 & Y2 misses X1 )
by A5; :: thesis: verumassume
Y1 meets X2
; :: thesis: contradiction

then A7: Y1 meet Y2 meets X2 by A2, Th29;

X2 is SubSpace of X1 union X2 by TSEP_1:22;

hence contradiction by A3, A4, A7, Th18; :: thesis: verum

end;then A7: Y1 meet Y2 meets X2 by A2, Th29;

X2 is SubSpace of X1 union X2 by TSEP_1:22;

hence contradiction by A3, A4, A7, Th18; :: thesis: verum