let X be non empty TopSpace; :: thesis: for A1, A2 being Subset of X

for X0 being non empty SubSpace of X

for B1, B2 being Subset of X0 st B1 = the carrier of X0 /\ A1 & B2 = the carrier of X0 /\ A2 & A1,A2 are_weakly_separated holds

B1,B2 are_weakly_separated

let A1, A2 be Subset of X; :: thesis: for X0 being non empty SubSpace of X

for B1, B2 being Subset of X0 st B1 = the carrier of X0 /\ A1 & B2 = the carrier of X0 /\ A2 & A1,A2 are_weakly_separated holds

B1,B2 are_weakly_separated

let X0 be non empty SubSpace of X; :: thesis: for B1, B2 being Subset of X0 st B1 = the carrier of X0 /\ A1 & B2 = the carrier of X0 /\ A2 & A1,A2 are_weakly_separated holds

B1,B2 are_weakly_separated

let B1, B2 be Subset of X0; :: thesis: ( B1 = the carrier of X0 /\ A1 & B2 = the carrier of X0 /\ A2 & A1,A2 are_weakly_separated implies B1,B2 are_weakly_separated )

assume ( B1 = the carrier of X0 /\ A1 & B2 = the carrier of X0 /\ A2 ) ; :: thesis: ( not A1,A2 are_weakly_separated or B1,B2 are_weakly_separated )

then A1: ( B1 \ B2 = the carrier of X0 /\ (A1 \ A2) & B2 \ B1 = the carrier of X0 /\ (A2 \ A1) ) by XBOOLE_1:50;

assume A1 \ A2,A2 \ A1 are_separated ; :: according to TSEP_1:def 5 :: thesis: B1,B2 are_weakly_separated

then B1 \ B2,B2 \ B1 are_separated by A1, Th26;

hence B1,B2 are_weakly_separated ; :: thesis: verum

for X0 being non empty SubSpace of X

for B1, B2 being Subset of X0 st B1 = the carrier of X0 /\ A1 & B2 = the carrier of X0 /\ A2 & A1,A2 are_weakly_separated holds

B1,B2 are_weakly_separated

let A1, A2 be Subset of X; :: thesis: for X0 being non empty SubSpace of X

for B1, B2 being Subset of X0 st B1 = the carrier of X0 /\ A1 & B2 = the carrier of X0 /\ A2 & A1,A2 are_weakly_separated holds

B1,B2 are_weakly_separated

let X0 be non empty SubSpace of X; :: thesis: for B1, B2 being Subset of X0 st B1 = the carrier of X0 /\ A1 & B2 = the carrier of X0 /\ A2 & A1,A2 are_weakly_separated holds

B1,B2 are_weakly_separated

let B1, B2 be Subset of X0; :: thesis: ( B1 = the carrier of X0 /\ A1 & B2 = the carrier of X0 /\ A2 & A1,A2 are_weakly_separated implies B1,B2 are_weakly_separated )

assume ( B1 = the carrier of X0 /\ A1 & B2 = the carrier of X0 /\ A2 ) ; :: thesis: ( not A1,A2 are_weakly_separated or B1,B2 are_weakly_separated )

then A1: ( B1 \ B2 = the carrier of X0 /\ (A1 \ A2) & B2 \ B1 = the carrier of X0 /\ (A2 \ A1) ) by XBOOLE_1:50;

assume A1 \ A2,A2 \ A1 are_separated ; :: according to TSEP_1:def 5 :: thesis: B1,B2 are_weakly_separated

then B1 \ B2,B2 \ B1 are_separated by A1, Th26;

hence B1,B2 are_weakly_separated ; :: thesis: verum