let X be non empty TopSpace; for X1, X2 being non empty SubSpace of X
for Y1, Y2 being SubSpace of X st Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & X1,X2 are_separated holds
Y1,Y2 are_separated
let X1, X2 be non empty SubSpace of X; for Y1, Y2 being SubSpace of X st Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & X1,X2 are_separated holds
Y1,Y2 are_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;
let Y1, Y2 be SubSpace of X; ( Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & X1,X2 are_separated implies Y1,Y2 are_separated )
assume A1:
( Y1 is SubSpace of X1 & Y2 is SubSpace of X2 )
; ( not X1,X2 are_separated or Y1,Y2 are_separated )
assume A2:
X1,X2 are_separated
; Y1,Y2 are_separated
hence
Y1,Y2 are_separated
; verum