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 )
now :: thesis: ( not Y1 misses Y2 implies ( Y1 misses X2 & Y2 misses X1 ) )
assume A4: not Y1 misses Y2 ; :: thesis: ( Y1 misses X2 & Y2 misses X1 )
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;
now :: thesis: not Y1 meets X2
assume 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;
hence ( Y1 misses X2 & Y2 misses X1 ) by A5; :: thesis: verum
end;
hence ( Y1 misses X2 & Y2 misses X1 ) by A1, A2, Th19; :: thesis: verum