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

( X1 meets X2 & X2 meets X1 )

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

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 X0 meets X2 & not X2 meets X0 ) or ( X1 meets X2 & X2 meets X1 ) )

then A1: A0 c= A1 by TSEP_1:4;

hence ( X1 meets X2 & X2 meets X1 ) by A2; :: thesis: verum

( X1 meets X2 & X2 meets X1 )

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

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 X0 meets X2 & not X2 meets X0 ) or ( X1 meets X2 & X2 meets X1 ) )

then A1: A0 c= A1 by TSEP_1:4;

A2: now :: thesis: ( X0 meets X2 & ( X0 meets X2 or X2 meets X0 ) implies ( X1 meets X2 & X2 meets X1 ) )

assume
( X0 meets X2 or X2 meets X0 )
; :: thesis: ( X1 meets X2 & X2 meets X1 )assume
X0 meets X2
; :: thesis: ( ( not X0 meets X2 & not X2 meets X0 ) or ( X1 meets X2 & X2 meets X1 ) )

then A2 meets A0 by TSEP_1:def 3;

hence ( ( not X0 meets X2 & not X2 meets X0 ) or ( X1 meets X2 & X2 meets X1 ) ) by TSEP_1:def 3, A1, XBOOLE_1:63; :: thesis: verum

end;then A2 meets A0 by TSEP_1:def 3;

hence ( ( not X0 meets X2 & not X2 meets X0 ) or ( X1 meets X2 & X2 meets X1 ) ) by TSEP_1:def 3, A1, XBOOLE_1:63; :: thesis: verum

hence ( X1 meets X2 & X2 meets X1 ) by A2; :: thesis: verum