let X be non empty TopSpace; :: thesis: 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; :: thesis: 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 Y1, Y2 be SubSpace of X; :: thesis: ( 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 ) ; :: thesis: ( not X1,X2 are_separated or Y1,Y2 are_separated )
reconsider A1 = the carrier of X1 as Subset of X by Th1;
reconsider A2 = the carrier of X2 as Subset of X by Th1;
assume A2: X1,X2 are_separated ; :: thesis: Y1,Y2 are_separated

now

let B1, B2 be Subset of X; :: thesis: ( B1 = the carrier of Y1 & B2 = the carrier of Y2 implies B1,B2 are_separated )
assume ( B1 = the carrier of Y1 & B2 = the carrier of Y2 ) ; :: thesis: B1,B2 are_separated
then ( A1,A2 are_separated & B1 c= A1 & B2 c= A2 ) by A1, A2, Def8, Th4;
hence B1,B2 are_separated by CONNSP_1:8; :: thesis: verum

end;

hence Y1,Y2 are_separated by Def8; :: thesis: verum