let X be non empty TopSpace; 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; 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; 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; ( 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
; ( 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
; ( 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
; 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; verum