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;

A2: now :: thesis: ( X0 meets X2 & ( X0 meets X2 or X2 meets X0 ) implies ( 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;

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