let X be non empty TopSpace; 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; ( X1 meets X2 & X1,Y are_separated implies X1 meet X2,Y are_separated )
assume
X1 meets X2
; ( 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; verum