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_separated holds

B1,B2 are_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_separated holds

B1,B2 are_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_separated holds

B1,B2 are_separated

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

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

then reconsider C1 = B1 as Subset of X ;

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

then A3: B2 c= A2 by XBOOLE_1:17;

reconsider C2 = B2 as Subset of X by A2;

assume A4: A1,A2 are_separated ; :: thesis: B1,B2 are_separated

B1 c= A1 by A1, XBOOLE_1:17;

then C1,C2 are_separated by A3, A4, CONNSP_1:7;

hence B1,B2 are_separated by Th25; :: 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_separated holds

B1,B2 are_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_separated holds

B1,B2 are_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_separated holds

B1,B2 are_separated

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

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

then reconsider C1 = B1 as Subset of X ;

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

then A3: B2 c= A2 by XBOOLE_1:17;

reconsider C2 = B2 as Subset of X by A2;

assume A4: A1,A2 are_separated ; :: thesis: B1,B2 are_separated

B1 c= A1 by A1, XBOOLE_1:17;

then C1,C2 are_separated by A3, A4, CONNSP_1:7;

hence B1,B2 are_separated by Th25; :: thesis: verum