let X be non empty TopSpace; for Y, X1, X2 being non empty SubSpace of X st X1 meets X2 holds
( ( X1,Y are_weakly_separated & X2,Y are_weakly_separated implies X1 meet X2,Y are_weakly_separated ) & ( Y,X1 are_weakly_separated & Y,X2 are_weakly_separated implies Y,X1 meet X2 are_weakly_separated ) )
let Y, X1, X2 be non empty SubSpace of X; ( X1 meets X2 implies ( ( X1,Y are_weakly_separated & X2,Y are_weakly_separated implies X1 meet X2,Y are_weakly_separated ) & ( Y,X1 are_weakly_separated & Y,X2 are_weakly_separated implies Y,X1 meet X2 are_weakly_separated ) ) )
assume A1:
X1 meets X2
; ( ( X1,Y are_weakly_separated & X2,Y are_weakly_separated implies X1 meet X2,Y are_weakly_separated ) & ( Y,X1 are_weakly_separated & Y,X2 are_weakly_separated implies Y,X1 meet X2 are_weakly_separated ) )
reconsider A2 = the carrier of X2 as Subset of X by Th1;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
reconsider C = the carrier of Y as Subset of X by Th1;
thus
( X1,Y are_weakly_separated & X2,Y are_weakly_separated implies X1 meet X2,Y are_weakly_separated )
( Y,X1 are_weakly_separated & Y,X2 are_weakly_separated implies Y,X1 meet X2 are_weakly_separated )
hence
( Y,X1 are_weakly_separated & Y,X2 are_weakly_separated implies Y,X1 meet X2 are_weakly_separated )
; verum