let X be non empty TopSpace; :: thesis: for X0 being non empty SubSpace of X

for X1, X2 being SubSpace of X

for Y1, Y2 being SubSpace of X0 st the carrier of X1 = the carrier of Y1 & the carrier of X2 = the carrier of Y2 holds

( X1,X2 are_separated iff Y1,Y2 are_separated )

let X0 be non empty SubSpace of X; :: thesis: for X1, X2 being SubSpace of X

for Y1, Y2 being SubSpace of X0 st the carrier of X1 = the carrier of Y1 & the carrier of X2 = the carrier of Y2 holds

( X1,X2 are_separated iff Y1,Y2 are_separated )

let X1, X2 be SubSpace of X; :: thesis: for Y1, Y2 being SubSpace of X0 st the carrier of X1 = the carrier of Y1 & the carrier of X2 = the carrier of Y2 holds

( X1,X2 are_separated iff Y1,Y2 are_separated )

let X01, X02 be SubSpace of X0; :: thesis: ( the carrier of X1 = the carrier of X01 & the carrier of X2 = the carrier of X02 implies ( X1,X2 are_separated iff X01,X02 are_separated ) )

reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by TSEP_1:1;

reconsider B1 = the carrier of X01, B2 = the carrier of X02 as Subset of X0 by TSEP_1:1;

assume A1: ( the carrier of X1 = the carrier of X01 & the carrier of X2 = the carrier of X02 ) ; :: thesis: ( X1,X2 are_separated iff X01,X02 are_separated )

thus ( X1,X2 are_separated implies X01,X02 are_separated ) :: thesis: ( X01,X02 are_separated implies X1,X2 are_separated )

for X1, X2 being SubSpace of X

for Y1, Y2 being SubSpace of X0 st the carrier of X1 = the carrier of Y1 & the carrier of X2 = the carrier of Y2 holds

( X1,X2 are_separated iff Y1,Y2 are_separated )

let X0 be non empty SubSpace of X; :: thesis: for X1, X2 being SubSpace of X

for Y1, Y2 being SubSpace of X0 st the carrier of X1 = the carrier of Y1 & the carrier of X2 = the carrier of Y2 holds

( X1,X2 are_separated iff Y1,Y2 are_separated )

let X1, X2 be SubSpace of X; :: thesis: for Y1, Y2 being SubSpace of X0 st the carrier of X1 = the carrier of Y1 & the carrier of X2 = the carrier of Y2 holds

( X1,X2 are_separated iff Y1,Y2 are_separated )

let X01, X02 be SubSpace of X0; :: thesis: ( the carrier of X1 = the carrier of X01 & the carrier of X2 = the carrier of X02 implies ( X1,X2 are_separated iff X01,X02 are_separated ) )

reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by TSEP_1:1;

reconsider B1 = the carrier of X01, B2 = the carrier of X02 as Subset of X0 by TSEP_1:1;

assume A1: ( the carrier of X1 = the carrier of X01 & the carrier of X2 = the carrier of X02 ) ; :: thesis: ( X1,X2 are_separated iff X01,X02 are_separated )

thus ( X1,X2 are_separated implies X01,X02 are_separated ) :: thesis: ( X01,X02 are_separated implies X1,X2 are_separated )

proof

thus
( X01,X02 are_separated implies X1,X2 are_separated )
:: thesis: verum
assume
X1,X2 are_separated
; :: thesis: X01,X02 are_separated

then A1,A2 are_separated ;

then for B1, B2 being Subset of X0 st B1 = the carrier of X01 & B2 = the carrier of X02 holds

B1,B2 are_separated by A1, Th25;

hence X01,X02 are_separated ; :: thesis: verum

end;then A1,A2 are_separated ;

then for B1, B2 being Subset of X0 st B1 = the carrier of X01 & B2 = the carrier of X02 holds

B1,B2 are_separated by A1, Th25;

hence X01,X02 are_separated ; :: thesis: verum

proof

assume
X01,X02 are_separated
; :: thesis: X1,X2 are_separated

then B1,B2 are_separated ;

then for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds

A1,A2 are_separated by A1, Th25;

hence X1,X2 are_separated ; :: thesis: verum

end;then B1,B2 are_separated ;

then for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds

A1,A2 are_separated by A1, Th25;

hence X1,X2 are_separated ; :: thesis: verum