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