let X be non empty TopSpace; :: thesis: for X0, X1, X2 being non empty SubSpace of X st X1 meets X2 holds

( ( ( X1 misses X0 or X2 misses X0 ) implies X1 meet X2 misses X0 ) & ( ( X0 misses X1 or X0 misses X2 ) implies X0 misses X1 meet X2 ) )

let X0, X1, X2 be non empty SubSpace of X; :: thesis: ( X1 meets X2 implies ( ( ( X1 misses X0 or X2 misses X0 ) implies X1 meet X2 misses X0 ) & ( ( X0 misses X1 or X0 misses X2 ) implies X0 misses X1 meet X2 ) ) )

reconsider A0 = the carrier of X0 as Subset of X by TSEP_1:1;

reconsider A1 = the carrier of X1 as Subset of X by TSEP_1:1;

reconsider A2 = the carrier of X2 as Subset of X by TSEP_1:1;

assume A1: X1 meets X2 ; :: thesis: ( ( ( X1 misses X0 or X2 misses X0 ) implies X1 meet X2 misses X0 ) & ( ( X0 misses X1 or X0 misses X2 ) implies X0 misses X1 meet X2 ) )

thus ( ( X1 misses X0 or X2 misses X0 ) implies X1 meet X2 misses X0 ) :: thesis: ( ( X0 misses X1 or X0 misses X2 ) implies X0 misses X1 meet X2 )

( ( ( X1 misses X0 or X2 misses X0 ) implies X1 meet X2 misses X0 ) & ( ( X0 misses X1 or X0 misses X2 ) implies X0 misses X1 meet X2 ) )

let X0, X1, X2 be non empty SubSpace of X; :: thesis: ( X1 meets X2 implies ( ( ( X1 misses X0 or X2 misses X0 ) implies X1 meet X2 misses X0 ) & ( ( X0 misses X1 or X0 misses X2 ) implies X0 misses X1 meet X2 ) ) )

reconsider A0 = the carrier of X0 as Subset of X by TSEP_1:1;

reconsider A1 = the carrier of X1 as Subset of X by TSEP_1:1;

reconsider A2 = the carrier of X2 as Subset of X by TSEP_1:1;

assume A1: X1 meets X2 ; :: thesis: ( ( ( X1 misses X0 or X2 misses X0 ) implies X1 meet X2 misses X0 ) & ( ( X0 misses X1 or X0 misses X2 ) implies X0 misses X1 meet X2 ) )

thus ( ( X1 misses X0 or X2 misses X0 ) implies X1 meet X2 misses X0 ) :: thesis: ( ( X0 misses X1 or X0 misses X2 ) implies X0 misses X1 meet X2 )

proof

hence
( ( X0 misses X1 or X0 misses X2 ) implies X0 misses X1 meet X2 )
; :: thesis: verum
assume
( X1 misses X0 or X2 misses X0 )
; :: thesis: X1 meet X2 misses X0

then ( A1 misses A0 or A2 misses A0 ) by TSEP_1:def 3;

then (A1 /\ A0) /\ (A2 /\ A0) = {} ;

then A1 /\ ((A2 /\ A0) /\ A0) = {} by XBOOLE_1:16;

then A1 /\ (A2 /\ (A0 /\ A0)) = {} by XBOOLE_1:16;

then (A1 /\ A2) /\ A0 = {} by XBOOLE_1:16;

then the carrier of (X1 meet X2) /\ A0 = {} by A1, TSEP_1:def 4;

then the carrier of (X1 meet X2) misses A0 ;

hence X1 meet X2 misses X0 by TSEP_1:def 3; :: thesis: verum

end;then ( A1 misses A0 or A2 misses A0 ) by TSEP_1:def 3;

then (A1 /\ A0) /\ (A2 /\ A0) = {} ;

then A1 /\ ((A2 /\ A0) /\ A0) = {} by XBOOLE_1:16;

then A1 /\ (A2 /\ (A0 /\ A0)) = {} by XBOOLE_1:16;

then (A1 /\ A2) /\ A0 = {} by XBOOLE_1:16;

then the carrier of (X1 meet X2) /\ A0 = {} by A1, TSEP_1:def 4;

then the carrier of (X1 meet X2) misses A0 ;

hence X1 meet X2 misses X0 by TSEP_1:def 3; :: thesis: verum