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
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; :: 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 )
assume A2: X1,X2 are_separated ; :: thesis: Y1,Y2 are_separated
now :: thesis: for B1, B2 being Subset of X st B1 = the carrier of Y1 & B2 = the carrier of Y2 holds
B1,B2 are_separated
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 A3: ( B1 c= A1 & B2 c= A2 ) by A1, Th4;
A1,A2 are_separated by A2;
hence B1,B2 are_separated by A3, CONNSP_1:7; :: thesis: verum
end;
hence Y1,Y2 are_separated ; :: thesis: verum