let X be non empty TopSpace; :: thesis: for X1, X2, Y being non empty SubSpace of X st X1 meets X2 & X1,Y are_separated holds
X1 meet X2,Y are_separated
let X1, X2, Y be non empty SubSpace of X; :: thesis: ( X1 meets X2 & X1,Y are_separated implies X1 meet X2,Y are_separated )
assume X1 meets X2 ; :: thesis: ( not X1,Y are_separated or X1 meet X2,Y are_separated )
then A1: X1 meet X2 is SubSpace of X1 by Th27;
Y is SubSpace of Y by Th2;
hence ( not X1,Y are_separated or X1 meet X2,Y are_separated ) by A1, Th71; :: thesis: verum