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

( X0 meets X1 & X1 meets X0 )

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

assume X0 is SubSpace of X1 ; :: thesis: ( X0 meets X1 & X1 meets X0 )

then A1: the carrier of X0 meets the carrier of X1 by XBOOLE_1:28, TSEP_1:4;

hence X0 meets X1 by TSEP_1:def 3; :: thesis: X1 meets X0

thus X1 meets X0 by A1, TSEP_1:def 3; :: thesis: verum

( X0 meets X1 & X1 meets X0 )

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

assume X0 is SubSpace of X1 ; :: thesis: ( X0 meets X1 & X1 meets X0 )

then A1: the carrier of X0 meets the carrier of X1 by XBOOLE_1:28, TSEP_1:4;

hence X0 meets X1 by TSEP_1:def 3; :: thesis: X1 meets X0

thus X1 meets X0 by A1, TSEP_1:def 3; :: thesis: verum